They are incompatible sets of axioms, but they can describe the same set of shapes, although one system is going to be a lot more inconvenient than the other. The differences are logically interesting, but about as incompatible as choosing to make the origin of a euclidean system one corner of the room instead of another.
In contrast physical theories contradict each other by making different predictions which can be falsified.
Describe/represent the ones that halt using 1; and the ones that don’t halt using 0. This produces the pairs (TM1, 1), (TM2, 1), (TM3, 0) etc.
Using this encoding the problem becomes trivial. It’s all other encodings which are unwieldy, complex and inconvenient.
Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable.
So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not.
Formally speaking Turing machines are formal language recognizers, so in which formal language is the formal statement of the Halting problem expressed in?
I'd also like to see the decider for "admissible" vs "inadmissible" encodings. Input validation is an Interesting problem-domain for sure.
(Of course, this is all for the sake of maximum pedantry)
Moving to a constructive setting lets you say things like "all functions are computable" because it has a restricted notion of function. It does not give you any new information about classical objects.
So express your English adjectives in Mathematics.
What do you mean by “restricted” when you are characterising a function?
Show me the decider… for “classical” and “non-classical” objects.
That is the definition of information; is it not? The answer to a yes/no questions
Is the object classical? Yes/no.
Sure, whatever - the point is that they're different objects, and results about one are not results about the other.
> What do you mean by “restricted” when you are characterising a function?
I mean whatever the word "function" means in a given setting. A classical function X -> Y is a relation such that if `(x, y1)` and `(x, y2)` hold then `y1 = y2`. A function in intuitionistic type theory is a well-typed lambda term. A function in the categorical semantics of a type theory is an exponential object. And so on.
> Show me the decider… for “classical” and “non-classical” objects.
No such thing: it's a metatheoretical judgement, not a theorem. Same story as type errors: within the language, `stringToUpperCase (5 :: Int) :: String` isn't a false statement, it's just inexpressible nonsense. There is no such object as `stringToUpperCase 5` and so nothing can be said about it internally. When we talk about it, we're talking, from outside the language, about a syntactic construct.
> That is the definition of information; is it not? The answer to a yes/no questions
No. Self-information of a given outcome with respect to a random variable, which is probably the most common sense of the word, is the negative log of its probability. Shannon entropy, also often called information, is the expected self-information of a random variable. Mutual information is the KL divergence of a joint distribution and the product of the respective marginals. There are other notions.
Sorry, I don't understand what you mean by "same" and "different".
By "same" do you mean =(x,y). And by "different" do you mean ¬=(x,y)
Or do you mean something like same(x,y) = { 1 if ??? else 0 }
>A classical function X -> Y is a relation such that if `(x, y1)` and `(x, y2)` hold then `y1 = y2
You seem to be confusing syntax and semantics here, and the infix notation isn't helping...
What does =(y1, y2) mean? What does =(x,x) mean?
>No such thing: it's a metatheoretical judgement, not a theorem.
What do you mean? Judgments are first-class citizens in Univalent Mathematics. a:R is a judgment that object a is of type R. This literally means "a proves R", and the particular expression "first class citizen" has well-understood meaning in Programming Language design ( https://en.wikipedia.org/wiki/First-class_citizen ).
>`stringToUpperCase (5 :: Int) :: String` isn't a false statement, it's just inexpressible nonsense.
So I must be a miracle worker then? Expressing the inexpressible nonsense...
In [1]: def stringToUpperCase(x): return(str(x).upper())
In [2]: stringToUpperCase(int(5))
Out[2]: '5'
Speaking of randomness in a classical setting, this function exists, right?
f(x) = { 1 if random(x), else 0 }
Relations are functions.
Can you tell us more about this function which relates Mathematical concepts to physical reality?
That is how they are defined in set theory based math. The mathematical definition is not the only meaning of a word. When when start to talk about the physical world, we need additional concepts. You are welcome to read the wikipedia page about correspondence theories of truth.
If you are going to talk about the correspondence theory in the same breath as you are talking about any language - you need to solve the symbol-grounding problem.
What function/mechanism/relation (or if you don't like any of those words - pick your own) grounds symbols?
A triangle in a euclidean system is not the same shape as a triangle in spherical, etc. They are only equivalent in that they have an analogous logical definition in their separate systems.
They don't look the same. They don't describe the same physical phenonoma either. In other words, the physical correspondence is not the same, so there is no contradiction.
In what we laughingly call "normal" geometry, given a line L and a point P not on L, there is exactly one line L' through P parallel to L. In this case, the interior angles of a triangle sum to 180 degrees.
In hyperbolic geometry, there is more than one line L', L'', etc., through P that are parallel to L. In this case, the interior angles of a triangle sum to <180 degrees.
In elliptic geometry, there are no lines L' through P parallel to L. (You also have to alter Euclid's 2nd axiom, defining a line as extending indefinitely.) And in this case, the interior angles of a triangle sum to >180 degrees.
Triangles are triangles; they have three points and three line segments. Their properties, however, are inconsistent in the three axiomatic systems.
If you are operating in a relatively small area, say a bronze-age farmer's field, Euclid's axioms satisfy all your geometrizing needs. If, however, you are on the somewhat-spherical Earth and are dealing with a large enough area, you can make a triangle with three 90 degree interior angles. You can tell which geometry your "physical space" is dealing with, and if you use the wrong one then you will get wrong answers.
For more than 2000 years, geometers assumed their space was essentially Euclidian. It turns out that is not really true, and it also turns out that there are (now, common) situations where the difference matters. So when you do any applied math, you assert that your axioms "faithfully reflect reality". And you may be wrong. And you may not have any way of knowing you are wrong. And you may not even have the mathematical tools to know what "wrong" means.