Peano Arithmetic cannot employ Induction for any ε0 ordering. My question is too easy to be interesting and there is a reason obviously for why it has a negative answer. Can you please provide it for me? Is there no way to build Induction upon the simple ω order that the towers of ε0 represent as written down? E.g. Prove something for the elements of the first ω at the bottom of the tower. Then assume that all elements up to some ω exponent have the same property, and manage (?) to prove that on this assumption all elements up the next exponent have it as well. Is there anything wrong with this approach in principle? This is a follow up after Andrés' illuminating reply. So, if I've got that right, on the assumption that the Church-Turing thesis is true, there must be no algorithm that represents how the Inductive proofs of some level in the tower behave relative to how they behave at the previous level. Otherwise, it would have being possible to assume that all elements up the nth omega level have the property, and, then, by using the algorithm establish the presence of an Inductive proof for all the elements of level n+1. (Proofs for all finite towers of omegas are assumed to be recursive here.) Thank you Andrés, I think I've got it now. One cannot built/code the entire Σ(n) inductive schema within any of the particular instances of it, and therefore nor within an ω exponent.

  • $\begingroup$ Possibly related. $\endgroup$ – Cameron Buie May 30 '18 at 2:16
  • 1
    $\begingroup$ Gentzen showed that PA + induction up to $\epsilon_0$ proves the consistency of PA. Does that constitute an answer to your question or were you aware of that and looking for something different? $\endgroup$ – spaceisdarkgreen May 30 '18 at 2:57
  • 2
    $\begingroup$ What you suggest is quite reasonable. When trying to formalize it to prove concrete statements (such as "every Goodstein sequence terminates") you usually find that the proof at the $n $th level of the tower requires something like a $\Sigma_n $ instance of the induction schema, so that the whole process is not quite formalizable in PA. $\endgroup$ – Andrés E. Caicedo May 30 '18 at 10:43
  • 1
    $\begingroup$ I think it may be benefitial to work in detail through a concrete example to see how the problem manifests. If you haven't, I suggest you read the Kirby-Paris paper to see this in action (model-theoretically). For a proof-theoretic approach, take a look at some of the papers in the AMS Contemporary Mathematics volume on "Logic and combinatorics". $\endgroup$ – Andrés E. Caicedo May 31 '18 at 2:30
  • 1
    $\begingroup$ No, it is not necessary. But my paper relies on some proof-theoretic results, so it is not self-contained. $\endgroup$ – Andrés E. Caicedo Jun 6 '18 at 12:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.