# Can ZFC provide a truth theory for arithmetic, and express arithmetic truth?

Background:

Tarski showed that PA isn't a truth theory for it's own language, i.e. there's no wff $T(x)$ in the language of arithmetic ($L_a$) such that, if $\phi$ is a sentence in $L_a$:

$$PA \vdash \phi \equiv T(\left\ulcorner \phi \right\urcorner)$$

Question 1: Can ZFC do this? That is, is there a wff $T(x)$ in the language of ZFC such that for the set-theoretic interpretation of any $L_a$-sentence $\phi$:

$$ZFC \vdash \phi \equiv T(\left\ulcorner \phi \right\urcorner)$$

Question 2 Can ZFC express arithmetic truth? That is, is there a wff $T(x)$ in the language of ZFC such that for the set-theoretic interpretation of any $L_a$-sentence $\phi$, $\phi$ is true in the standard model iff $ZFC \vdash T(\left\ulcorner \phi \right\urcorner)$.

And, finally, is there any relationship between these two questions?

• What is the difference between the two questions supposed to be? – Eric Wofsey Apr 30 '17 at 7:10
• Not entirely sure this is the "deepest" way of making the distinction, but question 1 is about whether ZFC can prove any biconditional of a certain form, whereas question 2 is about whether ZFC can express arithmetic truth in roughly the sense that it proves that a sentence is true just in case it's actually true. – user112067 Apr 30 '17 at 18:51
• Oh, I didn't realize that Question 2 was supposed to have parentheses around "$ZFC \vdash T(\left\ulcorner \phi \right\urcorner)$" rather than around "$T(\left\ulcorner \phi \right\urcorner)$ iff $\phi$ is true in the standard model of arithmetic". – Eric Wofsey Apr 30 '17 at 19:28
• Thanks, edited for clarity. – user112067 Apr 30 '17 at 19:34

A quick answer to Question 2 is NO. As $ZFC$ is recursively axiomatizable, if $T$ were any formula like that then $\{\varphi: ZFC \vdash T(\ulcorner \varphi \urcorner)\}$ would be recursively enumerable (i.e., $\Sigma^0_1$). However, the first-order theory of the standard model is not even arithmetic.
For Question 1, the answer is YES. Note that an $L_a$-formula is interpreted in ZFC as a formula with only bounded quantifiers: each $\forall x$ in an $L_a$-formula can be replaced by $\forall x \in \omega$ in ZFC. So in any $M \models ZFC$, the inductive definition of the satisfaction relation $\mathbb{N}^M \models \varphi$ can be done by an induction on the length of $\varphi$, and thus gives us a set $s \in M$ of the first-order theory of $\mathbb{N}^M$. The definition of $s$ is uniform (i.e., independent of $M$), so can be expressed by some $T(\ulcorner \cdot \urcorner)$.