Henkin extensions are conservative

Author: v--

text/first_order_completeness.tex

@@ -13,7 +13,7 @@ \section{First-order completeness}\label{sec:first_order_completeness}
 
   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 }.
+    \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}
 
@@ -76,13 +76,45 @@ \section{First-order completeness}\label{sec:first_order_completeness}
 \begin{proposition}\label{thm:def:fol_henkin_extension}
   \hyperref[def:fol_henkin_extension]{Henkin extensions} of syntactic theories have the following basic properties:
   \begin{thmenum}
-    \thmitem{thm:def:fol_henkin_extension/conservative}\mcite[lemma 3.1.7]{VanDalen2004LogicAndStructure} A Henkin extension is \hyperref[def:fol_theory/conservative]{conservative}.
+    \thmitem{thm:def:fol_henkin_extension/conservative}\mcite[lemma 3.1.7]{VanDalen2004LogicAndStructure} Every Henkin extension is \hyperref[def:fol_theory/conservative]{conservative}.
   \end{thmenum}
 \end{proposition}
 \begin{proof}
-  \SubProofOf{thm:def:fol_henkin_extension/conservative} Let \( \Gamma \) be a theory over \( \Sigma \). Let \( \Gamma^* \) be the Henkin extension of \( \Gamma \) with signature \( \Sigma^+ \).
+  \SubProofOf{thm:def:fol_henkin_extension/conservative} Let \( \Gamma \) be a theory over \( \Sigma \). Let \( \Gamma^* \) be the Henkin extension of \( \Gamma \) with signature \( \Sigma^+ \). Denote by \( \Delta \) the set of additional axioms from \( \Gamma^* \), so that \( \Gamma^* = \op*{Th}(\Gamma \cup \Delta) \).
 
-  Fix a formula \( \varphi \) over \( \Sigma \) that belongs to \( \Gamma^* \). Since \( \Gamma^* \) is a consequence closure of \eqref{eq:def:fol_henkin_extension}, there exists a \hyperref[def:fol_natural_deduction_proof_tree]{proof tree} \( P \) for \( \varphi \) whose open assumptions are from \eqref{eq:def:fol_henkin_extension}.
+  Fix a formula \( \varphi \) over \( \Sigma \) that belongs to \( \Gamma^* \). Since \( \Gamma^* \) is a consequence closure of \( \Gamma \cup \Delta \), there exists a \hyperref[def:fol_natural_deduction_proof_tree]{proof tree} \( P \) for \( \varphi \) whose open assumptions are from \( \Gamma \cup \Delta \).
+
+  Let \( \Delta_0 \) be the subset of formulas of \( \Delta \) that are open assumptions in \( P \). We will recursively build a sequence \( \ldots \subseteq \Delta_2 \subseteq \Delta_1 \subseteq \Delta_0 \) that eventually stabilizes at the empty set, and a corresponding sequence \( P_1, P_2, \ldots \) of proof trees, where \( P_k \) derives \( \varphi \) from \( \Gamma \cup \Delta_k \) and does not contain new constants except those from \( \Delta_k \).
+
+  We start with \( \Delta_0 \) and \( P_0 \coloneqq P \). At step \( k + 1 \), suppose we have already constructed \( \Delta_k \) and \( P_k \). If \( \Delta_k \) is empty, we are done with the proof. Otherwise, fix an axiom \( (\qexists x \psi) \synimplies \psi[x \mapsto c_{x,\psi}] \) from \( \Delta_k \) and define \( \Delta_{k+1} \) by removing it from \( \Delta_k \).
+
+  \Fullref{thm:fol_natural_deduction_deduction_theorem} gives us a proof tree \( P_k' \) deriving
+  \begin{equation*}
+    ((\qexists x \psi) \synimplies \psi[x \mapsto c_{x,\psi}]) \synimplies \varphi
+  \end{equation*}
+  from \( \Gamma \cup \Delta_{k+1} \), and \fullref{thm:theorem_on_constants} gives us a tree \( P_k^\dprime \) not containing \( c_{x,\psi} \) and deriving
+  \begin{equation*}
+    \qforall y \parens[\big]{ ((\qexists x \psi) \synimplies \psi[x \mapsto y]) \synimplies \varphi }
+  \end{equation*}
+  from \( \Gamma \cup \Delta_{k+1} \).
+
+  Let \( P_{k+1} \) be the following tree:
+  \begin{equation*}
+    \begin{prooftree}
+      \hypo{ [\qexists x \psi]^u }
+
+      \hypo{}
+      \ellipsis {\( P_k^\dprime \)} { \qforall y \parens[\big]{ ((\qexists x \psi) \synimplies \psi[x \mapsto y]) \synimplies \varphi } }
+      \infer1[\ref{inf:def:fol_natural_deduction/forall/elim}]{ ((\qexists x \psi) \synimplies \psi[x \mapsto y]) \synimplies \varphi }
+
+      \hypo{ [\psi[x \mapsto y]]^v }
+      \infer1[\ref{inf:def:propositional_natural_deduction/imp/intro}]{ \qexists x \psi \synimplies \psi[x \mapsto y] }
+      \infer2[\ref{inf:def:propositional_natural_deduction/imp/elim}]{ \varphi }
+      \infer[left label={\( v \)}]2[\ref{inf:def:fol_natural_deduction/exists/elim}]{ \varphi }
+    \end{prooftree}
+  \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.
 \end{proof}
 
 \begin{theorem}[First-order completeness]\label{thm:fol_completeness}\mcite[thm. 3.1.3]{VanDalen2004LogicAndStructure}

text/propositional_natural_deduction.tex

@@ -997,6 +997,13 @@ \section{Propositional natural deduction}\label{sec:propositional_natural_deduct
 \begin{proposition}\label{thm:propositional_admissible_rules}
   The following \hyperref[def:natural_deduction_rule]{natural deduction rules} are \hyperref[con:inference_rule_admissibility]{admissible} with respect to \hyperref[def:propositional_natural_deduction]{minimal propositional natural deduction}:
   \begin{thmenum}
+    \thmitem{thm:propositional_admissible_rules/self_conditional} The conditional of a formula with itself is tautologous:
+    \begin{equation*}\taglabel[\ensuremath{ \rightarrow_R }]{inf:thm:propositional_admissible_rules/self_conditional}
+      \begin{prooftree}
+        \infer0[\ref{inf:thm:propositional_admissible_rules/self_conditional}]{ \varphi \synimplies \varphi }
+      \end{prooftree}
+    \end{equation*}
+
     \thmitem{thm:propositional_admissible_rules/self_biconditional} The biconditional of a formula with itself is tautologous:
     \begin{equation*}\taglabel[\ensuremath{ \leftrightarrow_R }]{inf:thm:propositional_admissible_rules/self_biconditional}
       \begin{prooftree}
@@ -1065,6 +1072,15 @@ \section{Propositional natural deduction}\label{sec:propositional_natural_deduct
   \item These rules will be valid for \hyperref[def:first_order_logic]{first-order logic} and \hyperref[def:higher_order_logic]{higher-order logic} because the systems we will consider these will extend the propositional natural deduction rules.
 \end{comments}
 \begin{proof}
+  \SubProofOf{thm:propositional_admissible_rules/self_conditional}
+  \begin{equation*}
+    \begin{prooftree}
+      \hypo{ [\varphi]^u }
+      \hypo{ [\varphi]^u }
+      \infer[left label=\( u \)]2[\ref{inf:def:propositional_natural_deduction/imp/intro}]{ \varphi \synimplies \varphi }
+    \end{prooftree}
+  \end{equation*}
+
   \SubProofOf{thm:propositional_admissible_rules/self_biconditional}
   \begin{equation*}
     \begin{prooftree}