Take the 2-minute tour ×

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:


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).



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.

share|improve this question
COR looks like some kind of compactness condition to me- a very different beastie from transfinite induction... –  Tom Boardman May 20 '10 at 22:24
Can you clarify the meaning of your constructive omega rule? Your description of it sounds like the plain omega rule. –  François G. Dorais May 20 '10 at 22:58
add comment

2 Answers

The anwer 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 th 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 weakend 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.

share|improve this answer
Thanks for the answer. I added a clarification to my question. I intended to refer to a system that can actually build. In such system it is necessary to prove in the meta-logic that the computable function that generates the PA proof, indeed does do the job. You can have a function that generates a proof for each n, but for which it is not provable that it does. If PA + COR could prove each sentence you suggested, then it could prove its own consistency. This is not possible if the system can be formalized. –  Lucas K. May 21 '10 at 20:37
Lucas, because of Nelson's theorem, mentioned in the article Kristal links to, I don't think this makes a difference. –  Joel David Hamkins May 22 '10 at 2:28
I misunderstand something, or there is some kind of error. It looks to me that you say that PA+COR is complete for sentences in the arithmetic hierarchy ∏0/2. But PA+COR is a formal system that can be implemented, and completeness for ∏0/2 means that there is a procedure for undecidable problems. Since this is based on Nelson's theorem, I doubt if Nelson's theorem is correct. I tried to find the article. Googling on Colloquium Mathematicum gives me a Polish site. But searching on the article does not give results (probably not yet digitalized). So, I have to go to university library. –  Lucas K. May 25 '10 at 21:47
I also have become confused about it, and I don't know Nelson's theorem except what was said about it in that article. Perhaps the resolution will be that the proof in Nelson's system is still an infinite object, the proof tree, but that this tree has primitive recursive behavior on the nodes. Such a system would be different than what you seem to have in mind. I'll give it some more thought. I think your system, if I understand it, is probably very weak. –  Joel David Hamkins May 25 '10 at 21:57
With COR you can unroll some second order induction proofs, that have a first order final theorem. If SO(n) is a second order property of a natural number n, and you have SO(0), SO(n)->SO(n+1) and SO(n)->P(n), where P(n) is a first order property of n, then you can conclude P(n) for all n. The proof is second order, and can not be reduced to first order in general. However, with COR, you can do SO(0)->SO(1), SO(1)->SO(2) ... SO(n-1)->SO(n), SO(n)->P(n). You can do that for every n and reduce each individual proof for n to a first order proof. Problems arise, when nested. But Goodstein? –  Lucas K. May 25 '10 at 22:15
add comment

According to :this article in COR proof trees are limited to those are effective and effectiveness corresponds to primitive recursion. Goodstein's problem cannot be solved with primitive recursion so I don't think it can be solved with COR.

share|improve this answer
Kristal, doesn't the article insist merely on recursive as opposed to primitive recursive proof enumerations for the constructive $\omega$-rule? –  Joel David Hamkins May 21 '10 at 14:10
Yes I went back and looked at the article. In section 2 the restrictions as you say so Goodstein's theorem could be proved. –  Kristal Cantwell May 21 '10 at 16:35
add comment

Your Answer


