Describe higher-order logic proof tree in more detail

Author: v--

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

@@ -23,6 +23,15 @@
 from .system import NaturalDeductionPremise, NaturalDeductionRule
 
 
+@dataclass(frozen=True)
+class MarkedVariable:
+    var: Variable
+    marker: Marker
+
+    def __str__(self) -> str:
+        return f'{self.var}: {self.marker}'
+
+
 @dataclass(frozen=True)
 class AssumptionTree(InferenceTree[FormulaWithSubstitution, Mapping[Marker, Formula]]):
     conclusion: FormulaWithSubstitution
@@ -46,6 +55,12 @@ def build_renderer(self, *, conclusion: FormulaWithSubstitution | None = None) -
     def get_free_variables(self) -> Collection[Variable]:
         return get_free_variables(evaluate_substitution_spec(self.conclusion))
 
+    def get_marked_free_variables(self) -> Collection[MarkedVariable]:
+        return {
+            MarkedVariable(var, self.marker)
+            for var in self.get_free_variables()
+        }
+
     def __str__(self) -> str:
         return self.build_renderer().render()
 
@@ -178,7 +193,7 @@ def _filter_assumptions(self, *, discharged_at_current_step: bool) -> Iterable[t
             for marker, assumption in application_premise.tree.get_assumption_map().items():
                 is_discharged_at_current_step = application_premise.discharge is not None and \
                     evaluate_substitution_spec(application_premise.discharge) == assumption and \
-                    (application_premise.marker is None or application_premise.marker == marker)
+                    application_premise.marker == marker
 
                 if discharged_at_current_step == is_discharged_at_current_step:
                     yield marker, assumption
@@ -223,19 +238,17 @@ def build_renderer(self, *, conclusion: FormulaWithSubstitution | None = None) -
             [premise.build_renderer() for premise in self.premises]
         )
 
-    def iter_free_variables(self) -> Iterable[Variable]:
-        for rule_premise, application_premise in zip(self.rule.premises, self.premises, strict=True):
-            if application_premise.discharge:
-                continue
+    def get_marked_free_variables(self) -> Iterable[MarkedVariable]:
+        discharged_markers = self.get_marker_context()
+        discharged_eigen = {evar.var for evar in self.get_eigenvariable_context()}
 
-            eigen = get_main_eigenvariable(rule_premise, application_premise)
-
-            for var in application_premise.tree.get_free_variables():
-                if var != eigen:
-                    yield var
+        for application_premise in self.premises:
+            for mvar in application_premise.tree.get_marked_free_variables():
+                if mvar.marker not in discharged_markers and mvar.var not in discharged_eigen:
+                    yield mvar
 
     def get_free_variables(self) -> Collection[Variable]:
-        return set(self.iter_free_variables())
+        return {mvar.var for mvar in self.get_marked_free_variables()}
 
     def __str__(self) -> str:
         return self.build_renderer().render()

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

@@ -54,7 +54,8 @@ def test_single_implication_intro() -> None:
         CLASSICAL_NATURAL_DEDUCTION_SYSTEM['→₊'],
         prop_premise(
             tree=prop_assume('q', 'u'),
-            discharge='p'
+            discharge='p',
+            marker='u'
         )
     )
 
@@ -340,17 +341,20 @@ def test_forall_negation(dummy_signature: FormalLogicSignature) -> None:
                                                 ),
                                             )
                                         ),
-                                        discharge=v
+                                        discharge=v,
+                                        marker=parse_marker('v')
                                     )
                                 ),
                                 main_noop_sub=parse_variable('x')
                             )
                         )
                     ),
-                    discharge=u
+                    discharge=u,
+                    marker=parse_marker('u')
                 )
             ),
-            discharge=w
+            discharge=w,
+            marker=parse_marker('w')
         )
     )
 
@@ -418,6 +422,7 @@ def test_exists_elimination(dummy_signature: FormalLogicSignature) -> None:
                 assume(w, parse_marker('w')),  # We avoid discharging w here
             ),
             discharge=parse_formula_with_substitution('p₁(x)[x ↦ y]', dummy_signature),  # So that we can discharge it here
+            marker=parse_marker('w')
         ),
     )
 

text/curry_howard_correspondence.tex

@@ -13,7 +13,7 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
 
   Haskell Curry is credited for the realization that, in modern terms, the \hyperref[def:arrow_type]{arrow type} \( \tau \synimplies \rho \) can be regarded as a \hyperref[def:propositional_alphabet/connectives/conditional]{conditional formula}. In this section will extend this to \hyperref[def:simple_algebraic_types]{simple algebraic types}.
 
-  William Howard is credited for extending this analogy to \hyperref[sec:first_order_logic]{first-order logic} via what are now called \enquote{dependent types}. We discuss these extensions in \fullref{sec:higher_order_logic}.
+  William Howard is credited for extending this analogy to \hyperref[sec:first_order_logic]{first-order logic} via what are now called \enquote{dependent types}. We discuss some of these extensions in \fullref{sec:dependent_types}.
 
   Honoring Curry and Howard, we will refer to the overall identification of types and formulas as the \term[en=Curry-Howard correspondence (\cite[def. 4.1.7]{Mimram2020ProgramEqualsProof})]{Curry-Howard correspondence}.