Difference between truth and proof Let $\sigma$ be a signature, i.e. a set of operation symbols and relation symbols. Let $\mathcal{M}$ a structure that interprets $\sigma$, i.e. a set $M$ called the domain and a function or relation on $M$ for each symbol of $\sigma$, with the proper arities. Then a closed formula $F$ in the language of $\sigma$ can be interpreted in $\mathcal{M}$ as a value in $\{0,1\}$, by recursively interpreting the sub-formulas of $F$, and combining the sub-interpretations according to the logical connectives in $F$ (which can be $\lnot,\land,\lor,\Rightarrow,\forall,\exists$). As usual we note $\mathcal{M}\models F$ when this interpretation is 1. Since this interpretation mimics the logical reasoning we have in the ZFC set theory, I wonder whether the following equivalence holds
$$ \mathcal{M}\models F \quad\text{ if and only if }\quad ZFC \vdash F_M $$
where $F_M$ is a syntactic transformation of formula $F$ into a ZFC formula, by quantifying variables over the domain $M$ and replacing all symbols of $\sigma$ by their set-theoretic interpretations in $\mathcal{M}$.
As a simple corollary we would also have $\mathcal{M}\not\models F$ if and only if $ZFC \vdash \lnot F_M $.
But this would contradict the usual distinction we make between semantics and syntax. Truth is usually more on the left-hand side, when a model satisfies a formula, and provability is more on the right-hand side.
 A: The first major problem you run into here is that if you start with an arbitrary structure $\mathcal M$, then it's not a given that you can even define that $\mathcal M$ using a formula of set theory. Your proposed translation from $F$ to $F_{\mathcal M}$ needs to assume that you can write a symbolic formula that defines what the variable should range over when you translate $\forall x.\varphi$ -- but where do you get such a formula from? The symbol "$\mathcal M$" is not part of the language of set theory!
Even if $\sigma$ is something simple, such as a single constant $0$, a unary function $'$ and a unary predicate $p$, there are uncountably many elementarily distinct structures over that signature, differing in whether they consider each of $p(0), p(0'), p(0''), \ldots$ to be true. But there are only countably many formulas, so you'll have a hard time deriving your $F_M$ transformation in a systematic way. (Of course an unsystematic way would be to translate every $F$ to either $\forall x.x\in x$ or $\neg\forall x.x\in x$ depending on whether $\mathcal M\vDash F$ -- but surely that's cheating).
So you might decide to restrict yourself to $\mathcal M$ that you can define uniquely in the language of set theory -- such as, for example, $\mathbb N$ as an interpretation of $\sigma=(0,1,{+},{\times})$. In that particular case, your $F\mapsto F_{\mathcal M}$ is indeed just the standard way to represent arithmetic formulas in the language of set theory.
But then, as Asaf pointed out in a comment, you run into Gödel's first incompleteness theorem which says that ZFC doesn't prove every true formula over $(\mathbb N,0,1,{+},{\times})$ -- and neither does any other reasonable* theory.
So not even restricting to definable structures gives you what you were hoping for.

* Here "reasonable" means roughly that the theory is consistent (so it doesn't prove any false formulas either) and recursively axiomatized (so there's an algorithm for determining whether a claimed axiom is in fact an axiom).
