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.

  • 1
    $\begingroup$ What if $F$ is "Con(ZFC)" as an arithmetic statement and $\cal M$ is just $\omega$ as the usual model of PA? $\endgroup$
    – Asaf Karagila
    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.

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.