3
$\begingroup$

In David Marker's Model Theory, there is a exercise said " we can view a countable Henkin construction as a forcing construction ". But in the book the Henkin construction is used to prove the compactness theorem. He didn't prove the completeness theorem.

So my question is can we use forcing method to prove the completeness of first-order logic?

Thank you in advance.

  • 3
    Crossed posted on MathOverflow: http://mathoverflow.net/questions/116686/can-we-prove-the-completeness-of-fol-based-on-forcing2012-12-18

1 Answers 1

4

For simplicity, assume the original language is countable and that we have added a countable set of new constant symbols to the language. The Henkin construction makes a model whose domain is the set of these constant symbols.

Consider the Lindenbaum algebra $\mathcal{A}$ of the theory in the expanded language, ordered so that $\phi < \psi$ if $\phi \to \psi$, so the least element is $\bot$. Recall a filter on the algebra is a subset that is upward closed and so that for all $A,B$ in the filter there is a $C$ in the filter with $C \leq A$ and $C \leq B$. A filter is deductively closed if it is closed under the deduction rules of first order logic.

The deductive closure of the original theory $T$ gives a deductively closed filter $F_T$ that does not contain $\bot$, because the original theory is consistent. The point of the Henkin construction is that any extension of $F_T$ to a maximal deductively closed filter not containing $\bot$ will let us form a model of $T$. This extension can be formed because, for any $\phi$, a consistent theory cannot prove both $\phi$ and $\lnot \phi$, and thus it is consistent to add either $\lnot \phi$, if the theory does not prove $\phi$, or to add $\phi$, if the theory does not prove $\lnot \phi$.

This can be viewed as a forcing construction where the poset $P$ is the set of all deductively closed filters extending $T$, not containing $\bot$, which only mention finitely many of the new constants. The poset is ordered so that $F \leq G$ if $G \subseteq F$. A condition $F$ forces a statement $\phi$ if $\phi \in F$. For each $\phi$, the set of conditions that force $\phi$ or force $\lnot \phi$ is dense. Thus a generic filter for this notion of forcing will be an increasing sequence of filters on $\mathcal{A}$ none of which contains $\bot$ and which are all deductively closed. The union of this sequence will again be a filter $F$ on $\mathcal{A}$ that does not contain $\bot$, is deductively closed, and which contains either $\phi$ or $\lnot \phi$ for every $\phi$ in the extended language. There is another family of dense sets which ensure that for every existential formula $(\exists x)\phi(x)$ in the generic filter there will be a formula $\phi(c)$ for some constant symbol $c$ (this is why we need each filter to only mention finitely many of the constants). The reason that we need to assume everything is countable is so that the overall construction only needs to meet countably many dense sets, so that we can prove the generic filter exists. When constructed properly, the generic filter for this notion of forcing can be used to construct a Henkin model for $T$.

Another way to achieve the same result is to force with the poset of finite sets of formulas that are consistent with $T$, ordered by extension. This is closer in spirit to Cohen forcing from set theory, and it's the way to set things up for "effective" forcing in recursion theory. But this way looks even more like the usual inductive construction of the Henkin theory, thinly disguised as forcing.

  • 0
    So the proof shows that forcing can be used to construct a maximal consistent theory? I had expected forcing can do more.2012-12-19
  • 0
    Forcing is a convenient and elegant way of organizing a certain type of proof. Many proofs can be recast as "forcing" proofs even though the forcing machinery does very little. This is particularly the case in recursion theory and proof theory. The real power of forcing for results that can't be done "directly" is in set theory. The difference here is that we can directly construct the maximal filter anyway, so we don't "need" to use forcing, but in set theory the models that are obtained by forcing cannot be "directly" constructed without it.2012-12-19
  • 0
    As written, the construction does not produce a Henkin theory. $P$ should really be the poset of deductively closed consistent theories extending $T$ which are *finitely* axiomatized over $T$. Then for every formula $\phi(x)$, the set of conditions forcing $\exists x\,\phi(x)\to\phi(c)$ for some constant $c$ is also dense (due to the countable supply of fresh constants), hence the generic filter will give a Henkin theory.2012-12-19
  • 1
    It may be worth mentioning that the same construction (considering some more dense sets) can also be used to prove the omitting types theorem. This may help explaining why it only works for countable theories, since unlike the completeness theorem, the omitting types theorem does not hold for uncountable theories.2012-12-19
  • 0
    @Emil: thanks, you are right of course - we have to make sure that we actually build the Henkin theory as we go.2012-12-19