The position of constructive mathematics on Goodstein's theorem

[godelian]

Goodstein's theorem is important in classical mathematics because it is an example of Godel's incompleteness theorem:

https://en.m.wikipedia.org/wiki/Goodstein%27s_theorem
In mathematical logic, Goodstein's theorem is a statement about the natural numbers, proved by Reuben Goodstein in 1944, which states that every Goodstein sequence (as defined below) eventually terminates at 0.

Laurence Kirby and Jeff Paris[1] showed that it is unprovable in Peano arithmetic (but it can be proven in stronger systems, such as second-order arithmetic or Zermelo-Fraenkel set theory).

This was the third example of a true statement about natural numbers that is unprovable in Peano arithmetic, after the examples provided by Gödel's incompleteness theorem and Gerhard Gentzen's 1943 direct proof of the unprovability of ε0-induction in Peano arithmetic.

The Paris–Harrington theorem gave another example.

Constructive mathematics does not accept the classical proof:

ChatGPT: What is the position of constructive mathematics on Goodstein's theorem?

Constructive mathematics, particularly in the tradition of intuitionism and constructive logic, generally does not accept the standard proof of Goodstein’s theorem as valid, because that proof relies on principles that are non-constructive—especially transfinite ordinals and classical reasoning about infinite sets.

Summary of the Issue:

Goodstein’s theorem states that every Goodstein sequence eventually terminates at zero, no matter the starting number. However, the standard proof of this theorem, developed by Kirby and Paris, uses transfinite ordinal numbers (specifically, up to ε₀), which are not constructively justified.

Why Constructivists Reject the Proof:

1. Use of non-constructive ordinals: The ordinal ε₀ is a transfinite ordinal whose use requires accepting the law of the excluded middle and completed infinities—both of which are generally rejected in constructive frameworks.

2. Lack of a constructive bound: The proof does not provide a computable or constructive method to determine how long a Goodstein sequence takes to reach zero.

3. Unprovability in Peano Arithmetic (PA): While the theorem is true and provable in stronger classical systems (like second-order arithmetic), it is unprovable in PA, and constructive mathematics is often more restrictive than PA in what it accepts.

Alternative Constructive Approaches:

Some constructive mathematicians have attempted to analyze fragments of the Goodstein sequences or construct alternative, weaker versions of the theorem that are provable without transfinite induction.

Others explore the computational aspects of the sequence (like recursive bounds), but these still fall short of a full constructive proof of termination.

In Summary:

Constructive mathematics does not accept Goodstein’s theorem as proven, at least not in the full generality of the classical result, because the standard proof uses non-constructive methods that are not permitted in constructive logic. It remains a good example of a theorem that is classically true but not constructively provable.

There is a lot of non-constructive proof in classical mathematics, not all of which have a constructive alternative.

In my opinion, it may not always be possible to prove convergence of hyper-exponentially growing sequences by finitistic methods. It looks pretty much pointless to look for a finitary approach to decide the Goodstein problem. Therefore, I deem the infinitary method used in the proof to be an acceptable match for the problem at hand.

I reject the constructive objections to the classical proof and I accept Goodstein’s theorem as proven.

[Skepdick]

I reject the constructive objections to the classical proof and I accept Goodstein’s theorem as proven.

I reject your rejection using Classical reasoning.

Given that a system is defined by a sets of axioms - classically there exists a proper class of all possible axiom-systems, no?

Using the axiom of choice (as applied to the proper class of all possible axiom system) I shall consider only those collections of axioms which imply universes in which Goldstein's statement is either semantically false; or provably doesn't hold.

This is choice (and by Diaconescu - LEM) in action; you see. Either P or not P. I am choosing not-P together with all of its models.

Now, I have no idea what these universes are; but they obviously exist.

[godelian]

Given that a system is defined by a sets of axioms - classically there exists a proper class of all possible axiom-systems, no?

A subset of language sentences is itself a language sentence. So, theories are elements in the set of language sentences. So, they are a countable set. The number of models, however, is not guaranteed to be countable. I do not believe that you can enumerate the class of models.

Using the axiom of choice (as applied to the proper class of all possible axiom system) I shall consider only those collections of axioms which imply universes in which Goldstein's statement is either semantically false; or provably doesn't hold.

This is choice (and by Diaconescu - LEM) in action; you see. Either P or not P. I am choosing not-P together with all of its models.

Now, I have no idea what these universes are; but they obviously exist.

These theories must contain a sufficiently large fragment of ZF or a theory that is bi-interpretable with ZF to support manipulations on hereditary base-n notation.

Goodstein's theorem will therefore already be provable from that fragment alone, irrespective of what other clauses your arbitrary theory contains, unless it manages to axiomatize the negation of Goldstein. It can obviously do that by just mentioning the negation of Goldstein.

But then again, I expect that most theories that contain ZF or similar will simply prove Goldstein. In most theories that contain a sufficiently large fragment of PA, Goodstein will be true.

[Skepdick]

A subset of language sentences is itself a language sentence.

Yeah... that's the nonsense of set theory. Every set has a subset.

Even the set whose only subset is itself.

So it stands to reason that a symbol too is a sentence. Because symbols are subsets of strings of characters (which is what sentences are).

So, theories are elements in the set of language sentences. So, they are a countable set. The number of models, however, is not guaranteed to be countable. I do not believe that you can enumerate the class of models.

I am still waiting for you to count the subset of non-halting Turing Machines.

But then again, I expect that most theories that contain ZF or similar will simply prove Goldstein. In most theories that contain a sufficiently large fragment of PA, Goodstein will be true.

I have no idea how you can guess as to what most theories would; or wouldn't contain.

I'd imagine most theories to be nothing like ZF or PA.

Isn't the space of mathematical theories uncountably infinite; or something? We've only examined a measure-zero portion of the space of all theories.

[godelian]

A subset of language sentences is itself a language sentence.

Yeah... that's the nonsense of set theory. Every set has a subset.
Even the set whose only subset is itself.
So it stands to reason that a symbol too is a sentence. Because symbols are subsets of strings of characters (which is what sentences are).

We do not even need the notion of subset. The concatenation of two or more sentences is a sentence. You may have to use a separator. So, a theory is just one single sentence. Hence, the sentence embodying the entire multi-sentence theory is one single individual element in the set of language sentences.

[Skepdick]

We do not even need the notion of subset.

You don't? OK... lets see...

The concatenation of two or more sentences is a sentence.

Is the concatenation of two (or more) non-sentences a sentence?

You may have to use a separator.

Forget the separators for a moment. Is the concatenation of the strings "2+" and "2=4" a sentence?

Notice we have no separator.

So, a theory is just one single sentence.

Oh. Ok... So what is a collection of sentences? What is a collection of theories?

Hence, the sentence embodying the entire multi-sentence theory is one single individual element in the set of language sentences.

That sounds like something Deepak Chopra would say.

[godelian]

Oh. Ok... So what is a collection of sentences? What is a collection of theories?

A sentence can be mapped onto a natural number by means of an encoding function. You can use a pairing function to map/unmap two or more numbers onto one.

So, a theory is a natural number, which can be paired again. So, a set of theories can be represented as a natural number.

The sentences will have to satisfy a particular EBNF grammar.

[Skepdick]

Oh. Ok... So what is a collection of sentences? What is a collection of theories?

A sentence can be mapped onto a natural number by means of an encoding function. You can use a pairing function to map/unmap two or more numbers onto one.

So, a theory is a natural number, which can be paired again. So, a set of theories can be represented as a natural number.

The sentences will have to satisfy a particular EBNF grammar.

That sounds like a theory.

What natural number have you mapped it to? Can you show me the encoding function?

[godelian]

What natural number have you mapped it to? Can you show me the encoding function?

We are no longer in 1931. So, I am not going to use Gödel's prime factorization system anymore. Instead, I'm going to use plain UTF-8.

So, "hello" becomes in BigDecimal representation "104101108108111":

https://onlinetools.com/utf8/convert-utf8-to-decimal

In fact, the UTF-8 bytestream "hello" is already a natural number, represented by the bytestream 0x68 0x65 0x6c 0x6c 0x6f. What you are seeing on your screen, is the result of vector-based outlining instructions that the TTF stroke generator has painted. So, in digital format, the theory is natively already a natural number. It is the graphical representation/visualization by means of a True Type Font that requires additional effort.

On a computer, all data is already encoded into a natural number. So, why do it again?

[Skepdick]

What natural number have you mapped it to? Can you show me the encoding function?

We are no longer in 1931. So, I am not going to use Gödel's prime factorization system anymore. Instead, I'm going to use plain UTF-8.

So, "hello" becomes in BigDecimal representation "104101108108111":

https://onlinetools.com/utf8/convert-utf8-to-decimal

In fact, the UTF-8 bytestream "hello" is already a natural number, represented by the bytestream 0x68 0x65 0x6c 0x6c 0x6f. What you are seeing on your screen, is the result of vector-based outlining instructions that the TTF stroke generator has painted. So, in digital format, the theory is natively already a natural number. It is the graphical representation/visualization by means of a True Type Font that requires additional effort.

On a computer, all data is already encoded into a natural number. So, why do it again?

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.


From a type-theoretic lens it needs not have any other "meaning" than simply ... a bitstream. A randomly-chosen element of the set of all possible finite binary sequences {0,1}*

[godelian]

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

However, programming languages go out of their way to make this hard to do. Even C tries to discourage you from doing that:

Code: Select all

typedef struct {
    int id;
    float value;
} MyStruct;

MyStruct data = {123, 3.14f};
    unsigned char *byte_array = (unsigned char *)&data;
    size_t size = sizeof(MyStruct);

So, you can destructure MyStruct into a byte array of size long, but even C makes you jump through hoops to achieve this. In other languages, you will typically have to first copy the data into a new container suitable for reinterpretation. Furthermore, the tool may very well try to prevent you from copying data between data structures that it considers to be incompatible.

It's funny because all you really want, is to read an existing memory location without interpretation overhead. You would not have to do anything to achieve this in assembler.

So, about "nothing mandates you to interpret", the answer is: Your compiler or script engine clearly does. In practice, that is certainly something.

It is not so much "an arbitrary choice". It is rather a wall erected by programming-language ideological structuralism. What you want to do, is typically considered to be an offense against the political manifesto of the programming language party.

If you ever argued in one of their forums that "you simply want to do this", they will go to great lengths to convince you that "you should not even desire to do this". They will insist on protecting you against yourself, for your own good.

[Skepdick]

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

However, programming languages go out of their way to make this hard to do. Even C tries to discourage you from doing that:

Code: Select all

typedef struct {
    int id;
    float value;
} MyStruct;

MyStruct data = {123, 3.14f};
    unsigned char *byte_array = (unsigned char *)&data;
    size_t size = sizeof(MyStruct);

So, you can destructure MyStruct into a byte array of size long, but even C makes you jump through hoops to achieve this. In other languages, you will typically have to first copy the data into a new container suitable for reinterpretation. Furthermore, the tool may very well try to prevent you from copying data between data structures that it considers to be incompatible.

It's funny because all you really want, is to read an existing memory location without interpretation overhead. You would not have to do anything to achieve this in assembler.

So, about "nothing mandates you to interpret", the answer is: Your compiler or script engine clearly does. In practice, that is certainly something.

It is not so much "an arbitrary choice". It is rather a wall erected by programming-language ideological structuralism. What you want to do, is typically considered to be an offense against the political manifesto of the programming language party.

If you ever argued in one of their forums that "you simply want to do this", they will go to great lengths to convince you that "you should not even desire to do this". They will insist on protecting you against yourself, for your own good.

So use a void pointer.

Code: Select all

MyStruct data = {123, 3.14f};
void *ptr = &data;

Point anything to any object in memory and you have full control over meaning/interpretation of the raw data.
You've side-stepped the type-checker but so what? Most languages provide both safety rails and escape hatches.

Use as needed knowing precisely the sort of hell you are signing up for.

[godelian]

So use a void pointer.

Yes, agreed, a void pointer is also compatible with anything, but only because the C language allows that kind of things.

[Skepdick]

Yes, agreed, a void pointer is also compatible with anything, but only because the C language allows that kind of things.

Well, yeah. Most systems programming languages let you do that.

Rust, Go, Zig, Nim. Even higher-level languages with strong type systems like Haskell and OCaml provide escape hatches like unsafeCoerce and Obj.magic. In scripting languages; or any language with File IO you can always read/write directly from/to /dev/mem and /dev/kmem.

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

[godelian]

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:

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.