Add some notes on proofs with empty domains

Author: v--

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

@@ -67,8 +67,8 @@ def get_open_variables(
             if var not in eigen
         }
 
-    def is_strict(self) -> bool:
-        return True
+    def new_implicit_variables(self) -> Collection[Variable]:
+        return set()
 
     def __str__(self) -> str:
         return self.build_renderer().render()
@@ -193,9 +193,9 @@ def get_open_variables(
     ) -> Collection[Variable]:
         return set(self._iter_open_variables(eigen, discharged))
 
-    def is_strict(self) -> bool:
+    def new_implicit_variables(self) -> Collection[Variable]:
         open_vars = self.get_open_variables()
-        return any(var not in open_vars for var in self.implicit_variables)
+        return {var for var in self.implicit_variables if var not in open_vars}
 
     def __str__(self) -> str:
         return self.build_renderer().render()

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

@@ -9,6 +9,7 @@
     parse_formula_placeholder,
     parse_formula_with_substitution,
     parse_marker,
+    parse_variable,
 )
 from ..propositional import parse_prop_formula
 from ..signature import FormalLogicSignature
@@ -265,6 +266,24 @@ def test_forall_introduction() -> None:
     )
 
 
+# rem:fol_empty_universe/natural_deduction
+def test_forall_elimination(dummy_signature: FormalLogicSignature) -> None:
+    tree = apply(
+        CLASSICAL_NATURAL_DEDUCTION_SYSTEM['∀₋'],
+        assume(parse_formula('∀x.p¹(x)', dummy_signature), parse_marker('u')),
+        conclusion_config=parse_formula_with_substitution('p¹(x)[x ↦ y]', dummy_signature),
+    )
+
+    assert tree.get_open_variables() == set()
+    assert tree.new_implicit_variables() == {parse_variable('y')}
+    assert str(tree) == dedent('''\
+        [∀x.p¹(x)]ᵘ
+        ___________ ∀₋
+           p¹(y)
+        '''
+    )
+
+
 # ex:def:fol_natural_deduction/reintroduction
 def test_forall_reintroduction(dummy_signature: FormalLogicSignature) -> None:
     tree = apply(
@@ -280,7 +299,7 @@ def test_forall_reintroduction(dummy_signature: FormalLogicSignature) -> None:
     )
 
     assert tree.get_open_variables() == set()
-    assert not tree.is_strict()
+    assert tree.new_implicit_variables() == set()
     assert str(tree) == dedent('''\
         [∀x.p¹(x)]ᵘ
         ___________ ∀₋
@@ -305,7 +324,7 @@ def test_forall_reintroduction_with_renaming(dummy_signature: FormalLogicSignatu
     )
 
     assert tree.get_open_variables() == set()
-    assert not tree.is_strict()
+    assert tree.new_implicit_variables() == set()
     assert str(tree) == dedent('''\
         [∀x.p¹(x)]ᵘ
         ___________ ∀₋
@@ -330,7 +349,7 @@ def test_forall_to_exists(dummy_signature: FormalLogicSignature) -> None:
     )
 
     assert tree.get_open_variables() == set()
-    assert not tree.is_strict()
+    assert tree.new_implicit_variables() == set()
     assert str(tree) == dedent('''\
         [∀x.p¹(x)]ᵘ
         ___________ ∀₋
@@ -356,7 +375,7 @@ def test_forall_to_exists_with_constant(dummy_signature: FormalLogicSignature) -
     )
 
     assert tree.get_open_variables() == set()
-    assert not tree.is_strict()
+    assert tree.new_implicit_variables() == set()
     assert str(tree) == dedent('''\
         [∀x.p¹(x)]ᵘ
         ___________ ∀₋

text/first_order_natural_deduction.tex

@@ -477,7 +477,7 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 
     Actually, we will need a more elaborate construction --- a function \( F(D, E) \) depending on a set \( D \) of discharged markers and a set \( E \) of discharged eigenvariables. We call \( F(\varnothing, \varnothing) \) \enquote{the} set of open free variables of the tree.
 
-    \thmitem{def:fol_natural_deduction_proof_tree/implicit_variables} Similarly to implicit open premises, we may also have \term{implicit open variables}. We will call the proof tree \term{strict} if all implicit variables are also explicit open free variables.
+    \thmitem{def:fol_natural_deduction_proof_tree/implicit_variables} Similarly to implicit open premises, we may also have \term{implicit free variables}.
   \end{thmenum}
 
   Just as with assumption discharging, binding variables is also delicate to handle:
@@ -563,7 +563,7 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 
       Thus, have taken the union of all open variables of the subtrees and all free variables of the implicit premises, excluding those discharged at the current application.
 
-      \thmitem{def:fol_natural_deduction_proof_tree/application/implicit_variables} If the conclusion schema features a substitution, i.e. if \( \Psi = \Lambda[\xi \mapsto \Tau] \), let the set of implicit open variables be the set of variables of the term \( \Tau[\BbbI] \). Otherwise, let \( C_d \) be the empty set.
+      \thmitem{def:fol_natural_deduction_proof_tree/application/implicit_variables} If the conclusion schema features a substitution, i.e. if \( \Psi = \Lambda[\xi \mapsto \Tau] \), let the set of implicit free variables be the set of variables of the term \( \Tau[\BbbI] \). Otherwise, let \( C_d \) be the empty set.
     \end{thmenum}
   \end{thmenum}
 \end{definition}
@@ -576,7 +576,7 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 
   \item Even though we do not disallow eigenvariables in the conclusion, they would be treated the same as regular variables.
 
-  \item Implicit variables and strict proof trees are not established concepts. Nonstrict rule application trees, in which the conclusion may introduce new free variables, have some debatable aspects despite being the norm. See \cref{rem:fol_empty_universe/natural_deduction} for a broader discussion.
+  \item Implicit variables are not an established concept. Placing restrictions on them allows us to mitigate some debatable proof trees --- see \cref{rem:fol_empty_universe/natural_deduction} for a broader discussion.
 
   \item The term \enquote{eigenvariable} comes from \tcite{#2, where #1}{Gentzen1935LogischeSchließen} introduces natural deduction. In the corresponding English translation, \cite[293]{Gentzen1964LogicalDeduction}, eigenvariables are instead called \enquote{proper variables}. Both terms are currently used in English (e.g. \incite[\S 5.1.10]{Mimram2020ProgramEqualsProof} uses \enquote{eigenvariable}, while \incite[38]{TroelstraSchwichtenberg2000BasicProofTheory} uses \enquote{proper variable}).
 
@@ -927,11 +927,25 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 
   This derivation is not sound in an empty universe where nothing exists. Nevertheless, the standard treatment of natural deduction ignores this issue --- starting from Gentzen's \cite[186]{Gentzen1935LogischeSchließen}, and including \cite[ch. 2]{TroelstraSchwichtenberg2000BasicProofTheory}, \cite[\S 2.8]{VanDalen2004LogicAndStructure} and \cite[97]{КолмогоровДрагалин2006Логика}.
 
-  \incite*[\S 5.1.10]{Mimram2020ProgramEqualsProof} provides a hint at how to handle this situation. We have adapted his remarks when introducing strict proof trees in \cref{def:fol_natural_deduction_proof_tree/implicit_variables}. Since the only open assumption above has no free variables, the application of \ref{inf:def:fol_natural_deduction/forall/elim} is strict only if \( \tau \) is closed. This is the case when \( \tau \) contains at least one individual constant. But if the signature has an individual constant, its domain cannot be empty.
+  There are some ad-hoc ways to prevent the above rule applications:
+  \begin{thmenum}
+    \thmitem{rem:fol_empty_universe/restricted_implicit} We may require all \hyperref[def:fol_natural_deduction_proof_tree/implicit_variables]{implicit free variables} to belong to the existing \hyperref[def:fol_natural_deduction_proof_tree/open_variables]{open free variables}. This would affect the rule \ref{inf:def:fol_natural_deduction/forall/elim}. It would be possible to derive \( \varphi[x \mapsto \tau] \) from \( \qforall x \varphi \), but only if the free variables of \( \tau \) are open in the proof tree.
+
+    In our example, the proof tree has no variables open, thus \( \tau \) must use constants rather than variables. But if the signature has an individual constant, its domain cannot be empty. If, on the other hand, the domain is empty, the rule becomes inapplicable.
+
+    On the other hand, this restriction would prevent the following sound proof
+    \begin{equation*}
+      \begin{prooftree}
+        \hypo{ [\qforall x p(x)]^u }
+        \infer1[\ref{inf:def:fol_natural_deduction/forall/elim}]{ p(y) }
+        \infer1[\ref{inf:def:fol_natural_deduction/forall/intro}]{ \qforall z p(z) }
+      \end{prooftree}
+    \end{equation*}
 
-  If, on the other hand, the domain is empty, the rule is inapplicable. Strict proof trees require us to be more careful with the choice of conclusion of \ref{inf:def:fol_natural_deduction/forall/elim}. However, this makes them compatible with empty universes.
+    \thmitem{rem:fol_empty_universe/non_eigenvariable} An alternative is suggested by \incite[\S 5.1.10]{Mimram2020ProgramEqualsProof}. He allows implicit variables to be used at most once in non-eigenvariable substitutions. In our example, this allows the application of \ref{inf:def:fol_natural_deduction/forall/elim}, but not that of \ref{inf:def:fol_natural_deduction/exists/intro}.
 
-  Due to the increased complexity, we will not further pursue this path.
+    Unlike the solution above, this one does not prevent us from applying \ref{inf:def:fol_natural_deduction/forall/intro} instead because the restriction is only for non-eigenvariable substitutions.
+  \end{thmenum}
 \end{remark}
 
 \begin{remark}\label{rem:sequent_calculus_eigenvariables}