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

Question

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?

Answer 1

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)$.