# 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? Apr 30, 2017 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. Apr 30, 2017 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". Apr 30, 2017 at 19:28
• Thanks, edited for clarity. Apr 30, 2017 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, relaxing provability 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$$ (standard reference for this process is Azriel Lévy's A hierarchy of formulas in set theory, 1964), 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)$$.