4 ms·

Proof-theoretic ordinal ε₀ isn't sufficient to prove Goodstein's theorem; the entire point is that PA has ε₀ as proof-theoretic ordinal and yet is not able to p

Proof-theoretic ordinal ε₀ isn't sufficient to prove Goodstein's theorem; the entire point is that PA has ε₀ as proof-theoretic ordinal and yet is not able to prove it. The better point to make in the context of the parent comment is that ω is the first of many transfinite numbers; our ability to talk about multiple numbers "above infinity" is intimately related to the set theory which underlies Cantor's theorems. Infinities aren't just about some sort of mathematical game, but directly influence what we can define and describe.

btilly 5y ago
The link I gave begs to differ: The smallest epsilon number ε0 appears in many induction proofs, because for many purposes, transfinite induction is only required up to ε0 (as in Gentzen's consistency proof and the proof of Goodstein's theorem). If you trace through the sketch of the proof of Goodstein's theorem at https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Proof_of_Goodstein's_theorem https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Proof_of... you can see for yourself that transfinite induction up to ε₀ is indeed sufficient. As for the rest of your comment, I'm able to talk classical mathematics but my sympathies are firmly Constructivist. So yes, I really do see most discussion of infinities as part of an explicitly meaningless mathematical game known as Formalism.
- myWindoonn 5y ago
  You really don't want to try a Wikipedia slap-fight with me. From my original link, at the very top of the page, in the first paragraph: > 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 eventually terminates at 0. Kirby and Paris[1] showed that it is unprovable in Peano arithmetic (but it can be proven in stronger systems, such as second-order arithmetic). Despite PA having such a big proof-theoretic ordinal, PA cannot prove Goodstein's theorem. We need SOL. Also, as one constructivist to another: Nobody cares la~ Hopefully you know the difference between PA, which describes NNOs, and HOL, which is ambient in each topos. Just because some topoi have NNO (just because HOL can host PA) and topoi recognize Goodstein's theorem (because Goodstein's provable in HOL) doesn't imply that all NNOs can witness Goodstein. Indeed, double-check your understanding with the following quirk: In the topos Diff for synthetic differential geometry, the natural numbers are decideable and countable, but the real numbers are not decidable (and in fact prove LEM false!) and uncountable. Due to smoothness requirements, the real numbers are fundamentally different from the natural numbers in Diff. These are two different objects, two different infinities, with two different topologies.

btilly 5y ago

The link I gave begs to differ: The smallest epsilon number ε0 appears in many induction proofs, because for many purposes, transfinite induction is only required up to ε0 (as in Gentzen's consistency proof and the proof of Goodstein's theorem). If you trace through the sketch of the proof of Goodstein's theorem at https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Proof_of_Goodstein's_theorem https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Proof_of... you can see for yourself that transfinite induction up to ε₀ is indeed sufficient. As for the rest of your comment, I'm able to talk classical mathematics but my sympathies are firmly Constructivist. So yes, I really do see most discussion of infinities as part of an explicitly meaningless mathematical game known as Formalism.

myWindoonn 5y ago
You really don't want to try a Wikipedia slap-fight with me. From my original link, at the very top of the page, in the first paragraph: > 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 eventually terminates at 0. Kirby and Paris[1] showed that it is unprovable in Peano arithmetic (but it can be proven in stronger systems, such as second-order arithmetic). Despite PA having such a big proof-theoretic ordinal, PA cannot prove Goodstein's theorem. We need SOL. Also, as one constructivist to another: Nobody cares la~ Hopefully you know the difference between PA, which describes NNOs, and HOL, which is ambient in each topos. Just because some topoi have NNO (just because HOL can host PA) and topoi recognize Goodstein's theorem (because Goodstein's provable in HOL) doesn't imply that all NNOs can witness Goodstein. Indeed, double-check your understanding with the following quirk: In the topos Diff for synthetic differential geometry, the natural numbers are decideable and countable, but the real numbers are not decidable (and in fact prove LEM false!) and uncountable. Due to smoothness requirements, the real numbers are fundamentally different from the natural numbers in Diff. These are two different objects, two different infinities, with two different topologies.