Soundness of natural deduction for first-order logic

Author: v--

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

@@ -201,22 +201,63 @@ def __str__(self) -> str:
         return self.build_renderer().render()
 
 
-def apply(  # noqa: C901,PLR0915
+def _infer_application_instantiation(
     rule: NaturalDeductionRule,
-    *args: ProofTree | RuleApplicationPremiseConfig,
+    application_premises: Sequence[RuleApplicationPremiseConfig],
     instantiation: AtomicLogicSchemaInstantiation | None = None,
     implicit: Mapping[FormulaPlaceholder, Formula] | None = None,
     conclusion_config: FormulaWithSubstitution | None = None
-) -> RuleApplicationTree:
-    if len(args) != len(rule.premises):
-        raise RuleApplicationError(f'The rule {rule.name} has {len(rule.premises)} premises, but the application has {len(args)}')
-
+) -> AtomicLogicSchemaInstantiation:
     if instantiation is None:
         instantiation = AtomicLogicSchemaInstantiation(formula_mapping=implicit)
     elif implicit:
         raise RuleApplicationError('Cannot provide both an instantiation and implicit assumptions')
 
-    marker_map = dict[Marker, Formula]()
+    # Infer instantiation
+    for rule_premise, application_premise in zip(rule.premises, application_premises, strict=True):
+        for attachment_schema, attachment in zip(rule_premise.attachments, application_premise.attachments, strict=True):
+            if attachment:
+                instantiation |= infer_instantiation_from_formula_substitution_spec(
+                    attachment_schema,
+                    attachment.payload
+                )
+
+        if application_premise.main:
+            if rule_premise.main.sub is None:
+                instantiation |= infer_instantiation_from_formula(
+                    rule_premise.main.formula,
+                    evaluate_substitution(application_premise.main),
+                )
+            else:
+                instantiation |= infer_instantiation_from_formula_substitution_spec(
+                    rule_premise.main,
+                    application_premise.main,
+                )
+
+    if rule.conclusion.main.sub:
+        if conclusion_config is None:
+            raise RuleApplicationError(f'The rule {rule.name} requires a conclusion with an explicit substitution')
+
+        instantiation |= infer_instantiation_from_formula_substitution_spec(rule.conclusion.main, conclusion_config)
+
+    for attachment_schema in rule.conclusion.attachments:
+        try:
+            instantiate_substitution(attachment_schema, instantiation)
+        except SchemaInstantiationError as err:
+            raise RuleApplicationError(f'Cannot instantiate the implicit premise {attachment_schema} of the rule {rule.name}') from err
+
+    return instantiation
+
+
+def apply(  # noqa: C901
+    rule: NaturalDeductionRule,
+    *args: ProofTree | RuleApplicationPremiseConfig,
+    instantiation: AtomicLogicSchemaInstantiation | None = None,
+    implicit: Mapping[FormulaPlaceholder, Formula] | None = None,
+    conclusion_config: FormulaWithSubstitution | None = None
+) -> RuleApplicationTree:
+    if len(args) != len(rule.premises):
+        raise RuleApplicationError(f'The rule {rule.name} has {len(rule.premises)} premises, but the application has {len(args)}')
 
     application_premises = [
         premise_config(tree=premise_arg, attachments=[None] * len(rule_premise.attachments))
@@ -225,6 +266,17 @@ def apply(  # noqa: C901,PLR0915
         for rule_premise, premise_arg in zip(rule.premises, args, strict=True)
     ]
 
+    instantiation = _infer_application_instantiation(
+        rule, application_premises, instantiation, implicit, conclusion_config
+    )
+
+    marker_map = dict[Marker, Formula]()
+
+    if conclusion_config is None:
+        conclusion_config = instantiate_substitution(rule.conclusion.main, instantiation)
+
+    conclusion = evaluate_substitution(conclusion_config)
+
     for i, (rule_premise, application_premise) in enumerate(zip(rule.premises, application_premises, strict=True), start=1):
         for assumption in application_premise.tree.get_cumulative_assumptions():
             if assumption.marker is None:
@@ -245,6 +297,9 @@ def apply(  # noqa: C901,PLR0915
             if not application_premise.main.sub.is_noop() and eigen in get_formula_free_variables(application_premise.main.formula):
                 raise RuleApplicationError(f'The eigenvariable {eigen} of the unsubstituted premise conclusion {application_premise.main.formula} cannot be free in it')
 
+            if eigen in get_formula_free_variables(conclusion):
+                raise RuleApplicationError(f'The attached formula eigenvariable {eigen} cannot be free in the conclusion {conclusion} of the rule {rule.name}')
+
             if eigen in application_premise.tree.get_open_variables():
                 raise RuleApplicationError(f'The eigenvariable {eigen} cannot be free in the derivation of {application_premise.tree.conclusion}')
 
@@ -274,44 +329,11 @@ def apply(  # noqa: C901,PLR0915
                 if eigen in application_premise.tree.get_open_variables(discharged={attachment.marker}):
                     raise RuleApplicationError(f'The eigenvariable {eigen} cannot be free in the derivation of {app_conclusion}, except possibly in {attachment.eval()}')
 
-            # Update instantiation
-            instantiation |= infer_instantiation_from_formula_substitution_spec(
-                attachment_schema,
-                attachment.payload
-            )
-
-        if application_premise.main:
-            if rule_premise.main.sub is None:
-                instantiation |= infer_instantiation_from_formula(
-                    rule_premise.main.formula,
-                    evaluate_substitution(application_premise.main),
-                )
-            else:
-                instantiation |= infer_instantiation_from_formula_substitution_spec(
-                    rule_premise.main,
-                    application_premise.main,
-                )
-
-    if rule.conclusion.main.sub:
-        if conclusion_config is None:
-            raise RuleApplicationError(f'The rule {rule.name} requires a conclusion with an explicit substitution')
-
-        instantiation |= infer_instantiation_from_formula_substitution_spec(rule.conclusion.main, conclusion_config)
-
-    for attachment_schema in rule.conclusion.attachments:
-        try:
-            instantiate_substitution(attachment_schema, instantiation)
-        except SchemaInstantiationError as err:
-            raise RuleApplicationError(f'Cannot instantiate the implicit premise {attachment_schema} of the rule {rule.name}') from err
-
-    if conclusion_config is None:
-        conclusion_config = instantiate_substitution(rule.conclusion.main, instantiation)
-
     return RuleApplicationTree(
         rule,
         instantiation,
         [premise.eval() for premise in application_premises],
-        evaluate_substitution(conclusion_config),
+        conclusion,
         get_term_variables(conclusion_config.sub.dest) if conclusion_config.sub else set()
     )
 

text/first_order_logic.tex

@@ -1002,7 +1002,7 @@ \section{First-order logic}\label{sec:first_order_logic}
 \end{definition}
 
 \begin{definition}\label{def:fol_universal_validity}\mcite[105]{Hinman2005Logic}
-  If, for some \hyperref[def:fol_formula]{first-order formula} \( \varphi \) and some \hyperref[def:fol_structure]{first-order structure} \( \mscrX \), the \hyperref[alg:fol_formula_denotation]{denotation} \( \Bracks{ \varphi }_\mscrX^v \) equals \( \semtop \) for any variable assignment \( v \) in \( \mscrX \), we say that \( \varphi \) is \term[ru=общезначимая (формула) (\cite[def. 2.4.1]{Герасимов2014Вычислимость})]{universally valid} in \( \mscrX \).
+  If, in some \hyperref[def:fol_structure]{first-order structure} \( \mscrX \), every \hyperref[def:fol_variable_assignment]{variable assignment} \( v \) \hyperref[def:fol_semantics/satisfaction]{satisfies} the formula \( \varphi \), we say that \( \varphi \) is \term[ru=общезначимая (формула) (\cite[def. 2.4.1]{Герасимов2014Вычислимость})]{universally valid} in \( \mscrX \).
 \end{definition}
 \begin{comments}
   \item \hyperref[def:closed_fol_formula]{Closed formulas} are universally valid, but the notion is more general --- see \cref{rem:implicit_quantification_and_deduction}.

text/first_order_models.tex

@@ -252,7 +252,7 @@ \section{First-order models}\label{sec:first_order_models}
 \begin{proposition}\label{thm:functions_over_model_form_model}
   Let \( \Gamma \) to be a set of closed \hyperref[def:positive_formula]{positive formulas} \hi{without existential quantifiers}. Let \( \mscrX = (X, I) \) be a model of \( \Gamma \) and let \( A \) be a nonempty \hyperref[def:set]{plain set}, possibly unrelated to \( \mscrX \). Consider the set \( Y \coloneqq \fun(A, \mscrX) \) of \hyperref[def:function]{all set functions} from \( A \) to \( X \).
 
-  Define \( \iota: X \mapsto Y \) by sending each \( x \in X \) to the corresponding constant function in \( Y \).
+  Define \( \iota: X \to Y \) by sending each \( x \in X \) to the corresponding constant function in \( Y \).
 
   Define the interpretation \( J \) as follows:
   \begin{itemize}