Can the omega-rule rescue Hilbert's program?

Question

As known the second incompleteness theorem derailed Hilbert's program.

However, Hilbert himself tried to rescue it with the $\omega \text{-rule}$, according to the following paper:

http://repository.cmu.edu/cgi/viewcontent.cgi?article=1522&context=philosophy

The $\omega \text{-rule}$ says that if:

$$ \vdash \phi(c) $$ for every constant $c$ can be proven then the following theorem can be added: $$ \vdash \forall x: \phi(x) $$ Important is to define in which system the prove is given. To improve the notation, I think it is best to add the system as subscript. So, $\omega \text{-rule}_{PA}$ means that the proof must be given in $PA$, which stands for First Order Logic + Peano Axioms.

EDIT Given the answers the notation and the Hilbert's intend was not clear yet. If: $$ K = L + \omega\text{-rule}_M $$ Then $K$ and $L$ are two logics with the same syntax and sentences, but $M$ not necessarily. If: $$ M \vdash \forall x : \lceil L \vdash \phi (x) \rceil $$

Where the $x$ within $\lceil$ and $\rceil$ is expanded to $0, S(0), S(S(0))$, depended on the value of x, then:

$$ K \vdash \forall x: \phi(x) $$

END EDIT

I have a little bit trouble in following the mentioned paper, there are a lot of notations. My question is whether the second incompleteness theorem makes the following impossible: $$ PA + \omega\text{-rule}_{PA}\vdash Con(PA) $$ I was convinced that this was not possible due to the following reasoning. If: $$ PA + \omega\text{-rule}_{PA}\vdash\perp $$ then the proof of that could easily be reduced to a proof of: $$ PA \vdash \perp $$ In such way that this is provable in $PA$. From that you have proven in $PA$ the relative consistency of $PA$ and $PA + \omega\text{-rule}_{PA}$. With that it would follow that $PA + \omega\text{-rule}_{PA}$ can prove its own consistency and then $PA$ could prove its own consistency.

However, I am not so sure anymore that the a proof of $\perp$ using the $\omega\text{-rule}_{PA}$ can easily be reduced to a $PA$ proof. If the result of $\omega\text{-rule}_{PA}$ is used in an induction hypothesis, then things get complicated.

I am now trying to prove $PA + \omega\text{-rule}_{PA}\vdash Con(PA)$ using Gentzen and don't see an obstacle yet, but these kind of proofs need a lot of care and I am not that far yet.

I also want to mention that the $\omega\text{-rule}$ will always a rule separate of all the other axioms and inference rules. If a system $L$ is created such that: $$ L = PA + \omega\text{-rule}_L $$ then the system $L$ is inconsistent. This is already the case with the reflection rule which is a special case of the $\omega\text{-rule}$.

Furthermore, the article uses $PRA$, but I consider that too restrictive. I prefer the $\Pi_2$ fragment of $PA$. And since it is believed that $PA$ is a conservative extension of this fragment, $PA$ in total can be used.

Answer 1

Addressing your issue with Godel: note that even the one-use $\omega$-rule is not computable. There's no obstacle to a non-recursive theory being complete.

---

Actually this is a bit more subtle than I'm giving it credit for, but the point still holds. Using your restricted $\omega$-rule, we do have finitary-ish proof objects: e.g. a proof of $PA+\omega_{PA}\vdash \forall x\varphi(x)$ is a Turing machine $\Phi_e$ such that for all $n$, $\Phi_e(n)$ is a $PA$-proof of $\varphi(n)$. In this sense, a proof is a finite object. However, telling whether $\Phi_e$ has this property is not computable! That is, proof-verification is non-effective.

Note that things get even worse once we allow more $\omega$-ruliness . . .

Answer 2

$PA+\omega$-rule certainly proves $Con(PA)$. If $Con(PA)$ is false, PA proves everything. If $Con(PA)$ is true, this is a $\Pi^0_1$-statement, and $PA+\omega$-rule proves every true $\Pi^0_1$-statement (for each $n$, take the proof in $PA$ that $n$ does not encode a proof of $\bot$ in $PA$, and apply the $\omega$-rule to these proofs).

Your subscript seems to imply that you're only allowing a single use of the $\omega$-rule (that is, that you don't allow the $\omega$-rule to be used in the proofs justifying other uses of the $\omega$-rule). However not that $PA$ together with the full $\omega$-rule gives true statements in $\mathbb{N}$, by a straightforward induction on the complexity of the formula.

However $PA+\omega$-rule is conservative over $PA$ for $\Sigma_1$ statements, including $\bot$. This is shown by Schutte in his infinitary proof of cut-elimination for PA.

I don't understand your last two comments at all; $PA+\omega$-rule (the usual $\omega$-rule, not one with restricted premises) satisfies $L=PA+\omega_L$, and is $\Sigma_1$ conservative over $PA$, so not inconsistent.

Answer 3

Note: In Buldt's paper "The Scope of Goedel's First Incompletness Theorem" (find it under title on the web), he has the following statement (in Section 3.3):

"When we enter the (small) transfinite, we achieve closure, though, which precisely at $\omega^2$, viz., $\mathcal F^{\Omega}$=$\mathcal F^{\omega}_{\omega^2}$ [where $\mathcal F$ is a semi-formal theory extending $\mathrm Q$, $\mathcal F^{\Omega}$ is its closure under the $\omega$-rule, and $\mathcal F^{\omega}_{\alpha}$ is the same theory under $\alpha$ applications of the $\omega$-rule--my comment]. We should mention that $G2$ [the Second Incompleteness Theorem--my comment] still applies, for $\mathcal F^{\Omega}$ [=True Arithmetic--my comment] cannot formally prove its own consistency, which is now a $\Sigma^1_1$-sentence."

So apparently $G2$ keeps reappearing, even with closure under the $\omega$-rule.