(1) Does full second-order arithmetic (Z2) prove soundness and uniform reflection schemas for first-order arithmetic (PA)? That is, do we have for all formulas $\phi$: $$ \underset \phi \forall \; Z2 \vdash \square_{PA} \ulcorner \phi \urcorner \rightarrow \phi $$ and $$ \underset \phi \forall \; Z2 \vdash \forall x: \big ( \square_{PA} \ulcorner \phi(x) \urcorner \rightarrow \phi(x) \big ) $$


(2) What would be a good reference to cite to this effect?

  • $\begingroup$ When you say "All formulas $\phi$", do you mean formulas of PA, or formulas of second-order arithmetic? $\endgroup$ Commented Apr 6, 2014 at 0:41

1 Answer 1


Yes; if $\phi(x)$ is a formula of first-order arithmetic, then $Z_2$ proves $$ (\forall x)[ \Box_{PA}\ulcorner \phi(x)\urcorner \Rightarrow \phi(x) ] $$ (The rest of this answer would go through with $Z_2$ replaced by the subsystem with only $\Pi^1_1$ comprehension, and likely in even weaker subsystems, although that goes beyond the question.)

The argument is sketched as follows:

  • $Z_2$ can construct a truth function $T_1$ for all sentences of first-order arithmetic with parameters in $\mathbb{N}$.

  • $Z_2$ can prove that each axiom of PA is true under this truth function.

  • $Z_2$ can prove that the set of true sentences is closed under the inference rules of PA. In other words $Z_2$ can formalize and prove $\mathbb{N} \vDash \text{PA}$.

  • So $Z_2$ proves, for each $\phi(x)$ in the language of PA, that $$(\forall x)[\Box_{PA}\ulcorner \phi(x)\urcorner \Rightarrow T_1(\ulcorner \phi(x)\urcorner) = 1]$$ (In fact $Z_2$ proves this with a quantifier over codes for PA-formulas $\phi$, but this isn't needed for the argument at hand.)

  • For each particular formula $\phi$ of PA, $Z_2$ proves $$(\forall x)[ T_1(\ulcorner \phi(x)\urcorner) = 1 \Rightarrow \phi(x)].$$ The proof is by induction on the structure of $\phi$ using the truth definition that was used to define $T_1$.

  • The rest of the proof is immediate.

As for a reference, this is nothing deep, it is just an exercise. I don't know whether it is mentioned anywhere in the literature, but the techniques are all standard.

  • $\begingroup$ Thanks, Carl! I don't suppose you'd happen to have a reference for $Z_2$ being able to construct a truth function between PA-sentences and $\mathbb N$? If not, it's good enough for me to know that Z2 does in fact prove uniform reflection over PA. Thank you for the $\Pi^1_1$ reference, that gets me a bit closer to knowing the minimal second-order subsystem that will do it, which isn't a critical fact in context but is one that I was curious about. $\endgroup$ Commented Apr 9, 2014 at 2:41
  • $\begingroup$ The truth set for sentences of first-order PA is definable by a $\Pi^1_1$ formula, by just writing out all the Tarski conditions. Actually the truth set is a $\Delta^1_1$ set. So you just write down the correct formula and apply comprehension to get the truth function - there is nothing deep to it. $\endgroup$ Commented Apr 9, 2014 at 2:51

You must log in to answer this question.

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