Henkin-style proof of first-order compactness

Question

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.

Answer 1

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