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.