4 ms·

Goodstein's theorem comes with a function on the natural numbers. Whether we can prove that the function works correctly, and indeed whether we can implement th

Goodstein's theorem comes with a function on the natural numbers. Whether we can prove that the function works correctly, and indeed whether we can implement the function, depends on how big we allow infinities to be. https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Sequence_length_as_a_function_of_the_starting_value https://en.wikipedia.org/wiki/Goodstein%27s_theorem#Sequence...

btilly 5y ago
Sorry, that isn't what that link says. We can implement the function on a Turing machine. Whether we can prove that the function winds up being well-defined depends on which axioms we use. But if you allow transfinite induction up to ε0 (see https://en.wikipedia.org/wiki/Epsilon_numbers_(mathematics) https://en.wikipedia.org/wiki/Epsilon_numbers_(mathematics)) we can prove that the function works correctly. And this statement can be made without any reference to the size of any uncountable infinities. (Indeed the argument can even be made constructively, within mathematical systems where everything is countable.)
- myWindoonn 5y ago
  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

Sorry, that isn't what that link says. We can implement the function on a Turing machine. Whether we can prove that the function winds up being well-defined depends on which axioms we use. But if you allow transfinite induction up to ε0 (see https://en.wikipedia.org/wiki/Epsilon_numbers_(mathematics) https://en.wikipedia.org/wiki/Epsilon_numbers_(mathematics)) we can prove that the function works correctly. And this statement can be made without any reference to the size of any uncountable infinities. (Indeed the argument can even be made constructively, within mathematical systems where everything is countable.)

myWindoonn 5y ago
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.