12

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?$"

Vladimir Reshetnikov
  • 6,709
  • 9
    @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. – Philip Welch Jun 11 '14 at 05:58
  • 5
    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). – Piotr Shatalin Jun 11 '14 at 06:09
  • 3
    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$. – Emil Jeřábek Jun 11 '14 at 11:25
  • 2
    @PhilipWelch I would suggest that your comment should be an answer. – Joel David Hamkins Jun 11 '14 at 13:18
  • 1
    If you take for $\Phi$ a false statement, then the axiom simply states that $T$ is consistent. So, actually there is no need for a schema of axioms, one is enough. – Alex Gavrilov Jun 11 '14 at 14:59
  • 6
    Note that your theories $\mathsf{PA}_\alpha$ are not entirely well-defined, as explained in this earlier question. This probably answers Question 1. – François G. Dorais Jun 11 '14 at 15:33
  • 7
    @Alex: I think the OP is expressing a reflection principle or perhaps a soundness property rather than just iterated consistency. – François G. Dorais Jun 11 '14 at 15:40
  • By the way, what is $PA_{\omega}$? I am curious. – Alex Gavrilov Jun 12 '14 at 04:33
  • @AlexGavrilov $\sf PA_\omega$ contains all axioms of all $\sf PA_n$ for $n\in\omega$. So, it asserts that all theorems of $\sf PA$ are true, and if we add this as a new axiom to get $\sf PA_1$, then all its theorems are true, and if we add this as a new axiom to get $\sf PA_2$, then all its theorems are true, and if we repeat this step any finite number of times to get $\sf PA_n$, then all its theorems are also true (this is not a quantified statement, but an axiom schema). It's still a decidable problem to check if a wff is an axiom of $\sf PA_\omega$, so it is recursively axiomatizable. – Vladimir Reshetnikov Jun 12 '14 at 23:04
  • @AlexGavrilov There is a certain difference between the soundness axiom schema and the single axiom of consistency. Imagine a pure formalist (I'm not) who rejects any meaning of mathematical symbols and accepts a statement as a theorem only when a full formal proof is presented. Suppose he formally proved in $\sf PA$ that a certain statement $S$ has a formal proof in $\sf PA$. Because he does not assign any meaning (let alone truth) to what he just proved, he cannot use it as a substitute for a proof of $S$. But if he works in $\sf PA_1$, the soundness schema immediately yields a proof of $S$. – Vladimir Reshetnikov Jun 13 '14 at 00:05

1 Answers1

8

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.

Noah Schweber
  • 18,932
  • Can we get an inconsistent theory on at least one path? – Vladimir Reshetnikov Jun 13 '14 at 00:33
  • 2
    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. – Noah Schweber Jun 13 '14 at 01:36
  • I meant, if we formally assume axioms of $\sf ZFC$, can we prove that all paths yield only consistent theories? – Vladimir Reshetnikov Jun 13 '14 at 01:57
  • 4
    @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 ... – Emil Jeřábek Jun 13 '14 at 09:43
  • 3
    ... 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 http://www.sciencedirect.com/science/article/pii/0168007295000074 are highly relevant on these matters. – Emil Jeřábek Jun 13 '14 at 09:48
  • Emil, that's nice - I knew $\Sigma^0_1$ soundness was necessary, but I didn't know it was sufficient. – Noah Schweber Jun 13 '14 at 15:01