7
$\begingroup$

Recall that the omega-rule is an infinitary rule of inference that allows one to deduce $\forall x A(x)$ from $A(0), A(1), \dots$. It's known that adjoining PA (or even Q) with the omega-rule results in a complete theory (true arithmetic). I'm curious what happens to stronger theories when we allow the omega-rule as the sole infinitary rule of inference (and all the axioms must be recursively enumerable, as I will hereafter assume). For example, can there be a complete theory of analysis or set theory if we allow ourselves the omega-rule? I suspect the answer is no, but I'm not sure how to prove it.

We can also generalize the omega-rule to allow deducing a universal statement from the set of all true instances of size at most, say, $2^{\aleph_0}$ (so for example, deduce $\forall x \in \mathbb{R} B(x)$ from the $2^{\aleph_0}$ instances of $B(x)$ for each real number $x$). Again, I suspect but cannot prove that there will be a sufficiently strong theory (something stronger than analysis) that must be incomplete even if one allows this generalized omega-rule (and similarly for generalized omega-rules for each cardinality).

$\endgroup$

2 Answers 2

9
$\begingroup$

If $T$ is a recursively axiomatized theory of second-order arithmetic (or set theory) that extends, say, $\mathrm{ACA}_0$, you can define a well-behaved provability predicate $\Pr^\omega_T(x)$ expressing provability in $T^\omega$ (i.e., $T$ extended with the $\omega$-rule) by a $\Pi^1_1$ formula. It is then not particularly difficult to check in $T^\omega$ that this predicate obeys the usual Hilbert–Bernays–Löb derivability conditions, and therefore $T^\omega$ is subject to Gödel’s second incompleteness theorem (and Löb’s theorem): if $T^\omega$ is consistent, then $T^\omega\nvdash\neg\Pr^\omega_T(\bot)$. See Boolos, The Logic of Provability.

$\endgroup$
4
  • $\begingroup$ Thanks. Do similar phenomena arise when we add the stronger generalizations of the omega-rule to set theories stronger than analysis? And is there any rule analogous to the omega-rule that makes all sentences of analysis provable or refutable? $\endgroup$
    – BPP
    Commented Oct 14, 2020 at 18:16
  • $\begingroup$ I don’t really know, but I suspect that stuff will break in various ways when you move to uncountable analogues of the $\omega$-rule. (In general, $L_{\omega_1,\omega}$, of which the $\omega$-rule can be seen as a special case, is much more well behaved that $L_{\kappa,\omega}$ for $\kappa>\omega_1$.) $\endgroup$ Commented Oct 14, 2020 at 18:41
  • $\begingroup$ A related question that's in the spirit of the previous question is, is there a version of the incompleteness theorem for set theory that guarantees an independent sentence for any theory, but with the proviso that this independent sentence has no arithmetic consequences (like CH or AC relative to ZF)? $\endgroup$
    – BPP
    Commented Oct 14, 2020 at 21:11
  • $\begingroup$ Yes, that's exactly it. Where can I read up on the proof of this? $\endgroup$
    – BPP
    Commented Oct 15, 2020 at 1:51
6
$\begingroup$

Footnote to Emil Jeřábek's answer:

(1) Rosser (Journal of Symbolic Logic, 1937) was the first to show that there is a true $\Sigma^1_1$-statement that is unprovable in (second order arithmetic + the $\omega$-rule) with the essentially the same proof outlined by Emil.

(2) In contrast, as shown in a 1961-paper of Grzegorczyk, Mostowski, and Ryll-Nardzewski, every true $\Pi^1_1$-statement is provable in (second order arithmetic + the $\omega$-rule).

I learned the above facts as a graduate student from Barwise' article "The role of the Omitting Types Theorem in infinitary logic" (see p.57), published in Arch. math. Logik 21 (1981),55-68.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .