3
$\begingroup$

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

The proof by contradiction reads:

"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?

$\endgroup$

3 Answers 3

Reset to default
5
$\begingroup$

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

$\endgroup$
4
$\begingroup$

My intuition about this does not (directly) use contradiction. Rather, it follows from the soundness and completeness of first-order logic:

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

$\endgroup$
12
  • 1
    $\begingroup$ @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) $\endgroup$
    – Noah Schweber
    Dec 8, 2018 at 20:54
  • 1
    $\begingroup$ 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. $\endgroup$
    – Noah Schweber
    Dec 8, 2018 at 20:57
  • 1
    $\begingroup$ @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. $\endgroup$
    – Noah Schweber
    Dec 9, 2018 at 1:17
  • 1
    $\begingroup$ Everything after "I also like" is not part of the proof of compactness, but an afterthought. $\endgroup$
    – Noah Schweber
    Dec 9, 2018 at 1:17
  • 1
    $\begingroup$ @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. $\endgroup$
    – Noah Schweber
    May 25, 2021 at 2:11
1
$\begingroup$

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$

$\endgroup$
6
  • 1
    $\begingroup$ So does Doets assume that $\Sigma$ has a model? $\endgroup$
    – Mike
    Dec 8, 2018 at 20:32
  • $\begingroup$ 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$ $\endgroup$
    – ℋolo
    Dec 8, 2018 at 20:35
  • $\begingroup$ @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. $\endgroup$
    – Noah Schweber
    Dec 8, 2018 at 20:38
  • $\begingroup$ @NoahSchweber that is true.. but this is the easiest way to look at this(at least the easiest from the ways I know) $\endgroup$
    – ℋolo
    Dec 8, 2018 at 20:50
  • $\begingroup$ @Holo I disagree - $\vdash$ isn't needed at all, this is just a direct application of the basic definition of $\models$. $\endgroup$
    – Noah Schweber
    Dec 8, 2018 at 20:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .