6
$\begingroup$

In the comments to my answer to this post Noah Schweber mentioned a Henkin-style proof of the compactness theorem for first-order logic, based on a finitary satisfaction relation. At his suggestion, I'm posting to ask to see the proof. I'm particularly interested to see how this proof of compactness can help you engineer a sound and complete proof system.

$\endgroup$
3
  • $\begingroup$ Maybe you are interested in this semantic (and very elegant) proof. $\endgroup$ – Taroccoesbrocco Aug 9 '19 at 17:37
  • $\begingroup$ @Taroccoesbrocco That one's not quite the same thing, but Joel's answer to that question (of which I was unaware) does mention the argument I give below. $\endgroup$ – Noah Schweber Aug 9 '19 at 17:45
  • $\begingroup$ Thanks for the link to the MO post. $\endgroup$ – Chris Eagle Aug 9 '19 at 18:46
4
$\begingroup$

EDIT: An old MO answer of Joel David Hamkins mentions this argument briefly, and that question and its answers are quite interesting. Also I should clarify that this argument is very much not due to me - it seems to be folklore.


Let $\models_f$ be the finitary companion of the usual entailment relation $\models$: that is, $\Gamma\models_f\varphi$ iff $\Gamma'\models\varphi$ for some finite $\Gamma'\subseteq\Gamma$. This consequence relation is trivially compact, and we want to show that it coincides with $\models$.

As in the proof of the completeness theorem, we're going to set up a notion of term structure $Term(\Gamma;\models_f)$ assigned to an arbitrary finitely satisfiable theory $\Gamma$; we'll then argue that every theory $\Gamma$ is contained in a larger theory $\Gamma'$ such that $Term(\Gamma';\models_f)\models\Gamma'$ (and hence $\Gamma$).

Our term structures are defined in the obvious way:

  • The underlying set of $Term(\Gamma;\models_f)$ is the set of equivalence classes of closed terms in our language, under the equivalence relation $$t\approx_\Gamma^f s\iff \Gamma\models_ft=s.$$

  • The interpretation is given in the obvious way (e.g. for a term $t$ and a unary predicate $U$ we set $Term(\Gamma;\models_f)\models U([t])$ iff $\Gamma\models_fU(t)$), with well-definedness being straightforward to prove.

(Why closed terms? I just prefer to avoid free variables. This is purely a matter of taste. Note that we can always add a new constant symbol into our language, so WLOG there actually are closed terms in the language of our theory and so we get a nonempty term structure, or we could just allow structures to be empty in general.)

As in the proof of the completeness theorem, there's no reason to have $Term(\Gamma;\models_f)\models\Gamma$. So we need to fix this. As before we'll look at two particular ways to "improve" a theory:

  • Every finitely satisfiable theory $\Gamma$ has a "$\models_f$-complete" extension - that is, a finitely satisfiable extension $\Gamma'\supseteq\Gamma$ such that for each $\varphi$ we have $\Gamma\models_f\varphi$ or $\Gamma\models_f\neg\varphi$. This is proved exactly as for $\vdash$ - just do a "greedy algorithm." The key point is that the result is in fact finitely satisfiable, and this holds since every finite stage was finitely satisfiable and finite satisfiability of a theory is determined by its finite fragments.

  • We can also Henkinize exactly as usual. If $\Gamma\models_f\forall x\exists y\varphi(x,y)$, we can add a function symbol $p_\varphi$ and pass to $\Gamma\cup\{\forall x\varphi(x, p(x))\}$, which is finitely satisfiable if $\Gamma$ itself is.

These two transformations together let us build, for $\Gamma$ an arbitrary finitely satisfiable theory, an extension $\Gamma'\supseteq\Gamma$ which is finitely satisfiable and $\models_f$-complete. We now prove that

$(*)$ for each $\psi\in\Gamma'$ we have $Term(\Gamma';\models_f)\models\psi$

by (a purely semantic) induction on complexity of $\psi$, and finish the proof by passing to the reduct to the original language of $\Gamma$.

Going through this argument with a fine-toothed comb, we can enumerate the properties $\models_f$ needs to satisfy in order for things to work out. For example, we need to have rules like "If $\Gamma\models_f\psi$ and $\Gamma\models_f\theta$ then $\Gamma\models_f\psi\wedge\theta$" in order to run the inductive proof of $(*)$. The consequence relation generated by all these rules is then trivially complete, and was "discovered organically" - there was never a worry that we might not find all the rules since we were literally just ripping them from an argument we already knew worked.

(This isn't quite fair - it's important to note that in addition to finitary closure properties, the argument above needed $\models_f$ to be finitary in order to construct $\models_f$-completions. But finitarity of our consequence relation is trivial, since it's generated by definition from finitary rules.)


Afterthought: One thing I really like about this argument is that it motivates the idea of taking a purely semantic consequence relation and studying its various "cousins," especially its perhaps-better-behaved fragments. This becomes a really important perspective in the study of infinitary logic, introduced by Barwise (see e.g. section $3$ of Keisler/Knight's wonderful survey). Perhaps more valuably it builds (at least, it did for me) an "aesthetic bridge" between the syntactic and semantic perspectives on consequence relations, which (again, at least for me) helps motivate their algebraic study which somehow falls (yet again, at least for me) in between the two

$\endgroup$
1
  • $\begingroup$ Thank you! This is a very nice argument, especially for the reasons you describe in the "afterthought". I always felt like it was sort of a stroke of good luck that someone happened to come up with an adequate proof system, but this argument makes it clear to me that one could have come up with the proof system along the way to proving the completeness theorem (I doubt that's the real history, but I always like feeling like things could be discovered by non-geniuses - of course, thinking to look at the finite consequence relation is clever too!). $\endgroup$ – Chris Eagle Aug 9 '19 at 17: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.