[commonlisp94]

This is not true.

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.

[ukj]

At that level of pedantry even the halting problem is solvable. Just choose a suitable representation for the Turing machines in question.

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.

[consilient]

That's no longer the halting problem: formally, the input to a halting oracle is an index for some fixed choice of admissible numbering of the set of Turing machines, meaning one that can be computed from the standard numbering induced by some universal Turing machine. Your encoding is not admissible.

[ukj]

>That's no longer the halting problem

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)

[consilient]

> 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.

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.

[ukj]

You say “restricted” I say “better defined”. Either way - A constructive setting is more expressive.

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.

[consilient]

> You say “restricted” I say “better defined”.

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.

[commonlisp94]

No, the comment above mine is the one being pedantic. We can absolutely talk about physical correspondence of mathematical concepts, even though there are multiple equally good logical systems for describing them.

[ukj]

Correspondence is a relation.

Relations are functions.

Can you tell us more about this function which relates Mathematical concepts to physical reality?

[commonlisp94]

> Relations are functions.

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.

[ukj]

The fact is you are talking about the meaning of words. Be they English words; or Mathematical words.

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?

https://en.wikipedia.org/wiki/Symbol_grounding_problem

[mcguire]

What is the sum of the interior angles of a triangle?

[commonlisp94]

Let's recall your original comment. You said we can't talk about reality correspondence of math because multiple logical systems can describe physical space equally well.

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.

[mcguire]

What? I said nothing of the sort.

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.