# If $\Sigma \models \phi$, then for some finite $\Delta \subset\Sigma$, $\Delta \models \phi$.

This is an easy consequence (Doets calls it Compactness Theorem (version 2)) in Kees Doets' Basic Model theory:

Let $$\Sigma$$ a set of sentences and $$\phi$$ a sentence.

If $$\Sigma \models \phi$$, then for some finite $$\Delta \subset\Sigma$$, $$\Delta \models \phi$$.

"If $$\phi$$ does not logically follow from some $$\Delta \subset \Sigma$$, then the set $$\Sigma \cup \{\neg \phi\}$$ is finitely satisfiable and therefore, by compactness, satisfiable."

How do we know that $$\Sigma \cup \{\neg \phi\}$$ is finitely satisfiable?

From the fact that $$\phi$$ does not logically follow from some $$\Delta$$, we know that $$\neg \phi$$ follows from every $$\Delta \subset \Sigma$$. But how does this imply that there's a model for every finite subset of the set of sentences?

First, a quick comment. Your statement "From the fact that $$\varphi$$ does not logically follow from some $$\Delta$$, we know that $$\neg\varphi$$ follows from every $$\Delta\subseteq \Sigma$$." is incorrect: when $$A$$ is a set of sentences, "$$A\not\models b$$" is different from "$$A\models\neg b$$." We could have $$b$$ be independent of $$A$$ - that is, $$A\not\models b$$ and $$A\not\models\neg b$$.

What is true is that since $$\varphi$$ isn't entailed by any finite $$\Delta\subseteq\Sigma$$, $$\neg\varphi$$ must be compatible with every finite $$\Delta\subseteq\Sigma$$ in the sense that, for every $$\Delta\subseteq\Sigma$$, the set $$\Delta\cup\{\neg\varphi\}$$ will be satisfiable. (It's arguably more natural to say "consistent with" instead of "compatible with," but consistency is a syntactic property which isn't needed in this purely semantic question, so I want to avoid using language which might bring in confusion.)

This is in fact the crux of the problem!

Saying "$$\Sigma\cup\{\neg\varphi\}$$ is finitely satisfiable" just means "$$\Delta\cup\{\neg\varphi\}$$ is satisfiable for every finite $$\Delta\subseteq\Sigma$$." But "$$\Delta\cup\{\neg\varphi\}$$ is satisfiable" just means "there is some model of $$\Delta\cup\{\neg\varphi\}$$," which is to say $$\Delta\not\models\varphi$$ ("$$\Delta\models\varphi$$" means exactly "every model of $$\Delta$$ satisfies $$\varphi$$," which can't be true if there is some model of $$\Delta\cup\{\neg\varphi\}$$).

All that is to say that the statement "$$\Sigma\cup\{\neg\varphi\}$$ is finitely satisfiable" is equivalent to "For every finite $$\Delta\subseteq\Sigma$$, we have $$\Delta\not\models\varphi$$." But this latter statement is precisely our hypothesis "$$\varphi$$ does not logically follow from some [finite] $$\Delta\subseteq\Sigma$$!"

Note that the phrase "logically follow from" could confuse things here: it's meant in the semantic sense ($$\models$$), not the syntactic sense ($$\vdash$$).

If $$\Sigma\vDash\phi$$, then there is a proof of $$\Sigma\vdash\phi$$ (completeness), and since that proof is a finite object it mentions at most finitely many of the axioms of $$\Sigma$$. Therefore the same proof proves $$\Delta\vdash\phi$$ for some finite $$\Delta\subseteq\Sigma$$, and thus $$\Delta\vDash\phi$$ (soundness).

• @HenningMakholm You're probably already familiar with this, but just in case: the semantic proof of compactness that really clicked for me - before the ultraproduct proof - was the fact that you can make Henkinization purely semantic. Let $\models_{fin}$ be the "finitary satisfaction relation," $A\models_{fin}b$ iff $D\models b$ for some finite $D\subseteq A$. We now proceed as usual, with $\models_{fin}$ in place of $\vdash$, and everything goes through basically unchanged. I also like this argument because it gives a(n interestingly, completely ahistorical) "story" for completeness: (cont'd) Commented Dec 8, 2018 at 20:54
• in light of the coincidence of $\models$ with $\models_{fin}$, since the latter is finitary it's reasonable to hope that it is in fact computably enumerable. To find an appropriate $\vdash$, we now just look carefully through the proof that $\models_{fin}$ is all of $\models$, and each time we use a property of $\models_{fin}$ we get a corresponding proof rule. Of course, this isn't how it happened, but it's a natural enough story that I found it very helpful in learning the proof theoretic side of things: that the semantic result led naturally to the syntactic conjecture and ultimate success. Commented Dec 8, 2018 at 20:57
• @HenningMakholm Comment 2 happens after comment 1. The "in light of" is following the proof of the compactness theorem above. My point is that, having proved compactness, it's now natural to look for a proof notion making the completeness theorem true; and having proved compactness specifically in the Henkin style, this becomes very straightforward. Commented Dec 9, 2018 at 1:17
• Everything after "I also like" is not part of the proof of compactness, but an afterthought. Commented Dec 9, 2018 at 1:17
• @AtticusStonestrom Yup, that tends to be exactly how I explain it. So far I've had good results, but to be fair I've only taught rather limited audiences with this so far. Commented May 25, 2021 at 2:11

Every $$\Delta$$ finite have $$\Delta\vDash\lnot\varphi$$, so every model of $$\Delta$$ is a model of $$\Delta\cup\{\lnot\varphi\}$$, and there is a model for every $$\Delta$$, namely, the model of $$\Sigma$$

• So does Doets assume that $\Sigma$ has a model?
– Mike
Commented Dec 8, 2018 at 20:32
• If there is no model to $\Sigma$, there is finite deduction sequence that proves contradiction, take $\Delta$ be all the elements of $\Sigma$ that appear in that sequence and you got a finite subset of $\Sigma$ that proves $\varphi$
– Holo
Commented Dec 8, 2018 at 20:35
• @Holo "If there is no model to $\Sigma$, there is finite deduction sequence that proves contradiction" This uses the completeness theorem, which is overkill here. Commented Dec 8, 2018 at 20:38
• @NoahSchweber that is true.. but this is the easiest way to look at this(at least the easiest from the ways I know)
– Holo
Commented Dec 8, 2018 at 20:50
• @Holo I disagree - $\vdash$ isn't needed at all, this is just a direct application of the basic definition of $\models$. Commented Dec 8, 2018 at 20:51