# Semi-recursive ω-rule

I thought of the following semi-recursive ω-rule for a sequence of first-order theories $$PA_k$$ that extend $$PA_0 = PA$$:

Semi-recursive ω-rule: For each $$1$$-parameter arithmetical sentence $$Q$$, if (using the usual encoding) $$PA_k \vdash \forall n ( PA_k \vdash Q(n) )$$, then we add $$∀n ( Q(n) )$$ as an axiom of $$PA_{k+1}$$.

$$PA_k$$ clearly has a semi-recursive axiom set for each natural $$k$$, so it has a theorem generator and will still be arithmetically-incomplete by the generalized incompleteness theorems. Anyway if PA is sound then $$PA_k$$ would also be sound. My questions are:

(1) What is the strength of each $$PA_k$$ for natural $$k$$?

(2) What happens if I go further by defining $$PA_ω = \bigcup_{k \in ω} PA_k$$ and carry on iterating all the way up the computable ordinals?

(3) What if we start with ACA instead? In general, what happens to the strength of the system on applying this semi-recursive ω-rule?

Assuming $$PA$$ is sound, I cannot even think of a single sentence that $$PA_1$$ proves that $$PA$$ does not. So I am actually guessing that this rule is completely useless. Can anyone prove that $$PA_1 = PA$$ and $$ACA_1 = ACA$$? If not, does the hierarchy reach a fixed point?

• Note that Craig's trick lets you go from a semirecursive axiomatization to a recursive axiomatization. – Noah Schweber Oct 4 '17 at 20:07
• @NoahSchweber: I'm aware of that trick, but it's doesn't help to answer the question, right? – user21820 Oct 5 '17 at 15:20
• I thought it was worth mentioning given your use of the term "semi-recursive." Also: what do you mean when you say "does not have a proof verifier program"? It's an r.e. theory, the set of its theorems is r.e. – Noah Schweber Oct 5 '17 at 15:31
• @NoahSchweber: Well I just meant that there is no program that decides the validity of a proof of a sentence. Perhaps my use of the word "verifier" is slightly misleading, but I can't think of a better English word. Anyway do you have any idea what this kind of hierarchy gives? I'm curious to know whether the strength of the theory stabilizes at some point, and where that point is. – user21820 Oct 5 '17 at 15:37
• It's a more subtle question than I thought, I like it ! – Xoff Nov 29 '18 at 19:38

Below, all theories are "appropriate" - that is, they are recursively axiomatizable, consistent, and contain PA. Of course this last bit is overkill, but what the hey.

I can't give a full answer, but let me address your question as to whether $$PA=PA_1$$. The answer is no, and indeed the "semirecursive $$\omega$$-rule operator" has no nontrivial fixed points.

The key is the following fact: that PA is internally $$\Sigma_1$$-complete, that is, that PA proves "PA proves every true $$\Sigma_1$$ fact." See e.g. here. And of course this is hereditary upwards - all the theories we consider will share this property too. (Actually, we really only need $$\Delta_0$$-completeness, but meh.)

Internal $$\Sigma_1$$-completeness lets us make the following neat argument. Given an appropriate theory $$S$$, let $$Q_S(x)$$ be the formula "$$x$$ is not (the Godel number of) a proof of a contradiction in $$S$$." Then I claim that we have $$S\vdash\forall x(S\vdash Q_S(x)).$$ Consequently the "next step up" from $$S$$ according to your semi-recursive $$\omega$$-rule is at least (and indeed will wind up being much more than) $$S+Con(S)$$, since "$$\forall x(Q_S(x))$$" is just "$$Con(S)$$."

To see this, we reason inside $$S$$ as follows:

"Fix $$n$$; we need to show that $$S$$ proves '$$n$$ is not (the Godel number of) an $$S$$-proof of a contradiction.' There are two possibilities. Maybe $$n$$ is the Godel number of a proof of a contradiction in $$S$$, in which case $$S$$ is inconsistent and so we have $$S\vdash Q_S(n)$$ trivially. Otherwise, $$n$$ is not the Godel number of a proof of a contradiction in $$S$$, in which case we have $$S\vdash Q_S(n)$$ since 'not-being-a-proof-of' is $$\Sigma_1$$ (indeed, $$\Delta_0$$) and $$S$$ is $$\Sigma_1$$-complete. Either way, it must be the case that $$S\vdash Q_S(n)$$, regardless of $$n$$ - if only for stupid reasons!"

The fact that $$S$$ knows itself to be $$\Sigma_1$$-complete is what lets the "otherwise" case work.

• Thanks a lot! It's the most jolly answer I've read from you. =) So $S_1$ proves $Con(S)$. Does $S_1$ prove $Con(S+Con(S))$? The argument doesn't work.. – user21820 Jan 20 '19 at 15:00
• Hi! Did you get any more ideas regarding my question (and comment)? =) – user21820 Feb 20 '19 at 6:52