# 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.

• What if $F$ is "Con(ZFC)" as an arithmetic statement and $\cal M$ is just $\omega$ as the usual model of PA? May 29 at 18:17

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.