Theorem: Finitely Satisfiable Set of Sentences has Maximal Finitely Satisfiable Extension

Let $\LL$ be a language of predicate logic.
Let $\FF$ be a finitely satisfiable set of $\LL$-sentences.
Then there exists a finitely satisfiable set of $\LL$-sentences $\FF' \supseteq \FF$ such that:
:For all $\LL$-sentences $\phi$, either $\phi \in \FF'$ or $\sqbrk {\neg \phi} \in \FF'$

Proof:
Let $S$ be the set of all $\LL$-sentences.
For every finite subset $P \subseteq S$, define:
:$M_P = \set {t \in \Bbb B^P : \exists \MM : \paren {\MM \models_{\mathrm {PL}} \FF \cap P} \land \paren {\forall \phi \in P : \map t \phi = T \iff \MM \models_{\mathrm {PL}} \phi}}$
Define:
:$M = \bigcup_{P \mathop \in I} M_K$
where $I$ is the set of all finite subsets of $S$.
We want to show that $M$ is a binary mess over $S$.
For axiom $\text M 1$:
:Let $P \in I$ be arbitrary.
:As Intersection is Subset and Subset of Finite Set is Finite, $\FF \cap P$ is a finite subset of $\FF$.
:As $\FF$ is finitely satisfiable, there is some $\LL$-structure $\MM_P$ such that $\MM_P \models_{\mathrm {PL}} \FF \cap P$.
:Define $t_P : P \to \Bbb B$ as:
::$\map {t_P} \phi = \begin{cases}
T & : \MM_P \models_{\mathrm {PL}} \phi \\
F & : \MM_P \not\models_{\mathrm {PL}} \phi
\end{cases}$
:As it satisfies the rule, $t_P \in M_P \subseteq M$, proving axiom $\text M 1$.
For axiom $\text M 2$:
:Let $P \in I$ and $t \in M$ be arbitrary.
:By definition, $t \in M_Q$ for some $Q \in I$.
:Thus, there is some $\LL$-structure $\MM_Q$ such that:
::$\MM_Q \models_{\mathrm {PL}} \FF \cap Q$
::$\map t \phi = T \iff \MM_Q \models_{\mathrm {PL}} \phi$ for all $\phi \in Q$
:As $\FF \cap Q \cap P \subseteq \FF \cap Q$, it follows that $\MM_Q \models \FF \cap Q \cap P$
:As $Q \cap P \subseteq Q$, it follows that $\map t \phi = T \iff \MM_Q \models_{\mathrm {PL}} \phi$ for all $\phi \in Q \cap P$
:Thus, $t \restriction_P$ satisfies the criteria for $M_{Q \cap P}$, and $t \restriction_P \in M$, proving axiom $\text M 2$.
{{qed|lemma}}
By the Consistency Principle for Binary Mess:
:There exists a mapping $f : S \to \Bbb B$ that is consistent with $M$.
Define:
:$\FF' = \set {\phi \in S : \map f \phi = T}$
We now need to verify that the following properties hold for $\FF'$:
:$\FF' \supseteq \FF$.
:$\FF'$ is finitely satisfiable.
:$\forall \phi \in S: \phi \in \FF' \lor \sqbrk {\neg \phi} \in \FF'$.
Let $\phi \in \FF$ be arbitrary.
We need to show that $\map f \phi = T$.
By definition of consistent, $f\restriction_{\set \phi} \in M$.
Thus, there is an $\LL$-structure $\MM_{\set \phi}$ such that:
:$\MM_{\set \phi} \models \set \phi$
:$\map {f\restriction_{\set \phi}} \phi = T \iff \MM_{\set \phi} \models \set \phi$
It immediately follows that $\map {f\restriction_{\set \phi}} \phi = T$, and thus that $\map f \phi = T$.
{{qed|lemma}}
Let $P \subseteq \FF'$ be an arbitrary finite subset.
By definition, for every $\phi \in P$, $\map f \phi = T$.
By definition of consistent, $f\restriction_P \in M$.
Thus, there is an $\LL$-structure $\MM_P$ such that:
:$\forall \phi \in P: \map {f\restriction_P} \phi = T \iff \MM_P \models \phi$
It follows immediately that:
:$\forall \phi \in P: \MM_P \models \phi$
As $P$ was arbitrary, $\FF'$ is finitely satisfiable by definition.
{{qed|lemma}}
{{AimForCont}}, suppose $\phi \notin \FF'$ and $\sqbrk {\neg \phi} \notin \FF'$, where $\phi \in S$.
Then, $\map f \phi = \map f {\neg \phi} = F$, by definition of $\FF'$.
By definition of consistent, we have that $f\restriction_{\set {\phi, \neg \phi}} \in M$.
Thus, there is an $\LL$-structure $\MM_{\set {\phi, \neg \phi}}$ such that:
:$\map {f\restriction_{\set {\phi, \neg \phi}}} \phi = T \iff \MM_{\set {\phi, \neg \phi}} \models \phi$
:$\map {f\restriction_{\set {\phi, \neg \phi}}} {\neg \phi} = T \iff \MM_{\set {\phi, \neg \phi}} \models \neg \phi$
It follows immediately that:
:$\MM_{\set {\phi, \neg \phi}} \not\models \phi$
:$\MM_{\set {\phi, \neg \phi}} \not\models \neg \phi$
By definition of $\mathrm{PL}$:
:$\map {\operatorname{val}_{\MM_{\set {\phi, \neg \phi}}}} \phi = F$
:$\map {\operatorname{val}_{\MM_{\set {\phi, \neg \phi}}}} {\neg \phi} = F$
{{begin-eqn}}
{{eqn | l = F
      | r = \map {\operatorname{val}_{\MM_{\set {\phi, \neg \phi} } } } {\neg \phi}
}}
{{eqn | r = \map {f^\neg} {\map {\operatorname{val}_{\MM_{\set {\phi, \neg \phi} } } } \phi}
      | c = {{Defof|Value of Formula under Assignment}}
}}
{{eqn | r = \map {f^\neg} F}}
{{eqn | r = T
      | c = {{Defof|Logical Not/Truth Function|Truth Function of Logical Not}}
}}
{{end-eqn}}
As $F \ne T$, that is a contradiction.
Thus, at least one of $\phi$ and $\neg \phi$ is in $\FF'$
{{qed}}
{{BPI|Consistency Principle for Binary Mess}}