# Can the omega-rule rescue Hilbert's program?

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.

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

• Noah, thanks for the answer, but I think that was not what I intended, and also not what Hilbert intended (see article). I edited the question, to make this more clear. You have to take the $\forall$ within the PA proof. With that I can perfectly make a verification program for this system. Jan 10, 2016 at 8:44
• @LucasK. I must be misunderstanding something about your $\omega_{PA}$-rule. Note that $PA$ proves, for each $n$, that ($PA$ does not prove $\perp$ in ($\le n$)-many steps). Doesn't your $\omega_{PA}$-rule immediately transform this into a proof $PA+\omega_{PA}\vdash Con(PA)$? Jan 10, 2016 at 9:06
• @NoahSchweber: Suppose one limits ones self to Robinson arithmetic $\mathrm Q$, and to $\omega^2$ applications of the primitive recursive $\omega$-rule. Could one derive True Arithmetic from $\mathrm Q$ then (note that on pg. 51 of his textbook Mathematical Logic he gives a finitary proof of the consistency of $\mathrm Q$ so that deriving True Arithmetic from $\mathrm Q$ preserves consistency)? (See Bernd Buldt's paper, "The Scope of Goedel's First Incompleteness Theorem", section 3.4.2, on "Inconsistent Arithmetic" to see why the preservation of truth when deriving True Arithmetic from Jan 10, 2016 at 9:39
• (cont.) $\mathrm Q$ using an $\omega$-rule is important.) Jan 10, 2016 at 9:40
• @LucasK. I don't understand what you mean by "as inference rule" as opposed to "as axiom scheme" - in my argument, I used it as an inference rule. We have infinitely many PA-sequents of the form $PA\vdash \varphi(n)$, and the $\omega_{PA}$-rule allows us to deduce from these sequents the sequent $PA+\omega_{PA}\vdash \forall x\varphi(x)$ (fine, this isn't a sequent since $\omega_{PA}$ isn't first-order; call it a pseudosequent). Can you clarify, please, what the $\omega_{PA}$-rule does? In particular, can you give an example of something provable in $PA+\omega_{PA}$ but not $PA$? Jan 10, 2016 at 11:39

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

• Henry, thanks for the answer, but this was not what I intended and also not what Hilbert intended (see article). I edited the question to make my notation more clear. You have to take the $\forall$ within the PA proof. Then, there is no guarantee that PA is capable of proving it. However, with the $\omega\text{-rule}_{PA}$ you can simulate second order proofs and that might make it possible to prove transfinite induction. Jan 10, 2016 at 8:50
• If you follow the definition after my edit you can make a paradoxical sentence $p$, with $p = \lceil L \vdash p \rceil \rightarrow \bot$. This is tricky because the sentence must end up as the $p$ used within the sentence. This is similar in making a program that prints its own source code. $L$ can prove $p$ and from there can prove $\bot$. Jan 10, 2016 at 8:55

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.

• Thanks for your answer, I will take a look at it. However, it is not my intention to make a system that can prove its own consistency, that is not possible due to G2. But the $\omega\text {-rule}_{AP}$ might strengthen $PA$ (without the rule) beyond $Con (PA)$. At least there are good arguments to give that with the rule certain second order proofs can be made. I don't to which extend. Jan 10, 2016 at 17:55
• @LucasK. It does. $PA$+$\omega$-rule (since $PA$ is an extension of $\mathrm Q$)= True Arithmetic. See Buldt's Proposition 3.5. His Lemma 3.6 might be of real use to you in your research on this question. Jan 10, 2016 at 21:47
• @LucasK.: Here is Buldt's Lemma 3.6 (and proof): "Lemma 3.6. (For all $n$$\in$$\mathbb N$) $\mathscr F^{\omega}_n$ is $\Pi_{2n}$- and $\Sigma_{2n}$-complete. Proof: The induction basis comes for free ($\Delta_0$-completeness). In the induction step, remove the two outermost quantifiers and employ the induction hypothesis. $\exists$-introduction and the $\omega$-rule then prove the result." Since you say $PA$ is a conservative extension of $\Pi_2$, $\Pi_2$-completeness might be useful in proving the results you wanted. Jan 10, 2016 at 23:48
• I think we still don't understand each other. The system proposed is a system for which a verification program can be made. That can never lead to True Arithmetic, because of G1. This discussion and misunderstanding is also in the referenced article, page 8 on the bottom and page 9 in particular. Still, I will take a look at Buldt. Jan 11, 2016 at 21:36
• LukasK: $\mathcal F^{\Omega}$= $\mathcal F^{\omega}_{\omega^2}$=True Arithmetic. What I understand you proposing is a single application of the $\omega$-rule--this gets you $\Pi_{2n}$-completeness by Lemma 3.6. If $\mathcal F$=$PA$ then is $\mathcal F^{\omega}$ (that is, the $\Pi_2$-complete fragment) the fragment of $PA$ you want? Jan 11, 2016 at 22:37