Torn between classical and constructive mathematics

[godelian]

ChatGPT: Does constructive mathematics acknowledge the existence of the set of uncomputable numbers?

Great question — and it gets to the heart of the philosophical differences in mathematics!

In constructive mathematics, the existence of a mathematical object typically means that you can construct it explicitly — i.e., give a procedure to build or describe it. This is different from classical mathematics, where something can be said to exist just because its nonexistence would lead to a contradiction.

Uncomputable numbers, by definition, are real numbers for which no algorithm exists that can produce their digits. In classical mathematics, it's easy to prove that almost all real numbers are uncomputable (using diagonalization and cardinality arguments). But constructive mathematics is more conservative — it doesn't accept the existence of objects unless they can be constructed explicitly.

Constructive mathematics generally does not acknowledge the existence of the set of uncomputable numbers in the same way classical mathematics does, because you can't construct such a set — or even a member of it — explicitly. Only objects that can be built step-by-step or specified algorithmically are accepted.

In this case, I totally disagree with the view of constructive mathematics on uncomputable numbers. It almost sounds like: We vehemently deny the existence of unsolvable problems because unless you solve the problem, the problem does not even exist.

But then again, classical mathematicians can also be psychopaths:

ChatGPT: Does classical mathematics allow the use of the axiom of choice on the set of uncomputable numbers?

Yes, classical mathematics allows the use of the axiom of choice (AC) on any set, including the set of uncomputable numbers. Classical set theory (like Zermelo–Fraenkel set theory with the axiom of choice, or ZFC) makes no restrictions on how sets are defined or constructed, whether or not the elements are computable, definable, or even explicitly describable. In this framework, the axiom of choice applies to any collection of nonempty sets, regardless of whether we can explicitly describe their elements or have an algorithm to select them.

Using AC on Uncomputable Numbers:

The axiom of choice doesn't require us to construct a choice function explicitly — it merely asserts the existence of one. So in classical mathematics, you can apply the axiom of choice to select an element from every nonempty subset of uncomputable numbers, even though you can't compute that choice.

It is impossible to choose an uncomputable number out of its set. By definition, there is no procedure for that. However, by using the Axiom of Choice, they simply brush this problem under the table. That is an approach from Absurdistan. In fact, they use an axiom to overrule the definition of uncomputable number. A choice is a computation. How can you do that computation in the context of the uncomputable? The classical position almost sounds like: The problem is unsolvable but if we create an additional axiom that the unsolvable problem can be solved, then the problem is no longer unsolvable. Henceforth, the problem has a solution, even though we cannot tell you what that solution actually is.

My current take on the matter is that both classical as constructive mathematics can develop tendencies of becoming absurd.

[Skepdick]

...

You have missed the forrest for the trees.

Whether you are working classically; or constructively you are still using symbolic logic. A symbol represents/denotes whatever you say it represents/denotes. It has no "inherent meaning"

You want a term of the type "Set of uncomputable numbers". OK... that term is S.
S denotes/represents the set of uncountable uncomputable numbers. Now what? What can you DO with S? Well... I can DO whatever we say about S.

And we have said that... forall x in S: Uncomputable(X) is true. By definition.

Namely, I can tell you that the set of computable functions which have a value in S is not inhabited.
And if you can, in fact produce a function f() such that f terminates/produces a value; then f is not in S. Boring.

OK... the symbol S represents the "set of uncomputable numbers". And now what?
How do you interact with it? What functions are computable on it?

If you want an intuition for it. Imagine S as an object in an object-oriented programming language.

The interesting questions are: What sort of functions are computable on S? What methods does the object have?
How do you interact with that object?
What sort of messages can you send to it?
What sort if responses can you receive from it?

Can you do S.contains(x) ?
Can you do S.cardinality() ?
Can you do S.isEmpty() ?

It's just a game of message-passing. Request - response.

It is impossible to choose an uncomputable number out of its set.

Why? The set exists. You have the axiom of choice. Therefore you have. S.getRandomElement() and this function will produce a result.

So you have an uncomputable number: g := S.getRandomElement()

What can you do with such an object? What methods does g support? What operations can you perform on g?

Well ... none! It's uncomputable!

Oh but hey.... we have an axiom... forall x in S: Uncomputable(X) is true.

So I can tell you Uncomputable(g) is true.

My current take on the matter is that both classical as constructive mathematics can develop tendencies of becoming absurd.

absurdity is a type. absurd :: Void → a (a is any type).

You can always interpret the axiom of choice (or applications thereof) as a function which takes NO values/parameters (void) and returns an object of ANY type.

This is not even new; or interesting. It's just this intuition applied...

https://math.andrej.com/2008/02/06/repr ... able-sets/

In general, we can make any function f:X->Y whatsoever computable if we are allowed to change the representation of X: represent elements x in X as pairs (a,b) where a represents x (in the original representation of X) and b represents f(x) in the representation of Y. The function f then becomes easily computable as the first projection: given a pair (a,b) representing x, the value f(x) is represented by b.

The distinction between Classical Mathematics and Constructive Mathematics is the distinction between assembly (imperative) programming and object-oriented programming.

Constructive Mathematics (like OOP) with methods that operate on that data. it focuses on operationalizing Mathematics away from the abstract Classical nonsense.

No applied mathematician gives a shit about some weird abstract objects whose existence is declared, yet you can't DO anything with them.
Such objects are functional blackboxes - they are terminal/irreducible.

They are like /dev/null (not even /dev/zero).
You can write infinite information into them (e.g you can assign whatever meaning you want to it), but you can't get anything out.

[godelian]

No applied mathematician gives a shit about some weird abstract objects whose existence is declared, yet you can't DO anything with them.
Such objects are functional blackboxes - they are terminal/irreducible.

They are like /dev/null (not even /dev/zero).
You can write infinite information into them (e.g you can assign whatever meaning you want to it), but you can't get anything out.

Yes, agreed, uncomputable objects are fundamentally unusable. However, these objects are eminently useful to elucidate the details of the structure of arithmetic truth. For example:

ChatGPT: True arithmetic is defined to be the set of all sentences in the language of first-order arithmetic that are true in N, written Th(N). Does constructive mathematics acknowledge the existence of this set?

Constructive mathematics generally does not acknowledge the existence of the full set Th(ℕ), because doing so would require accepting principles (like the law of excluded middle) that constructive frameworks typically reject.

In classical logic, we take for granted that each sentence in this language is either true or false in ℕ, so the set Th(ℕ) is well-defined — though not computable, due to Tarski's undefinability of truth and Gödel's incompleteness theorems.

However, in constructive mathematics, particularly in frameworks like intuitionistic logic, truth is not bivalent: a statement is only true if we can constructively prove it, and a statement is false if we can constructively refute it.

A Constructivist Might Say:

"We can talk about the set of all arithmetic sentences provable in our constructive system (e.g., Heyting Arithmetic), but not the set of all sentences that are classically true in ℕ — because we reject the notion of truth that is divorced from provability."

Concerning "we reject the notion of truth that is divorced from provability", this point of view clearly rejects Gödel's classical work. I cannot possibly reconcile myself with this view. If you accept that truth and provability are in fact divorced, then you can see much more, and understand much more, about arithmetical truth. For example, the paper "True but unprovable" by Noson S. Yanofsky is incredibly insightful as to what arithmetic truth really looks like (http://www.sci.brooklyn.cuny.edu/~noson ... ovable.pdf).

Furthermore, Tarski's model theory is to an important extent about nonstandard models/universes of arithmetic populated with nonstandard, uncomputable numbers on which new computations are certainly not supported in any way:

https://en.wikipedia.org/wiki/Non-stand ... arithmetic

Tennenbaum's theorem shows that for any countable non-standard model of Peano arithmetic there is no way to code the elements of the model as (standard) natural numbers such that either the addition or multiplication operation of the model is computable on the codes. This result was first obtained by Stanley Tennenbaum in 1959.

If the Pythagorean view from antiquity is correct, i.e. the arithmetical multiverse and the physical multiverse are structurally similar, then rejecting that the notion of truth is divorced from provability, will ultimately also prevent you from understanding the structure of the physical universe. Therefore, I reject what constructive mathematics says about Th(ℕ), about model theory, or about nonstandard models of arithmetic. Constructive mathematics has a very poor view on the abstract, Platonic world of mathematical objects.

Furthermore, I simply don't care that these weird abstract objects are indeed of no use to the applied mathematician.

[Skepdick]

Concerning "we reject the notion of truth that is divorced from provability", this point of view clearly rejects Gödel's classical work.

Sure. It's the semantic vs syntactic view of Mathematics.

Computationally - it's a distinction without a difference. Semantics is just more syntax.

It's still symbol-manipulation. And manipulation of anything (matter; or symbols) is computation.

I cannot possibly reconcile myself with this view. If you accept that truth and provability are in fact divorced, then you can see much more, and understand much more, about arithmetical truth.

There's no fucking difference. If you accept truth (as in theorem) then you'll accept any system in which the theorem holds.

And if you can't find a system where the truth of a theorem holds... then you can trivially make the theorem hold by identity. X -> X

Take any principle and invent any system where the principle succeeds; or fails.

[godelian]

There's no fucking difference. If you accept truth (as in theorem) then you'll accept any system in which the theorem holds.
And if you can't find a system where the truth of a theorem holds... then you can trivially make the theorem hold by identity. X -> X
Take any principle and invent any system where the principle succeeds; or fails.

It is about standard arithmetic. It contains ineffable theorems. Such theorem is not just unprovable. it is even unspeakable. That is why you cannot manipulate it as an individual theorem. You need to accept it as a set of theorems in which you cannot choose an individual one.

This is not about a new system. This is about the standard system.

[Skepdick]

It is about standard arithmetic. It contains ineffable theorems.

Which arithmetic is "standard"?

The one which coincides precisely with the ineffable theorems you accept?
None of the ones which contain any theorems you (ineffably) reject?

Such theorem is not just unprovable. it is even unspeakable.

OK...what does that even mean? Can you detect violations; or non-satisfactions of your unspeakable theorems; or not?

That is why you cannot manipulate it as an individual theorem. You need to accept it as a set of theorems in which you cannot choose an individual one.

This is not about a new system. This is about the standard system.

OK... So does your "standard" system allow me to sell you 3 apples; even though I only have 2?

Is your "standard" arithmetic closed under addition and open under subtraction; or closed under both addition and subtraction?

[godelian]

Which arithmetic is "standard"?

Th(ℕ) is the complete truth about PA.

One which coincides precisely with the ineffable theorems you accept?
None of the ones which contain any theorems you (ineffably) reject?

Model theory is about structure. Not about computation.

OK...what does that even mean? Can you detect violations; or non-satisfactions of your theorems; or not?

You can only do that with individual sentences, not with sets of sentences. You cannot pick one such sentence out of Th(ℕ).

Is your "standard" arithmetic closed under addition and open under subtraction; or closed under both addition and subtraction?

It's about PA.

Yanovsky discusses the nature and some of the structure of Th(ℕ) in his paper "True but unprovable".

[Skepdick]

Which arithmetic is "standard"?

Th(ℕ) is the complete truth about PA.

OK... so your "standard" arithmetic is defined on ℕ; not on ℤ.

Meaning that 2-3 is a syntax error; and 2-3=-1 is not true.

Model theory is about structure. Not about computation.

That's a non-response. I am asking whether you can detect when your ineffable structure is satisfied; and when it isn't.

Because that's exactly and precisely a decision procedure.

Sat(X,Y) is the predicate/relation which is true IFF X satisfies the structure Y.

It's about PA.

OK... so 2-3 is not an arithmetic statement/expresion?

There is no difference between syntax and semantics in a computational paradigm!

2+3 is syntactically valid in PA (semantically/computationally - it returns 5).
2-3 is syntactically invalid in PA (semantically/computationally - it returns ??? Syntax error? DomainError? InvalidExpressionError? KernelPanic/Crash?)

What does your computational/proof-theoretic system DO when it encounters the expression "2-3" ?

You can certainly extend any system to say more; and more; and more... but you can't extend it to say everything.

[godelian]

the same
What does your computational/proof-theoretic system DO when it encounters the expression "2-3" ?

The expression is not valid in PA. Th(ℕ) is the truth about the natural numbers; not about the integers.

[Skepdick]

the same
What does your computational/proof-theoretic system DO when it encounters the expression "2-3" ?

The expression is not valid in PA. Th(ℕ) is the truth about the natural numbers; not about the integers.

OK... you are refusing to answer my question for some reason.

First you were talking about arithmetic truth. Now you are moving the goal posts to "truth about the natural numbers" and "truth about integers".

I don't care about any of that jazz. I want to know if the expression "2-3=-1" satisfies the ineffable structure you call "arithmetic"

[godelian]

the same
What does your computational/proof-theoretic system DO when it encounters the expression "2-3" ?

The expression is not valid in PA. Th(ℕ) is the truth about the natural numbers; not about the integers.

OK... you are refusing to answer my question for some reason.

First you were talking about arithmetic truth. Now you are moving the goal posts to "truth about the natural numbers" and "truth about integers".

I don't care about any of that jazz. I want to know if 2-3=-1 satisfies the structure you call "arithmetic"

I was only talking about "true arithmetic":

https://en.m.wikipedia.org/wiki/True_arithmetic

In mathematical logic, true arithmetic is the set of all true first-order statements about the arithmetic of natural numbers. This is the theory associated with the standard model of the Peano axioms in the language of the first-order Peano axioms.

ChatGPT: Does 2-3=-1 satisfy the set of all true first-order statements about the arithmetic of natural numbers?

No, the statement 2 − 3 = −1 does not satisfy the set of all true first-order statements about the arithmetic of natural numbers.

Here's why:

The natural numbers (usually denoted ℕ) typically start at 0 or 1, depending on the convention, and include only non-negative integers:
ℕ = {0, 1, 2, 3, ...} or ℕ = {1, 2, 3, ...}

In either case, −1 is not a natural number.

Subtraction like 2 − 3 is not always defined in ℕ, because it can lead to negative results which are outside the set of natural numbers.

So in standard first-order Peano arithmetic (which formalizes arithmetic over ℕ), the expression 2 − 3 is not defined, or if subtraction is defined as a partial function, it would be undefined in this case.

Conclusion:

The statement 2 − 3 = −1 is not true in the standard model of the natural numbers and therefore does not satisfy the set of all true first-order statements about ℕ.

[Skepdick]

The natural numbers (usually denoted ℕ) typically start at 0 or 1, depending on the convention, and include only non-negative integers:
ℕ = {0, 1, 2, 3, ...} or ℕ = {1, 2, 3, ...}

OK... so is "true arithmetic" closed or open under x-x? for x ∈ ℕ

What condition/relation between x and y determines whether x-y is a valid operation; or not?
Is "x-y" valid when y < x; or is it valid when y <= x ?

[godelian]

The natural numbers (usually denoted ℕ) typically start at 0 or 1, depending on the convention, and include only non-negative integers:
ℕ = {0, 1, 2, 3, ...} or ℕ = {1, 2, 3, ...}

OK... so is "true arithmetic" closed or open under x-x? for x ∈ ℕ

What condition/relation between x and y determines whether x-y is a valid operation; or not?
Is "x-y" valid when y < x; or is it valid when y <= x ?

Zero is axiomatized in PA. So, true arithmetic is closed under x-x.

[Skepdick]

The natural numbers (usually denoted ℕ) typically start at 0 or 1, depending on the convention, and include only non-negative integers:
ℕ = {0, 1, 2, 3, ...} or ℕ = {1, 2, 3, ...}

OK... so is "true arithmetic" closed or open under x-x? for x ∈ ℕ

What condition/relation between x and y determines whether x-y is a valid operation; or not?
Is "x-y" valid when y < x; or is it valid when y <= x ?

Zero is axiomatized in PA. So, true arithmetic is closed under x-x.

That's a non-sequitur.

I am asking you about your "ineffable theorem" of "true arithmetic"; not the axioms of "true arithmetic".

Is your "ineffable theorem" violated when 0 is NOT axiomatized; or is your "ineffable theorem" violated when 0 IS axiomatized?
Are you operating within a structure in which x-x is ALWAYS defined; or a structure in which x-x is NEVER defined?

[godelian]

OK... so is "true arithmetic" closed or open under x-x? for x ∈ ℕ

What condition/relation between x and y determines whether x-y is a valid operation; or not?
Is "x-y" valid when y < x; or is it valid when y <= x ?

Zero is axiomatized in PA. So, true arithmetic is closed under x-x.

That's a non-sequitur.

I am asking you about your "ineffable theorem" of "true arithmetic"; not the axioms of "true arithmetic".

Is your "ineffable theorem" violated when 0 is NOT axiomatized; or is your "ineffable theorem" violated when 0 IS axiomatized?
Are you operating within a structure in which DEFINED(x-x) is always true; or a structure in which NOT(DEFINED(x-x)) is always true?

Check the wikipedia page for more details: https://en.wikipedia.org/wiki/True_arithmetic