Tarski famously proved arithmetic truth is not definable in the language of arithmetic. Ie there's no predicate $T$ such that $T(|\sigma|)$ is true in the standard model of arithmetic iff $\sigma$ is true in the standard model of arithmetic.
I have heard that nonetheless such a predicate exists in the language of ZF set theory. Since there is no standard model of ZF, what does it mean for an arithmetic truth predicate T to exist in the language of ZF?
Possibly “there is no standard model of ZF” betrays my total ignorance of set theory.
