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.

constructiveomega rule? Your description of it sounds like the plain omega rule. $\endgroup$ – François G. Dorais♦ May 20 '10 at 22:58