Let $\sf PA$ denote the theory of natural numbers with constants $(0, 1)$ and binary operators $(+,\times)$ based on the first-order predicate calculus with equality, having the following axioms, where the last one is the axiom schema of induction yielding an axiom for each wff $\Phi(a)$:

  • $a+0=a$
  • $a\times1=a$
  • $a+(b+c)=(a+b)+c$
  • $a\times(b+c)=a\times b+a\times c$
  • $a+c=b+c\implies a=b$
  • $a+1\ne0$
  • $\forall a\,\left(\Phi(a)\implies\Phi(a+1)\right)\implies\left(\Phi(0)\implies\Phi(c)\right)$

Note that $\sf PA$ is powerful enough to introduce Gödel numbering for its own formulae and define the predicate for their provability in $\sf PA$.

Let's use $\sf ZFC$ as a meta-theory to reason about $\sf PA$ and its extensions defined below, and furthermore assume $\sf ZFC$ is consistent.

For any recursively axiomatizable theory $\sf T$, that contains $\sf PA$ as its fragment, define $\sf T^+$ to be a new theory obtained from $\sf T$ by adjoining the following axiom schema yielding an axiom for each wff $\Phi$:

  • $\left(\Phi\ \text{is provable in}\ \sf T\right)\implies\Phi$

Note that $\sf T^+$ can prove consistency of $\sf T$, thus, if $\sf T$ is consistent, $\sf T^+$ is stronger than $\sf T$.

Let $\alpha$ range over recursive ordinals, i.e. $\alpha\in\omega_1^{CK}$. Define the countable transfinite sequence of theories $\sf PA_\alpha$ such that:

  • $\sf PA_0$ is $\sf PA$
  • $\sf PA_{\alpha+1}$ is $\sf PA_\alpha^+$
  • for a limit ordinal $\alpha$, $\sf PA_\alpha$ is the theory whose set of axioms is the union of sets of axioms of all $\sf PA_\beta$, where $\beta<\alpha$

Apparently, each of $\sf PA_\alpha$ is recursively axiomatizable. I also believe each of them is consistent, but do not yet see how to prove it.

Question 1: Can we prove it?

Question 2: Does any of $\sf PA_\alpha$ contain a theorem that is not provable in $\sf ZFC$ (when properly translated to the language of set theory, with natural numbers represented as finite von Neumann ordinals, and operators $(+,\times)$ as ordinal addition and multiplication)? If so, what's the least $\alpha$ with this property?

Update: As pointed out in the comments below, my "definition" of the transfinite sequence $\sf PA_\alpha$ is not really a definition because we have some wiggle room in choosing a specific ordinal notation at limit points (I do not yet completely understand how exactly it can affect the strength of theories in the sequence, but I've started to read a book on this topic — Thanks!). But I believe we still can define the set $\mathcal T$ of all possible transfinite sequences constructed this way (although it is not a singleton set). So, each of my questions can be restated as "Is it the case for at least one sequence in $\mathcal T?$ Is it the case for all sequences in $\mathcal T?$"

  • 9
    $\begingroup$ @Vladimir There is a whole literature on this kind of thing, initiated by Turing and carried on by Feferman. A huge amount of care is needed to get this formalised correctly. A good place to start looking is T. Franzen "Inexhaustibility", ASL Lecture Notes in Logic, vol.16. $\endgroup$ Jun 11 '14 at 5:58
  • 5
    $\begingroup$ There could be nothing wrong with saying that everything $PA$ proves is true. This is what most mathematicians believe anyway. But, of course, $PA$ itself cannot prove it, because it implies its consistency (something that a consistent theory cannot prove about itself). $\endgroup$ Jun 11 '14 at 6:09
  • 3
    $\begingroup$ You got the axioms wrong: the theory you described has a one-point model, and as such it is much weaker than PA. You need to replace the last but one axiom with $a+1\ne0$. $\endgroup$ Jun 11 '14 at 11:25
  • 6
    $\begingroup$ Note that your theories $\mathsf{PA}_\alpha$ are not entirely well-defined, as explained in this earlier question. This probably answers Question 1. $\endgroup$ Jun 11 '14 at 15:33
  • 7
    $\begingroup$ @Alex: I think the OP is expressing a reflection principle or perhaps a soundness property rather than just iterated consistency. $\endgroup$ Jun 11 '14 at 15:40

A stark demonstration of why precisely defining how you form $PA_{\lambda +1}$ for $\lambda$ a limit ordinal: in 1939 Turing showed that if $\varphi$ is a true $\Pi^0_1$ statement, there is a notation for $\omega+1$ according to which $PA_{\omega+1}$ proves $\varphi$.

Less pathologically, I believe (although I can't at present find a reference) that there are "nice" paths through Kleene's $\mathcal{O}$ such that the corresponding sequence of theories gotten by adding successive consistency assumptions (so, in particular, weaker than your theories) proves every true $\Pi^0_1$ sentence; so in particular, one of them proves a $\Pi^0_1$ sentence not provable from ZFC.

On the other hand, Spector and Feferman (http://www.jstor.org/stable/2964544) showed that there are paths through $\mathcal{O}$ which don't give you every true $\Pi^0_1$ sentence. I don't know whether their arguments or others let you control which $\Pi^0_1$ sentences you do get, or whether they extend to your theories, but in principle there could be a path along which you didn't get $\Pi^0_1$ sentences which ZFC doesn't prove. This seems extremely unlikely, though.

  • $\begingroup$ Can we get an inconsistent theory on at least one path? $\endgroup$ Jun 13 '14 at 0:33
  • 2
    $\begingroup$ Certainly not if $PA$ is true; I'm sure there's a weaker and less-Platonist criterion guaranteeing that all paths yield consistent theories, but I don't know one off the top of my head. $\endgroup$ Jun 13 '14 at 1:36
  • $\begingroup$ I meant, if we formally assume axioms of $\sf ZFC$, can we prove that all paths yield only consistent theories? $\endgroup$ Jun 13 '14 at 1:57
  • 4
    $\begingroup$ @VladimirReshetnikov: Yes. @ NoahS: (Assuming something like PA as a metatheory.) As every true $\Pi^0_1$ sentence is provable along some path, this obviously implies that PA is $\Sigma^0_1$-sound. Less obviously, the converse also holds. For iterated local reflection principle, this follows easily enough from an exercise in provability logic showing that if $T+\mathrm{Rfn}_T$ proves a $\Sigma^0_1$-sentence $\phi$, then $T$ proves $\Box^n_T\phi$ for some $n$. For iterated uniform reflection principles, one needs the “fine-structure theorem” by Schmerl, which basically says that iterating ... $\endgroup$ Jun 13 '14 at 9:43
  • 3
    $\begingroup$ ... the uniform reflection principle along an ordinal is, wrt $\Pi^0_1$ consequences, equivalent to iterating consistency along a suitably longer ordinal. Beklemishev’s papers such as sciencedirect.com/science/article/pii/0168007295000074 are highly relevant on these matters. $\endgroup$ Jun 13 '14 at 9:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.