The position of constructive mathematics on Goodstein's theorem

[Skepdick]

If you really want total control over memory and no assistance/tooling to save you from yourself why not grab a punch card?

I was just pointing out the limitations of what you wrote earlier:

There are no limitations of what I wrote earlier. My statement is generic - both in the common sense meaning e.g general/broad and in the precise technical sense of "generic programming".

It's so strange that you haven't joined the dots between Generic programming (a.k.a parametric polymorphism) and the y-axis on the Lambda cube.

This interpretative freedom you so deeply desire is already formalized in the Calculus of Construction.

Nothing anywhere mandates you to interpret the configurations of bits in memory as "natural numbers", or UTF-8; or anything.
Any given bit; or a collection of bits could represent anything. That's just an arbitrary choice.

So, about "Nothing anywhere mandates you to interpret", the answer is that the tools do. It is hard and it takes effort to escape mandatory interpretation.

Nothing anywhere mandates you to use the tools which force upon you choices that you disagree with.
Especially since those "default choices" have well documented escape hatches.

It takes minimal effort to use those escape hatches.
It takes zero effort to use no tools whatsoever.

Write your own tools - which encode your own interpretative choices. You can even construct your own virtual machine with its own memory model to abstract away the hardware peculiarities underneath. As you see fit.

Interpretative choice exists at every level of computing, from individual bits to entire system architectures.

You know. Because meta circular evaluation.

[promethean75]

I can't understand you, Skep. You're starting to talk with a LISP.

(get it.... LISP? Nice.)

[Skepdick]

I can't understand you, Skep. You're starting to talk with a LISP.

(get it.... LISP? Nice.)

Lithp? What lithp?

[godelian]

Write your own tools - which encode your own interpretative choices. You can even construct your own virtual machine with its own memory model to abstract away the hardware peculiarities underneath. As you see fit.

Such rebellion against the established order is rarely successful. Occasionally, it works, though.

[Skepdick]

Write your own tools - which encode your own interpretative choices. You can even construct your own virtual machine with its own memory model to abstract away the hardware peculiarities underneath. As you see fit.

Such rebellion against the established order is rarely successful. Occasionally, it works, though.

Rebellion? You aren't forcing anyone else to use your tools.

You'd be merely reinventing your own. On the quest for self-sufficiency you have nothing to lose but time.

[godelian]

Rebellion? You aren't forcing anyone else to use your tools.

You'd be merely reinventing your own. On the quest for self-sufficiency you have nothing to lose but time.

If you build your own, it assumes that you know better than the existing tools. In my experience, this is rarely the case, but occasionally, it is.

For example, the decades-old quest for an alternative for the C compiler (and libc) for systems programming. We all know that C has its quirks. However, every alternative seems to be even worse. For example, the Linux kernel was supposedly going to accept contributions in Rust. It has led to a rebellion in the ranks of long-time kernel programmers. They consider the cure to be even worse than the disease.

[Skepdick]

Rebellion? You aren't forcing anyone else to use your tools.

You'd be merely reinventing your own. On the quest for self-sufficiency you have nothing to lose but time.

If you build your own, it assumes that you know better than the existing tools. In my experience, this is rarely the case, but occasionally, it is.

OK, but you were insisting that existing tools constrain your interpretative choice in a manner that's unacceptable to you.

Did that change?

For example, the decades-old quest for an alternative for the C compiler (and libc) for systems programming. We all know that C has its quirks. However, every alternative seems to be even worse.

Worse? You want more interpretative choice (neuter C's safety nets); but when you are given it you don't want it?

For example, the Linux kernel was supposedly going to accept contributions in Rust. It has led to a rebellion in the ranks of long-time kernel programmers. They consider the cure to be even worse than the disease.

OK but this has nothing to do with the social dynamics at play.

This was about your own, personal gripe with the interpretative impositions of the tools you are using; and your desire for interpretative freedom.

Rust is a much stricter language than C and it can detect vastly more errors in your code. So if C already feels too opinionated and restrictive; I can only imagine why Rust would feel even worse. The upside of Rust is that you get memory safety. The down side is that you have more rules.


None of this should matter to you because both Rust and C have escape hatches and you can turn off all the hand-holding at any point.
Perhaps you want the opposite approach? Zero hand-holding by default with optional hand-holding when desired?

You want a dynamic language without all the pitfalls.
You want a square triangle.

[godelian]

Worse? You want more interpretative choice (neuter C's safety nets); but when you are given it you don't want it?
This was about your own, personal gripe with the interpretative impositions of the tools you are using; and your desire for interpretative freedom.

It is not that I "want more interpretative choice". It was about your earlier remark:

Nothing anywhere mandates you to interpret the configurations of bits in memory as "natural numbers", or UTF-8; or anything.
Any given bit; or a collection of bits could represent anything. That's just an arbitrary choice.

I was merely pointing out the implications of what "interpretative choice" actually means in practice. I have exactly zero ambition to try to improve the C compiler for systems programming. There are people who try, though. This is what it leads to:

https://felipec.wordpress.com/2025/02/1 ... for-linux/

Rust doesn’t belong in the Linux kernel; it’s all about ideology

Rust in the Linux kernel has been a source of drama for quite some time now, and while I somewhat sympathize with both sides (pro-Rust and anti-Rust), I believe the fundamental problem is that both sides don’t really understand each other (although one side more than the other), and it’s not just the technical issue of how to better write a kernel: it’s much more that the entire worldview is different.

The latest chapter in the saga is the resignation of yet another maintainer because of the way one of the patches for Rust support was handled.

TRIGGER WARNING: this article contains political references, even though I’ll try to refrain from any value judgement, people who need trigger warnings will find my implications offensive.

Not all of us are married to C, I would love a language that was like C, but better, unfortunately there isn’t one (that includes Rust, Go, and Zig). People who think otherwise are not experts at C. Only somebody who is exceptional at C can tell you if there is a fine replacement, and as I argued in another article: most people are not great at C, and that includes developers with years of experience writing C.

When I discuss with Rust advocates and mention the fact that you can’t write a simple linked list like linux does (intrusive doubly circular linked list), they say two things 1) “yes you can” (untrue), and 2) “you shouldn’t want that”. Typical “it’s not happening and it’s a good thing that it is” responses.

The moment somebody tells me “you shouldn’t want that”, I stop using their software. Period.

I shouldn’t need to explain why I want to do something, the software either supports it or it doesn’t. I can’t count the number of times I’ve asked for help on some chat only to be told I shouldn’t want to do that — with the assumption that I know less than they do.

It is pointless to try to change the mind of somebody with an entrenched worldview, it would be as pointless as trying to change the mind of some family member who believes Donald Trump is Hitler.

What I’ve heard Rust advocates say is that linux is wrong in using linked lists in the first place. Right… because Rust advocates (many who likely aren’t even that good in Rust) know better than the best C developers out there, including Linus Torvalds.

Ironically progressive people boast themselves about being “inclusive”, but the second somebody expresses an opinion they vehemently dislike, they immediately segregate that person and anybody who thinks like him.

If you believe Christoph is technically wrong, that’s fine, you are entitled to your opinion, but why must progressives jump from technically wrong to immoral?

Programming is highly ideological. It is full of politics, and the politics are about interpretative choice. But then again, I am saying this descriptively. I am not saying this normatively. I am not advocating anything. I am not clamoring for anything to change. I do not have any "personal gripe with the interpretative impositions of the tools" I am using. I have no "desire for interpretative freedom". I am just describing what is going on. The article that I quoted is actually much more normative that me. The author rejects Rust. He prefers C. I am simply acknowledging that he does. This is how the world seems to turn around. These things are so incredibly political.

[Skepdick]

Worse? You want more interpretative choice (neuter C's safety nets); but when you are given it you don't want it?
This was about your own, personal gripe with the interpretative impositions of the tools you are using; and your desire for interpretative freedom.

It is not that I "want more interpretative choice". It was about your earlier remark:

Nothing anywhere mandates you to interpret the configurations of bits in memory as "natural numbers", or UTF-8; or anything.
Any given bit; or a collection of bits could represent anything. That's just an arbitrary choice.

I was merely pointing out the implications of what "interpretative choice" actually means in practice. I have exactly zero ambition to try to improve the C compiler for systems programming.

I don't know why you are so set on missing the point.

Yes, the compiler has a default choice which you can accept; or override; but it's neither mandatory to accept; nor mandatory to reject the compiler's default choice.

Choosing to use the default is a choice.
Choosing to use your own implementation is also a choice.

Therefore....

Nothing anywhere mandates you to interpret the configurations of bits in memory as "natural numbers", or UTF-8; or anything.
Any given bit; or a collection of bits could represent anything. That's just an arbitrary choice.

Yes, the default choice exerts weight which becomes a social norm.
Yes, going against the default choice is like swimming upstream.

But which way you swim (upstream; or downstream) is up to you.

[godelian]

Choosing to use the default is a choice.

Choosing the default usually amounts to avoiding to make a choice. Overruling the default requires knowledge about the subject and awareness of the implications.

[Skepdick]

Choosing the default usually amounts to avoiding to make a choice. Overruling the default requires knowledge about the subject and awareness of the implications.

And that's how you end up with classical mathematics/set theory as your "foundation"... Cultural momentum that you fail to bypass.

[godelian]

Choosing the default usually amounts to avoiding to make a choice. Overruling the default requires knowledge about the subject and awareness of the implications.

And that's how you end up with classical mathematics/set theory as your "foundation"... Cultural momentum that you fail to bypass.

Even though I acknowledge some of the concerns expressed by constructive mathematics, I also clearly see where it is being unreasonable.

For example, we know that uncomputable numbers exist and that they are inexpressible. Asking us to express a witness, i.e. an actual example, is clearly unreasonable.

More generally, there exist nonempty sets of mathematical objects -- we can prove their existence -- for which it is not possible to construct a witness.

So, I decisively and resolutely refuse to overrule the default of classical mathematics. It is not just cultural momentum. I do not want to switch to constructivism because I consider it to be often unreasonable. It is a deliberate choice and not just a default.

[Skepdick]

For example, we know that uncomputable numbers exist and that they are inexpressible. Asking us to express a witness, i.e. an actual example, is clearly unreasonable.

Since you can't express a witness; can you at least express how you know that uncomputable numbers exist?

Given that you can't tell me absolutely anything about an uncomputable number (not even how it interacts with other numbers) I am having a hard time understanding what its existence amounts to.

Most importantly: How do you know they exist? Is there any substance to such knowledge; or is it just a metaphysical commitment?

More generally, there exist nonempty sets of mathematical objects -- we can prove their existence -- for which it is not possible to construct a witness.

That largely depends on what you think "proof of existence" amounts to.

To repeat myself:How do you know they exist? Is there any substance to such knowledge; or is it just a metaphysical commitment?

This existence seems vacuous at best. Does it have any practical implications? What if these objects didn't exist? What would be different about the way we use Mathematics?

If mathematics with uncomputable numbers works identically to mathematics without them, what work is the existence claim doing?

So, I decisively and resolutely refuse to overrule the default of classical mathematics. It is not just cultural momentum. I do not want to switch to constructivism because I consider it to be often unreasonable. It is a deliberate choice and not just a default.

But what about the default choice as to what existence (and proof thereof) means?

What about the default choice as to what "reasonable" (and unreasonable) mean?

Now imagine mathematical "existence" were tied to mathematical practice rather than metaphysics.

[godelian]

Since you can't express a witness; can you at least express how you know that uncomputable numbers exist?
Given that you can't tell me absolutely anything about an uncomputable number (not even how it interacts with other numbers) I am having a hard time understanding what its existence amounts to.
Most importantly: How do you know they exist? Is there any substance to such knowledge; or is it just a metaphysical commitment?

It is provable:

ChatGPT: there exist nonempty sets of mathematical objects -- we can prove their existence -- for which it is not possible to construct a witness. Give me an example.

A classic example of a nonempty set of mathematical objects for which we can prove existence without being able to construct a witness comes from classical logic and non-constructive proofs in analysis or set theory. One famous example:

Example: A Real Number That Is Not Computable

Let’s define the set:

S={x∈R∣x is not computable}

Claim: The set S is nonempty, and in fact uncountable.
Why we know it exists:

The set of computable real numbers is countable (since there are only countably many Turing machines).
The set of all real numbers is uncountable.
Therefore, the set of non-computable real numbers is uncountable (by cardinality argument).

Why we cannot construct a witness:
To construct a real number is to give a finite procedure (e.g., algorithm) to compute it to arbitrary precision — in other words, to make it computable.
Hence, by definition, any number we can construct is computable.
Thus, we can prove that noncomputable numbers exist, but we cannot explicitly name or construct any one of them.

This is a canonical example of a set:
Proven to be nonempty (even large!),
Yet no individual element (witness) can be constructed.

ChatGPT just spat out the classical argument. It is perfectly satisfactory to me. I consider it even to be highly intuitive. It is exactly how I see things.

This existence seems vacuous at best. Does it have any practical implications? What if these objects didn't exist? What would be different about the way we use Mathematics? If mathematics with uncomputable numbers works identically to mathematics without them, what work is the existence claim doing?

The uncomputable numbers impact the computable ones in very subtle ways. For example, a true statement in the standard model of arithmetic becomes unprovable because in some nonstandard model the statement turns out to be false. These nonstandard models are replete with uncomputable numbers:

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.

It is indeed a bit metaphysical that uncomputable nonstandard numbers subtly influence the standard model of arithmetic. Mathematics without uncomputable numbers would need to remove the distortions caused by these uncomputable numbers. The standard model of arithmetic would not remain the same. One immediate effect would be:

ChatGPT: If there were no nonstandard models of arithmetic, what would be the immediate impact on the standard model?

This would mean that:
The first-order theory of arithmetic (PA) is categorical—it has only one model up to isomorphism.
This is impossible under first-order logic, so something major would have to change:
First-order logic would have to be replaced (e.g., by second-order logic with full semantics).
Or the Compactness and Löwenheim-Skolem theorems would fail.
Or PA would somehow become syntactically complete, which it is not due to Gödel's incompleteness theorem.
So, if no nonstandard models existed, it would imply a collapse or change in foundational logical theorems. There would be massive changes in logic and model theory—we would lose core theorems of first-order logic or have to shift to stronger logics.

This would just be the immediate impact. There would also be downstream knock-on effects. It is difficult to imagine what exactly would happen without actually making the change. In my intuition, lots of algorithms would start breaking all over the place. These uncomputable numbers keep hidden structures in place without which mathematics would no longer be what it is today.

[Skepdick]

Since you can't express a witness; can you at least express how you know that uncomputable numbers exist?
Given that you can't tell me absolutely anything about an uncomputable number (not even how it interacts with other numbers) I am having a hard time understanding what its existence amounts to.
Most importantly: How do you know they exist? Is there any substance to such knowledge; or is it just a metaphysical commitment?

It is provable:

ChatGPT: there exist nonempty sets of mathematical objects -- we can prove their existence -- for which it is not possible to construct a witness. Give me an example.

A classic example of a nonempty set of mathematical objects for which we can prove existence without being able to construct a witness comes from classical logic and non-constructive proofs in analysis or set theory. One famous example:

Example: A Real Number That Is Not Computable

Let’s define the set:

S={x∈R∣x is not computable}

Claim: The set S is nonempty

But that's just as vacuous as every Classical claim. Give me just one element in S.

Give me a single Real number which cannot be encoded on a Turing machine.

If you cannot present such a counter-example then you cannot insist that there is NO bijection between Real numbers and TMs; and you cannot insist that S exists.

Why we know it exists:
The set of computable real numbers is countable (since there are only countably many Turing machines).
The set of all real numbers is uncountable.
Therefore, the set of non-computable real numbers is uncountable (by cardinality argument).

This is simply a non-starter. There exists NO real number which cannot be represented/encoded as decimal expansion on the tape of a Turing machine. The Turing machine doesn't have to generate the digits of the number.
The number is already encoded on the tape as the TM's initial state.
The TM (in turn) either does nothing; or shifts right forever.

Since there exists NO real number that cannot be written down on an infinite piece of paper (such as the tape of a TM) then there exists a bijection. between Real numbers and Turing Machines.

If the reals are countable then so are TMs.
If the reals are uncountable then so are TMs.

But it cannot be that one is countable and one is uncountable; for this contradicts the bijection.

You cannot have a bijection between sets of different cardinalities.

The uncomputable numbers impact the computable ones in very subtle ways. For example, a true statement in the standard model of arithmetic becomes unprovable because in some nonstandard model the statement turns out to be false. These nonstandard models are replete with uncomputable numbers:

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.

It is indeed a bit metaphysical that uncomputable nonstandard numbers subtly influence the standard model of arithmetic. Mathematics without uncomputable numbers would need to remove the distortions caused by these uncomputable numbers. The standard model of arithmetic would not remain the same. One immediate effect would be:

ChatGPT: If there were no nonstandard models of arithmetic, what would be the immediate impact on the standard model?

This would mean that:
The first-order theory of arithmetic (PA) is categorical—it has only one model up to isomorphism.
This is impossible under first-order logic, so something major would have to change:
First-order logic would have to be replaced (e.g., by second-order logic with full semantics).
Or the Compactness and Löwenheim-Skolem theorems would fail.
Or PA would somehow become syntactically complete, which it is not due to Gödel's incompleteness theorem.
So, if no nonstandard models existed, it would imply a collapse or change in foundational logical theorems. There would be massive changes in logic and model theory—we would lose core theorems of first-order logic or have to shift to stronger logics.

This would just be the immediate impact. There would also be downstream knock-on effects. It is difficult to imagine what exactly would happen without actually making the change. In my intuition, lots of algorithms would start breaking all over the place. These uncomputable numbers keep hidden structures in place without which mathematics would no longer be what it is today.

But if the uncomputable numbers don't actually exist this renders your axiom "S is non-empty" as false.

Ex falso quodlibet *BOOM* you can prove anything.

Well what if Cantor's Diagonal argument was itself weaponized against Classical Mathematics?
Diagonalization (itself an infinitary process) is said to produce a unique real, so then perform diagonalization again; and again; and again... ad infinitum.

An "uncomputable real" would have to be something that cannot be produced even by infinite iterations of the very process that classical mathematics uses to prove their existence.