2
$\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$
4
$\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$ Dec 8 '18 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$ Dec 8 '18 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$ Dec 9 '18 at 1:17
  • 1
    $\begingroup$ Everything after "I also like" is not part of the proof of compactness, but an afterthought. $\endgroup$ Dec 9 '18 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$ May 25 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 '18 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 '18 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$ Dec 8 '18 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 '18 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$ Dec 8 '18 at 20:51

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.