Lemmas for Henkin's completeness theorem

v-- · v-- · commit 4e3919a410f1 · 2026-02-18T02:09:22.000+02:00
diff --git a/text/first_order_completeness.tex b/text/first_order_completeness.tex
@@ -5,17 +5,25 @@ \section{First-order completeness}\label{sec:first_order_completeness}
 \begin{definition}\label{def:fol_henkin_theory}\mcite[def. 3.1.7]{Hinman2005Logic}
   We say that the \hyperref[def:fol_theory]{first-order theory} \( \Gamma \) is \term[ru=экзистенциально полная (теория) (\cite[140]{ШеньВерещагин2017ЯзыкиИИсчисления})]{Henkin complete} is, whenever \( \qexists x \varphi \) belongs to \( \Gamma \), there exists a \hyperref[def:fol_closed_term]{closed term} \( \tau \) such that \( \varphi[x \mapsto \tau] \) belongs to \( \Gamma \). We call \( \tau \) the \term{Henkin witness} of \( \varphi \).
 \end{definition}
+\begin{comments}
+  \item Note that \( \qexists x \varphi \) is assumed to be closed, so \( x \) is the only variable possibly free in \( \varphi \).
+\end{comments}
 
 \begin{definition}\label{def:fol_henkin_extension}\mcite[def. 3.1.6]{VanDalen2004LogicAndStructure}
   Consider some \hyperref[def:fol_theory]{first-order theory} \( \Gamma \) over the signature \( \Sigma \).
 
-  Consider the \hyperref[def:fol_signature_extension]{extension} \( \Sigma^* \) of \( \Sigma \) where, for every existential formula \( \qexists x \varphi \) in \( \Gamma \), we add a new constant \( c_{x,\varphi} \).
+  Consider the \hyperref[def:fol_signature_extension]{extension} \( \Sigma^* \) of \( \Sigma \) where, for every existential formula \( \qexists x \varphi \) in \( \Gamma \), we add a new constant \( c_{x,\varphi} \). For the sake of determinism, suppose that \( c_{x,\varphi} \) is a symbol entirely determined by \( x \) and \( \varphi \).
 
   We define the \term{Henkin extension} \( \Gamma^* \) as the consequence closure of
   \begin{equation}\label{eq:def:fol_henkin_extension}
     \Gamma \cup \set[\big]{ (\qexists x \varphi) \synimplies \varphi[x \mapsto c_{x,\varphi}] \given* \qexists x \varphi \T{belongs to} \Gamma }.
   \end{equation}
 \end{definition}
+\begin{comments}
+  \item Note that \( \qexists x \varphi \) is assumed to be closed, so \( x \) is the only variable possibly free in \( \varphi \).
+
+  \item The determinism condition, although not present in \cite[def. 3.1.6]{VanDalen2004LogicAndStructure}, is important for some intermediate results like \cref{thm:def:fol_henkin_extension/scott_continuous}.
+\end{comments}
 
 \begin{theorem}[Theorem on constants]\label{thm:theorem_on_constants}\mcite[33]{Shoenfield1967MathematicalLogic}
   Over some \hyperref[def:fol_signature]{signature} \( \Sigma \), fix some set \( \Gamma \) of \hyperref[def:closed_fol_formula]{closed formulas} and a formula \( \varphi \) with free variables \( x_1, \ldots, x_n \).
@@ -73,10 +81,31 @@ \section{First-order completeness}\label{sec:first_order_completeness}
   \end{equation*}
 \end{proof}
 
+\begin{lemma}\label{thm:unward_union_of_theories}
+  With respect to a \hyperref[def:consequence_relation/compactness]{compact} \hyperref[def:consequence_relation]{consequence relation}, the union of an \hyperref[def:directed_set]{upward-directed family} of \hyperref[def:fol_theory]{first-order theories} is again a theory.
+\end{lemma}
+\begin{proof}
+  Let \( \seq{ \Gamma_k }_{k \in \mscrK} \) be an upward-directed family of theories and let \( \Gamma \) be their union.
+
+  If \( \Gamma \vdash \varphi \), by compactness there exists a finite subset \( \Gamma_0 \) of \( \Gamma \) such that \( \Gamma_0 \vdash \varphi \).
+
+  For every formula \( \psi \) in \( \Gamma \), let \( \Gamma_{k_\psi} \) be the smallest theory to which \( \psi \) belongs, and let \( k_0 > \max\set{ k_\psi \given \psi \in \Gamma_0 } \). Then \( \Gamma_0 \) is a subset of \( \Gamma_{k_0} \).
+
+  Since \( \varphi \) is a consequence of \( \Gamma_0 \), and hence of \( \Gamma_{k_0} \), it must belong to the latter, and hence to \( \Gamma \).
+
+  Therefore, \( \Gamma \) is also closed under consequence, i.e. it is a theory.
+\end{proof}
+
 \begin{proposition}\label{thm:def:fol_henkin_extension}
-  \hyperref[def:fol_henkin_extension]{Henkin extensions} of syntactic theories have the following basic properties:
+  \hyperref[def:fol_henkin_extension]{Henkin extensions} of syntactic (natural deduction) theories have the following basic properties:
   \begin{thmenum}
     \thmitem{thm:def:fol_henkin_extension/conservative}\mcite[lemma 3.1.7]{VanDalen2004LogicAndStructure} Every Henkin extension is \hyperref[def:fol_theory/conservative]{conservative}.
+
+    \thmitem{thm:def:fol_henkin_extension/scott_continuous} As an operator on theories, the Henkin extension operator \( (\anon)^* \) is \hyperref[def:scott_continuity]{Scott-continuous}.
+
+    \thmitem{thm:def:fol_henkin_extension/fixed_point}\mcite[lemma 3.1.8]{VanDalen2004LogicAndStructure} For a given theory \( \Gamma \), the union \( \Gamma^{*\omega} \) of the sequence \( \Gamma, \Gamma^*, \Gamma^{**}, \ldots \) is a \hyperref[def:fol_henkin_theory]{Henkin theory} and is invariant under Henkin extension.
+
+    Furthermore, \( \Gamma^{*\omega} \) is conservative over \( \Gamma \).
   \end{thmenum}
 \end{proposition}
 \begin{proof}
@@ -115,6 +144,26 @@ \section{First-order completeness}\label{sec:first_order_completeness}
   \end{equation*}
 
   Here \( \qexists x \psi \) is by assumption in \( \Gamma \), so \( P_{k+1} \) derives \( \varphi \) from \( \Gamma \cup \Delta_{k+1} \), as desired.
+
+  \SubProofOf{thm:def:fol_henkin_extension/scott_continuous} Let \( \seq{ \Gamma_k }_{k \in \mscrK} \) be an upward-directed family of theories and let \( \Gamma \) be their union. \Cref{thm:unward_union_of_theories} shows that \( \Gamma \) is also a theory.
+
+  We must show that
+  \begin{equation*}
+    \Gamma^* = \bigcup_{k \in \mscrK} \Gamma_k^*.
+  \end{equation*}
+
+  Indeed, let \( \psi = (\qexists x \varphi) \synimplies \varphi[x \mapsto c_{x,\varphi}] \) be a new axiom introduced in \( \Gamma^* \). Then there exists some index \( \Gamma_{k_0} \) to which \( \qexists x \varphi \) belongs. Then \( \psi \) is also present in \( \Gamma_{k_0}^* \). It follows that
+  \begin{equation*}
+    \Gamma^* \subseteq \bigcup_{k \in \mscrK} \Gamma_k^*.
+  \end{equation*}
+
+  Conversely, let \( \psi = (\qexists x \varphi) \synimplies \varphi[x \mapsto c_{x,\varphi}] \) be a new axiom introduced in some \( \Gamma_{k_0}^* \) for some index \( k_0 \). Then \( \qexists x \varphi \) is in \( \Gamma_{k_0} \), so \( \psi \) belongs to \( \Gamma^* \).
+
+  \SubProofOf{thm:def:fol_henkin_extension/fixed_point} Denote the signature of \( \Gamma \) by \( \Sigma \). Let \( \Gamma^{*\omega} \) be the union of \( \Gamma, \Gamma^*, \Gamma^{**}, \ldots \). \Cref{thm:unward_union_of_theories} implies that it is a theory, and \fullref{thm:knaster_tarski_iteration/continuous} implies that it is a fixed point of the Henkin extension operator.
+
+  Moreover, \( \Gamma^{*\omega} \) is a Henkin theory by construction. Indeed, given an existential formula \( \qexists x \varphi \) in \( \Gamma^{*\omega} \), since \( \Gamma^{*\omega} = \Gamma^{\omega*} \), it also contains \( (\qexists x \varphi) \synimplies \varphi[x \mapsto c_{x,\varphi}] \). Then can use \ref{inf:def:propositional_natural_deduction/imp/elim} to derive \( \varphi[x \mapsto c_{x,\varphi}] \).
+
+  It remains to show that \( \Gamma^{*\omega} \) is conservative over \( \Gamma \). If \( \varphi \) is a formula over \( \Sigma \) that belongs to \( \Gamma^{*\omega} \), it also belongs to some finite \( \Gamma^{*k} \). Using \cref{thm:def:fol_henkin_extension/conservative}, by induction on \( k \) we can show that \( \Gamma^{*k} \) is conservative over \( \Gamma \). Therefore, \( \varphi \) belongs to \( \Gamma \).
 \end{proof}
 
 \begin{theorem}[First-order completeness]\label{thm:fol_completeness}\mcite[thm. 3.1.3]{VanDalen2004LogicAndStructure}
diff --git a/text/first_order_theories.tex b/text/first_order_theories.tex
@@ -16,9 +16,9 @@ \section{First-order theories}\label{sec:first_order_theories}
 
     \thmitem{def:fol_theory/category} Based on theories and their morphisms, as per \cref{def:category_of_theories}, we have a category of (syntactic or semantic) theories \( \ucat{Th} \) for every \hyperref[def:grothendieck_universe]{Grothendieck universe} \( \mscrU \).
 
-    \thmitem{def:fol_theory/conservative} As in \cref{def:entailment_system_theory/conservative}, we say that a theory morphism \( t: (\Sigma, \Gamma) \to (\Theta, \Delta) \) is \term[en=conservative extension (\cite[180]{Hinman2005Logic})]{conservative} when \( \Gamma \vdash_\Sigma \varphi \) if and only if \( \Delta \vdash_\Theta \op*{Sen}(t)(\varphi) \).
+    \thmitem{def:fol_theory/conservative} Based on \cref{def:entailment_system_theory/conservative}, we say that a theory morphism \( t: (\Sigma, \Gamma) \to (\Theta, \Delta) \) is \term[en=conservative extension (\cite[180]{Hinman2005Logic})]{conservative} when \( \varphi \) belongs to \( \Gamma \) if and only if \( \op*{Sen}(t)(\varphi) \) belongs to \( \Delta \).
 
-    Sufficiency is obvious for both semantic entailment and natural deduction, so it usually suffices to check that \( \Delta \vdash_\Theta \op*{Sen}(t)(\varphi) \) implies \( \Gamma \vdash_\Sigma \varphi \).
+    Sufficiency is obvious for both semantic entailment and natural deduction, so it usually suffices to check that \( \op*{Sen}(t)(\varphi) \in \Delta \) implies \( \varphi \in \Gamma \).
 
     \thmitem{def:fol_theory/model}\mcite[def. 2.4.4]{Hinman2005Logic} As in \cref{def:theory_of_institutional_model}, we define the \term{theory} \( \cat{Th}(\mscrX) \) \hi{of} a structure \( \mscrX \) as the set of all sentences valid in \( \mscrX \).
 
diff --git a/text/propositional_completeness.tex b/text/propositional_completeness.tex
@@ -14,10 +14,6 @@ \section{Propositional completeness}\label{sec:propositional_completeness}
 
     \thmitem{def:propositional_theory/category} Based on propositional theories and their extensions, as per \cref{def:category_of_theories}, we have a (syntactic or semantic) category of theories \( \cat{Th} \).
 
-    \thmitem{def:propositoinal_theory/conservative} As in \cref{def:entailment_system_theory/conservative}, we say that a theory extension \( \Delta \) of \( \Gamma \) is \term{conservative} when \( \Gamma \vdash \varphi \) if and only if \( \Delta \vdash \varphi \).
-
-    Sufficiency is obvious for both semantic entailment and natural deduction, so it usually suffices to check that \( \Delta \vdash \varphi \) implies \( \Gamma \vdash \varphi \).
-
     \thmitem{def:propositional_theory/model}\mcite[def. 1.4.10]{Hinman2005Logic} As in \cref{def:theory_of_institutional_model}, we define the \term{theory} \( \cat{Th}(I) \) \hi{of} a propositional interpretation \( I \) as the set of all sentences valid in \( I \).
 
     \thmitem{def:propositional_theory/consistent}\mcite[def. 1.5.2]{VanDalen2004LogicAndStructure} We call a propositional theory \term[ru=противоречивое (множество формул) (\cite[def. 1.3.15]{Герасимов2014Вычислимость})]{consistent} if \( \Gamma \) contains no \hyperref[def:propositional_semantics/tautology]{contradictions}, i.e. if \( \Gamma \) does not contain \( \synbot \).
@@ -220,7 +216,7 @@ \section{Propositional completeness}\label{sec:propositional_completeness}
   \end{thmenum}
 \end{proposition}
 \begin{comments}
-  \item This also holds for \hyperref[sec:first_order_logic]{first-order logic} since the same natural deduction rules hold there.
+  \item This also holds for \hyperref[sec:first_order_logic]{first-order logic} since the same natural deduction rules are used there.
   \item See \cref{ex:con:curry_howard_correspondence/algebraic_types} for how this statement relates to \hyperref[def:simple_algebraic_type]{simple algebraic types} via the \hyperref[con:curry_howard_correspondence]{Curry-Howard correspondence}.
 \end{comments}
 \begin{proof}
