Revise the section on propositional natural deduction

Author: v--

src/notebook/math/logic/classical_logic.py

@@ -23,8 +23,8 @@
     parse_natural_deduction_rule('→₋', '(φ → ψ), φ ⊩ ψ'),
 
     parse_natural_deduction_rule('↔₊', '[φ] ψ, [ψ] φ ⊩ (φ ↔ ψ)'),
-    parse_natural_deduction_rule('↔₋ₗ', '(φ ↔ ψ), φ ⊩ ψ'),
-    parse_natural_deduction_rule('↔₋ᵣ', '(φ ↔ ψ), ψ ⊩ φ'),
+    parse_natural_deduction_rule('↔₋ₗ', '(φ ↔ ψ), ψ ⊩ φ'),
+    parse_natural_deduction_rule('↔₋ᵣ', '(φ ↔ ψ), φ ⊩ ψ'),
 
     parse_natural_deduction_rule('∀₊', 'φ[x ↦ y*] ⊩ ∀x.φ'),
     parse_natural_deduction_rule('∀₋', '∀x.φ ⊩ φ[x ↦ τ]'),

src/notebook/math/logic/deduction/test_proof_tree.py

@@ -117,6 +117,40 @@ def test_efq() -> None:
     )
 
 
+# ex:def:propositional_natural_deduction_systems/efq_vs_dne
+def test_dne() -> None:
+    tree = apply(
+        CLASSICAL_NATURAL_DEDUCTION_SYSTEM['→₊'],
+        prop_premise(
+            tree=apply(
+                CLASSICAL_NATURAL_DEDUCTION_SYSTEM['DNE'],
+                prop_premise(
+                    tree=apply(
+                        CLASSICAL_NATURAL_DEDUCTION_SYSTEM['¬₋'],
+                        prop_assume('¬¬p', 'u'),
+                        prop_assume('¬p', 'v'),
+                    ),
+                    discharge='¬p',
+                    marker='v'
+                )
+            ),
+            discharge='¬¬p',
+            marker='u'
+        )
+    )
+
+    assert str(tree) == dedent('''\
+          [¬¬p]ᵘ    [¬p]ᵛ
+          _______________ ¬₋
+                 ⊥
+        v _______________ DNE
+                 p
+        u _______________ →₊
+             (¬¬p → p)
+        '''
+    )
+
+
 # thm:minimal_implicational_logic_axioms_nd_proof
 def test_implication_distributivity_axiom_tree() -> None:
     tree = apply(

src/notebook/math/logic/theories/boolean/test_axioms.py

@@ -91,7 +91,7 @@ def test_bottom_minimality_proof() -> None:
         CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∀₊'],
         premise(
             tree=apply(
-                CLASSICAL_NATURAL_DEDUCTION_SYSTEM['↔₋ᵣ'],
+                CLASSICAL_NATURAL_DEDUCTION_SYSTEM['↔₋ₗ'],
                 apply(
                     CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∀₋'],
                     premise(
@@ -119,7 +119,7 @@ def test_bottom_minimality_proof() -> None:
            ∀y.((⫫ ≤ y) ↔ ((⫫ ⩓ y) = ⫫))          [∀x.((⫫ ⩓ x) = ⫫)]ᵛ
         __________________________________ ∀₋    ___________________ ∀₋
             ((⫫ ≤ x) ↔ ((⫫ ⩓ x) = ⫫))               ((⫫ ⩓ x) = ⫫)
-        ____________________________________________________________ ↔₋ᵣ
+        ____________________________________________________________ ↔₋ₗ
                                   (⫫ ≤ x)
         ____________________________________________________________ ∀₊
                                  ∀x.(⫫ ≤ x)

text/curry_howard_correspondence.tex

@@ -268,7 +268,7 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
 
   Introducing more complicated types, for example for handling first-order and higher-order logic, is often done, in the tradition established by Per Martin-L\"of, via a stout list of metatheoretic \hyperref[def:inference_rule]{inference rules}. The classification of these rules is described in \cref{rem:type_theory_rule_classification}, and concrete rules extending the Curry-Howard correspondence to higher-order logic are presented in \fullref{sec:dependent_types}.
 
-  Fortunately, for the types we will consider in this section, we will be able to easily reuse the machinery we have built for untyped and simply typed (with only arrow types) \( \muplambda \)-calculus, with some small adjustments. See \cref{rem:product_type_equality_rules} for a more concrete discussion. We will however only limit ourselves to introduction and elimination rules since we will not need the rest. We will avoid introducing judgmental equality rules because we have spent considerable effort ensuring correctness of even \hyperref[def:lambda_term_alpha_equivalence]{\( \alpha \)-equivalence}.
+  Fortunately, for the types we will consider in this section, we will be able to easily reuse the machinery we have built for untyped and simply typed (with only arrow types) \( \muplambda \)-calculus, with some small adjustments. See \cref{rem:simple_product_type_equality_rules} for a more concrete discussion. We will however only limit ourselves to introduction and elimination rules since we will not need the rest. We will avoid introducing judgmental equality rules because we have spent considerable effort ensuring correctness of even \hyperref[def:lambda_term_alpha_equivalence]{\( \alpha \)-equivalence}.
 
   Still, we will still find useful the classification of rules, mostly because of the respective terminology.
 \end{remark}
@@ -375,14 +375,14 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
 \begin{comments}
   \item A treatment of product types within simple type theory can be found in \cite[\S 4.3.1]{Mimram2020ProgramEqualsProof}.
 
-  \item We discuss how equality rules and \( \beta\eta \)-reduction are related in \cref{rem:product_type_equality_rules}.
+  \item We discuss how equality rules and \( \beta\eta \)-reduction are related in \cref{rem:simple_product_type_equality_rules}.
 
   \item This is a binary analogue to the dependent products defined in \cref{def:dependent_product}.
 \end{comments}
 
-\begin{remark}\label{rem:product_type_equality_rules}
+\begin{remark}\label{rem:simple_product_type_equality_rules}
   In \cref{ex:def:beta_eta_reduction/pairs}, we have shown that the \( \muplambda \)-terms \ref{ex:def:beta_eta_reduction/pairs/intro}, \ref{ex:def:beta_eta_reduction/pairs/elim_left} and \ref{ex:def:beta_eta_reduction/pairs/elim_right} enable the following \( \beta \)-reductions:
-  \begin{align}\label{eq:rem:product_type_equality_rules/beta}
+  \begin{align}\label{eq:rem:simple_product_type_equality_rules/beta}
     P_{-L} (P_+ A B) \bred* A
     &&
     \T{and}
@@ -440,13 +440,13 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
   \end{paracol}
 
   There is one important downside related to \( \eta \)-reduction and \hyperref[rem:type_theory_rule_classification/equality/uniq]{uniqueness rules}, however. We could expect that
-  \begin{equation}\label{eq:rem:product_type_equality_rules/eta}
+  \begin{equation}\label{eq:rem:simple_product_type_equality_rules/eta}
     P_+ (P_{-L} M) (P_{-R} A) \redrel*{\beta\eta} A.
   \end{equation}
 
-  \incite*[corr. 1.23]{Barendregt1974SurjectivePairing} demonstrates that there is no triple of untyped \( \muplambda \)-terms \( P_+ \), \( P_{-L} \) and \( P_{+R} \) satisfying \eqref{eq:rem:product_type_equality_rules/eta}.
+  \incite*[corr. 1.23]{Barendregt1974SurjectivePairing} demonstrates that there is no triple of untyped \( \muplambda \)-terms \( P_+ \), \( P_{-L} \) and \( P_{+R} \) satisfying \eqref{eq:rem:simple_product_type_equality_rules/eta}.
 
-  Barendregt calls a triple satisfying \eqref{eq:rem:product_type_equality_rules/beta} a \enquote{pairing}, and a triple additionally satisfying \eqref{eq:rem:product_type_equality_rules/eta} --- a \enquote{surjective pairing}. Thus, his result states that untyped \( \muplambda \)-calculus does not admit a surjective pairing, despite the obvious pairing shown in \cref{ex:def:beta_eta_reduction/pairs}.
+  Barendregt calls a triple satisfying \eqref{eq:rem:simple_product_type_equality_rules/beta} a \enquote{pairing}, and a triple additionally satisfying \eqref{eq:rem:simple_product_type_equality_rules/eta} --- a \enquote{surjective pairing}. Thus, his result states that untyped \( \muplambda \)-calculus does not admit a surjective pairing, despite the obvious pairing shown in \cref{ex:def:beta_eta_reduction/pairs}.
 
   Thus, even for simple types, adding new congruence and uniqueness rules cannot be circumvented by a simpler mechanism such as \( \delta \)-reduction. This will unfortunately require us to reprove all results involving either \( \beta\eta \)-reduction or only \( \alpha \)-equivalence. So, our decision is to avoid new rules and to sacrifice \hyperref[con:extensionality]{extensionality} for the sake of simplicity.
 \end{remark}
@@ -499,7 +499,7 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
 
   \item As with the \hyperref[def:simple_empty_type]{empty type}, unless we make the constants \( \synS_{+L} \) and \( \synS_{+R} \) depend on the types of the terms, we break the type uniqueness for typed terms shown in \cref{thm:typed_term_habitation_uniqueness}. Again, this is a sacrifice for the sake of simplicity of our formalized system.
 
-  \item We discuss how equality rules and \( \beta\eta \)-reduction are related in \cref{rem:sum_type_equality_rules}.
+  \item We discuss how equality rules and \( \beta\eta \)-reduction are related in \cref{rem:simple_sum_type_equality_rules}.
 
   \item This is a binary analogue to the dependent sums defined in \cref{def:dependent_sum}.
 \end{comments}
@@ -522,8 +522,8 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
   \item One downside of our approach is that some recursive tree traversals like that in \fullref{alg:simply_typed_reduction} become much more involved because application terms (i.e. \( M = NK \)) can be produced by a variety of rules. With a dedicated syntax, only \ref{inf:def:arrow_type/elim} is able to produce such terms.
 \end{comments}
 
-\begin{remark}\label{rem:sum_type_equality_rules}
-  Similarly to product types, we can use \( \beta\delta \)-reduction to emulate \hyperref[rem:type_theory_rule_classification/equality/comp]{computation rules}. See \cref{rem:product_type_equality_rules} for a broader discussion of the general idea.
+\begin{remark}\label{rem:simple_sum_type_equality_rules}
+  Similarly to product types, we can use \( \beta\delta \)-reduction to emulate \hyperref[rem:type_theory_rule_classification/equality/comp]{computation rules}. See \cref{rem:simple_product_type_equality_rules} for a broader discussion of the general idea.
 
   In our case, given \( M: \tau \), we have
   \begin{equation*}

text/dependent_types.tex

@@ -834,7 +834,7 @@ \section{Dependent types}\label{sec:dependent_types}
     N[a \mapsto M].
   \end{align*}
 
-  This is the desired result, as discussed in \cref{rem:sum_type_equality_rules}.
+  This is the desired result, as discussed in \cref{rem:simple_sum_type_equality_rules}.
 \end{remark}
 
 \begin{remark}\label{rem:dependent_sum_as_binary_product}

text/first_order_logic.tex

@@ -749,11 +749,17 @@ \section{First-order logic}\label{sec:first_order_logic}
 
     However, as per \cref{rem:model_theory_structure_terminology}, unlike in general institutions, we will refer to structures as \enquote{models} only with respect to a theory.
 
-    We say that \( \mscrX \) is a \term[ru=модель (\cite[2.6.21]{Герасимов2014Вычислимость}), en=model (\cite[def. def.2.2.13(ii)]{Hinman2005Logic})]{model} \hi{of} the set of closed formulas \( \Gamma \) and write \( \mscrX \vDash \Gamma \) if and only if \( \Bracks{\varphi}_\mscrX = T \) for every formula \( \varphi \in \Gamma \).
+    We say that \( \mscrX \) is a \term[ru=модель (\cite[2.6.21]{Герасимов2014Вычислимость}), en=model (\cite[def. def.2.2.13(ii)]{Hinman2005Logic})]{model} \hi{of} the set of closed formulas \( \Gamma \) and write \( \mscrX \vDash \Gamma \) if and only if \( \Bracks{\varphi}_\mscrX = T \) for every (closed) formula \( \varphi \in \Gamma \).
 
     We also say that \( \varphi \) is \term[en=valid (\cite[144]{VanDalen2004LogicAndStructure})]{valid} in \( \mscrX \).
 
-    \thmitem{def:fol_semantics/satisfiable} If \( \Gamma \) has a model, we say that it is \term[ru=выполнимая (формула) (\cite[def. 2.4.1]{Герасимов2014Вычислимость}), en=satisfiable (formula) (\cite[71]{VanDalen2004LogicAndStructure})]{satisfiable}.
+    Via \hyperref[def:fol_implicit_universal_quantification]{implicit universal quantification}, it is possible to extend the model relation to arbitrary formulas, not necessarily closed. Then \( \mscrX \) becomes a model of \( \varphi \) if and only if it is a model if its \hyperref[def:fol_quantifier_closure]{universal closure}.
+
+    \thmitem{def:fol_semantics/satisfaction} Consider some formula \( \varphi \), not necessarily closed. If there exists a structure \( \mscrX \) and a variable assignment \( v \) into \( \mscrX \) such that \( \Bracks{\varphi}_\mscrX^v = \semtop \), we say that \( v \) \term[en=satisfies (\cite[def. 2.1.23(i)]{Hinman2005Logic})]{satisfies} \( \varphi \).
+
+    Thus, \( \mscrX \) satisfies \( \varphi \) if and only if \( \mscrX \) is a model of its \hyperref[def:fol_quantifier_closure]{existential closure}. This coincides with validity in the case where \( \varphi \) is closed.
+
+    We say that \( \varphi \) is \term[ru=выполнимая (формула) (\cite[def. 2.4.1]{Герасимов2014Вычислимость}), en=satisfiable (formula) (\cite[71]{VanDalen2004LogicAndStructure})]{satisfiable} if at least one interpretation satisfies it.
 
     \thmitem{def:fol_semantics/tautology} We call the closed formula \( \varphi \) a \term[ru=тавтология (\cite[def. 2.4.1]{Герасимов2014Вычислимость}), en=tautology (\cite[97]{Hinman2005Logic})]{tautology} if \( \Bracks{\varphi}_\mscrX = \semtop \) for every interpretation \( \mscrX \), and a \term[ru=противоречивая формула (\cite[def. 2.4.1]{Герасимов2014Вычислимость})]{contradiction} if \( \Bracks{\varphi}_\mscrX < \semtop \) for every \( \mscrX \).
 
@@ -885,12 +891,19 @@ \section{First-order logic}\label{sec:first_order_logic}
 \end{remark}
 
 \begin{definition}\label{def:fol_implicit_universal_quantification}\mimprovised
-  We can extend the satisfaction relation from \cref{def:fol_semantics/model} for arbitrary \hyperref[def:fol_formula]{first-order formulas} as follows.
+  We can extend the model relation from \cref{def:fol_semantics/model} for arbitrary \hyperref[def:fol_formula]{first-order formulas} as follows via \hyperref[def:fol_universal_validity]{universal validity}.
 
   In a given \hyperref[def:fol_structure]{structure} \( \mscrX \), let \( \mscrX \vDash \varphi \) if and only if \( \Bracks{\varphi}_\mscrX^v = T \) for every variable assignment \( v \) in \( \mscrX \). Instead of using variable assignments, we can rely on the \hyperref[def:fol_quantifier_closure]{universal closure} of \( \varphi \) by requiring \( \Bracks{\qforall {x_1} \ldots \qforall {x_n} \varphi}_\mscrX = T \). This approach, which we will call \term{implicit universal quantification}, is used in \cite[def. 2.2.1]{Hinman2005Logic} and \cite[94]{Герасимов2014Вычислимость}.
 
   This easily extends to sets of formulas, so we let \( \mscrX \vDash \Gamma \) if and only if \( \mscrX \vDash \psi \) for every \( \psi \) in \( \Gamma \). For the corresponding entailment relation, let \( \Gamma \vDash \varphi \) if and only if \( \mscrX \vDash \varphi \) whenever \( \mscrX \vDash \Gamma \).
 \end{definition}
+\begin{comments}
+  \item We must be careful about using implicit universal quantification for two reasons:
+  \begin{itemize}
+    \item It is incompatible with \fullref{thm:fol_semantic_deduction_theorem}, as shown in \cref{rem:implicit_quantification_and_deduction}.
+    \item It can lead to confusion with implicit existential quantification, which is used in \cref{def:fol_semantics/satisfaction} to generalize satisfaction.
+  \end{itemize}
+\end{comments}
 
 \begin{remark}\label{rem:implicit_quantification_and_deduction}
   For first-order logic, we have defined the \hyperref[def:institution]{institution} in \cref{def:fol_institution} only for \hyperref[def:closed_fol_formula]{closed first-order formulas}. It is tempting to allow formulas with free variables via \hyperref[def:fol_implicit_universal_quantification]{implicit universal quantification}.

text/heyting_algebras.tex

@@ -100,7 +100,7 @@ \section{Heyting algebras}\label{sec:heyting_algebras}
         \mathllap{\synx \rightarrow \synx} \syneq \mathrlap{\top.}
       \end{equation}
 
-      \thmitem{def:heyting_algebra/axioms/modus_ponens} The following variation of \ref{inf:thm:axiomatic_derivation_as_natural_deduction/mp}:
+      \thmitem{def:heyting_algebra/axioms/modus_ponens} The following variation of \ref{inf:def:axiomatic_derivation_as_natural_deduction/mp}:
       \begin{equation}\label{eq:def:heyting_algebra/axioms/modus_ponens}
         \mathllap{\synx \wedge (\synx \rightarrow \syny)} \syneq \mathrlap{\synx \wedge \syny.}
       \end{equation}

text/higher_order_natural_deduction.tex

@@ -364,7 +364,7 @@ \section{Higher-order natural deduction}\label{sec:higher_order_natural_deductio
 \begin{remark}\label{rem:hol_axiomatic_derivations}
   We will outline the proof system of Andrews' \( \logic{Q}_0 \) from \incite[\S 51]{Andrews2002Logic} since it is the most refined of the Church-like systems listed in \cref{rem:higher_order_logic_and_type_theory/types}.
 
-  It is based on \hyperref[def:propositional_axiomatic_derivation_system]{axiomatic derivation systems}, but instead of \ref{inf:thm:axiomatic_derivation_as_natural_deduction/mp}, it features a peculiar rule:
+  It is based on \hyperref[def:propositional_axiomatic_derivation_system]{axiomatic derivation systems}, but instead of \ref{inf:def:axiomatic_derivation_as_natural_deduction/mp}, it features a peculiar rule:
   \begin{displayquote}
     \textit{Rule R}. From \( \mathbf{C} \) and \( \mathbf{A_\alpha} = \mathbf{B_\alpha} \) to infer the result of replacing one occurrence of \( \mathbf{A_\alpha} \) in \( \mathbf{C} \) by an occurrence of \( \mathbf{B_\alpha} \), provided that the occurrence of \( \mathbf{A_\alpha} \) in \( \mathbf{C} \) is not (an occurrence of a variable) immediately preceded by \( \muplambda \).
   \end{displayquote}
@@ -552,7 +552,7 @@ \section{Higher-order natural deduction}\label{sec:higher_order_natural_deductio
 
       \hypo{ [\psi \syniff y^{\syn\omicron}]^w }
       \hypo{ [\psi]^v }
-      \infer2[\ref{inf:def:propositional_natural_deduction_systems/iff/elim_left}]{ y^{\syn\omicron} }
+      \infer2[\ref{inf:def:propositional_natural_deduction_systems/iff/elim_right}]{ y^{\syn\omicron} }
 
       \hypo{ [\psi \syniff y^{\syn\omicron}]^w }
       \infer[left label=\( w \)]2[\ref{inf:def:propositional_natural_deduction_systems/iff/intro}]{ y^{\syn\omicron} \syniff (\psi \syniff y^{\syn\omicron}) }

text/mathematical_logic.tex

@@ -56,7 +56,7 @@ \chapter{Mathematical logic}\label{ch:mathematical_logic}
 
   In such case, it seems reasonable to say that the formula is a \hyperref[con:hypothetical_judgment]{hypothetical judgment} whose hypotheses disambiguate it. This is correct as long as the aforementioned terms are vague, but it is incorrect in the more precise meaning we will consider here.
 
-  The reason for this is that the validity of hypothetical judgments is determined via logical consequence. In the sequent notation from \cref{rem:sequent_notation}, \( \varphi \vdash \psi \) expresses that \( \psi \) is a logical consequence of \( \varphi \). Then, as per \ref{inf:thm:axiomatic_derivation_as_natural_deduction/mp}, if \( \varphi \) is considered true, so is \( \psi \).
+  The reason for this is that the validity of hypothetical judgments is determined via logical consequence. In the sequent notation from \cref{rem:sequent_notation}, \( \varphi \vdash \psi \) expresses that \( \psi \) is a logical consequence of \( \varphi \). Then, as per \ref{inf:def:axiomatic_derivation_as_natural_deduction/mp}, if \( \varphi \) is considered true, so is \( \psi \).
 
   The hypotheses in ambiguous formulas are instead not logical. Such is the case where \( \varphi \) depends on a \hyperref[con:variable_binding]{free variable} \( x \). Disambiguation is then achieved by substituting or binding \( x \), not via logical consequence.
 \end{remark}