Can we prove the completeness of FOL based on forcing? 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. 
 A: 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. 
