I am trying to understand transfinite induction and Gentzen's theories.
But I was wondering, if there is any connection with the Constructive Omega Rule (COR).
With COR I mean that if you can proof:
φ(x)
for every x in fully axiomatized system defined within your PA + COR system, then you may conclude:
∀ x.φ(x)
My question: Is it possible to prove Goodstein's theorem with PA + COR?
Or in general, has COR the same strength as transfinite induction or is it something entirely different (then I want to understand the difference).
Regards,
Lucas
Given the responses, some clarification of the rule is necessary. The referred article gives a rather good description of the rule I mean.
However, I do mean a rule that can actually be implemented. So, if there is a computable function that generates a PA proof A(n) for each n, then it is necessary to show in the meta-system (PA + COR), that this function terminates for each n.
Only then, the constructive omega rule (at least my variant), as additional inference rule, can be used to conclude ∀ n.A(n) in the PA + COR system.
Some second order proofs, with a first order final theorem can also be proven with first order PA + COR. Since, the Goodstein theorem is a second order proof with first order final theorem, I was curious of it is one of them.
Best Answer
The answer is Yes.
Goodstein's theorem asserts that for every natural number $n$ the Goodstein sequence starting with $n$ eventually terminates. Thus, it can be stated in the form $\forall n\ \exists m\ \varphi(n,m)$, where $\varphi$ has only bounded quantifiers.
I claim that any true statement of this form is provable in PA+COR. To see this, note that for any particular fixed $n$ there is an $m$ such that $\varphi(n,m)$, since the statement was assumed to be true, and so for each $n$ the statement $\exists m\ \varphi(n,m)$ is provable in PA. Furthermore, the map $n\mapsto p_n$, where $p_n$ is the shortest PA proof of $\exists m\ \varphi(n,m)$ is a computable function. According to the article to which Kristal links, this is what is needed in order to deduce by COR that $\forall n\ \exists m\ \varphi(n,m)$, as desired.
As François mentioned in the comments, the way you have described your rule, it sounds more like the ordinary $\omega$-rule. The difference is whether the $\omega$-sequence of proofs of the instances is effective or not. According to the article in Kristal's answer, you find (on page 1) that the sequence of proofs must be given by a computable procedure. For the purpose of Goodstein's theorem, we were able to attain this. But it turns out not to matter, since the article mentions that Shoenfield proved that PA+$\omega$-rule is the same as PA+ recursively restricted $\omega$-rule. The article also mentions that a weakened form with primitive recursive proof enumerations is also complete (Nelsen), since one may use a padding trick to reduce to the computable case.
Edit. You have changed or updated the formal system to insist that the effective enumeration of proofs also be provably total (provable in P+COR). Although this seems like a more severe requirement, I claim it does not change anything, provided that you have the copy proof element mentioned in the context of Nelson's theorem in the article linked to by Kristal. In that article, it is claimed that insisting on primitive recursive enumerations of proofs is fully complete, equivalent to the full $\omega$-rule. The proof evidently uses a padding trick of some kind (and I have not looked at the details). I take this to mean that any statement provable in PA with the full $\omega$-rule is provable in PA+ primitive recursive COR. Since primitive recursive functions are provable total in PA, this would seem to satisfy your additional requirement. Thus, it seems still to be the case that Goodstein's theorem is provable in your version of PA+COR.