# 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. – Lucas K. Jan 10 '16 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)$? – Noah Schweber Jan 10 '16 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 – Thomas Benjamin Jan 10 '16 at 9:39
• (cont.) $\mathrm Q$ using an $\omega$-rule is important.) – Thomas Benjamin Jan 10 '16 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$? – Noah Schweber Jan 10 '16 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. – Lucas K. Jan 10 '16 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$. – Lucas K. Jan 10 '16 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. – Lucas K. Jan 10 '16 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. – Thomas Benjamin Jan 10 '16 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. – Thomas Benjamin Jan 10 '16 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. – Lucas K. Jan 11 '16 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? – Thomas Benjamin Jan 11 '16 at 22:37