From e8d8f453ff9cb8f4824d37bf630d8a04eb26430a Mon Sep 17 00:00:00 2001 From: Kentaro Ozeki <32771324+ozekik@users.noreply.github.com> Date: Fri, 12 Dec 2025 00:00:00 +0900 Subject: [PATCH] feat: natural deduction for first-order logic --- docs/usage/natural-deduction.md | 25 ++ .../deduction/natural_deduction/__init__.py | 5 +- .../natural_deduction/natural_deduction.py | 17 +- mathesis/deduction/natural_deduction/rules.py | 276 +++++++++++++++--- 4 files changed, 279 insertions(+), 44 deletions(-) diff --git a/docs/usage/natural-deduction.md b/docs/usage/natural-deduction.md index d9ab296..249b10a 100644 --- a/docs/usage/natural-deduction.md +++ b/docs/usage/natural-deduction.md @@ -36,6 +36,31 @@ deriv.apply(deriv[25], rules.Disjunction.Intro("right")) print(deriv.tree()) ``` +## First-order Quantifiers + +First-order rules are available through dedicated `rules.Universal` and `rules.Particular` classes. Just as in standard textbooks, instantiations use a concrete term while generalizations require fresh terms that do not occur elsewhere in the branch. + +```python exec="1" result="text" source="material-block" +from mathesis.grammars import BasicGrammar +from mathesis.deduction.natural_deduction import NDTree, rules + +grammar = BasicGrammar() + +premises = grammar.parse(["∀x(P(x)→Q(x))", "∃x P(x)"]) +conclusion = grammar.parse("∃x Q(x)") + +deriv = NDTree(premises, conclusion) +print(deriv.tree()) + +deriv.apply(deriv[2], rules.Particular.Elim("a")) +deriv.apply(deriv[5], rules.Universal.Elim("a")) +deriv.apply(deriv[8], rules.Conditional.Elim()) +deriv.apply(deriv[24], rules.Particular.Intro("a")) + +print(deriv.tree()) +print(deriv.tree(style="gentzen")) +``` + ## Render as Gentzen-style Proof (WIP) Mathesis has an experimental support for rendering a natural deduction proof as a Gentzen-style proof or its LaTeX code. diff --git a/mathesis/deduction/natural_deduction/__init__.py b/mathesis/deduction/natural_deduction/__init__.py index 69768c8..345fb73 100644 --- a/mathesis/deduction/natural_deduction/__init__.py +++ b/mathesis/deduction/natural_deduction/__init__.py @@ -1 +1,4 @@ -from mathesis.deduction.natural_deduction.natural_deduction import NDTree # noqa +from mathesis.deduction.natural_deduction import rules +from mathesis.deduction.natural_deduction.natural_deduction import NDTree + +__all__ = ["rules", "NDTree"] diff --git a/mathesis/deduction/natural_deduction/natural_deduction.py b/mathesis/deduction/natural_deduction/natural_deduction.py index bb84eaa..c91abb0 100644 --- a/mathesis/deduction/natural_deduction/natural_deduction.py +++ b/mathesis/deduction/natural_deduction/natural_deduction.py @@ -18,7 +18,9 @@ class NDSequentItem(SequentItem): class NDSubproof(NodeMixin): derived_by: natural_deduction.rules.Rule | None - def __init__(self, item: SequentItem, *, parent=None, children=[]) -> None: + def __init__( + self, item: SequentItem, *, parent=None, children: list[NDSubproof] = [] + ) -> None: super().__init__() self.name = item self.item = item @@ -27,6 +29,12 @@ def __init__(self, item: SequentItem, *, parent=None, children=[]) -> None: self.derived_by = None + def __str__(self): + return f"" + + def __repr__(self): + return self.__str__() + class NDTree: """A natural deduction proof tree.""" @@ -41,12 +49,15 @@ def __init__(self, premises: list[Formula], conclusion: Formula): self.bookkeeper = self._sequent_tree.bookkeeper self.counter = self._sequent_tree.counter - # Proof tree + ## Proof tree + # Premises have empty child subproof for item in self._sequent_tree.root.left: item.subproof = NDSubproof(item, children=[]) + # Conclusion has premises as child subproofs self._sequent_tree.root.right[0].subproof = NDSubproof( self._sequent_tree.root.right[0], - children=[item.subproof for item in self._sequent_tree.root.left], + # children=[item.subproof for item in self._sequent_tree.root.left], + children=[], ) def __getitem__(self, index): diff --git a/mathesis/deduction/natural_deduction/rules.py b/mathesis/deduction/natural_deduction/rules.py index 9819f46..8c94c07 100644 --- a/mathesis/deduction/natural_deduction/rules.py +++ b/mathesis/deduction/natural_deduction/rules.py @@ -9,26 +9,53 @@ def _apply(target, new_items, counter, preserve_target=True): + """Add new items to a sequent, cloning existing items as needed.""" + branch_items = new_items new_target = None for item in target.sequent.items: if item != target or preserve_target: node = item.clone() + node.subproof = item.subproof node.n = next(counter) if item == target: - new_target = node + pass branch_items.append(node) branch_sequent = Sequent([], [], parent=target.sequent) branch_sequent.items = branch_items + # NOTE: Connect the subproofs + branch_sequent.right[0].subproof = target.sequent.right[0].subproof + if preserve_target: return branch_sequent, target else: return branch_sequent +def _instantiate_quantifier_body(quantifier, replacing_term: str): + subfml = quantifier.sub.clone() + subfml = subfml.replace_term(quantifier.variable, replacing_term) + return subfml + + +def _collect_branch_terms(sequent): + terms = set() + current = sequent + while current is not None: + for item in current.items: + terms.update(item.fml.free_terms) + current = current.parent + return terms + + +def _ensure_fresh_term(term: str, sequent): + branch_terms = _collect_branch_terms(sequent) + assert term not in branch_terms, "The chosen term already appears in this branch" + + class Rule: label: str latex_label: str @@ -264,16 +291,16 @@ def apply(self, target: SequentItem, counter=count(1)): elif self.conjunct == "right": item = SequentItem(conj2, sign=sign.POSITIVE, n=next(counter)) - sq1, target = _apply(target, [item], counter) - # sq2 = Sequent([target], [item], parent=target.sequent) - - # Subproof + # Attach a new subproof node item.subproof = NDSubproof( item, - children=[target.subproof], + children=[deepcopy(target.subproof)], parent=target.sequent.right[0].subproof, ) + sq1, target = _apply(target, [item], counter) + # sq2 = Sequent([target], [item], parent=target.sequent) + return { "queue_items": [sq1], "counter": counter, @@ -425,56 +452,225 @@ def apply(self, target: SequentItem, counter=count(1)): assert isinstance(target.fml, forms.Conditional), "Not a conditional" target.sequent.derived_by = self - target.subproof.derived_by = self antec, conseq = target.fml.subs - branches = [] - antec = SequentItem(antec, sign=sign.NEGATIVE, n=next(counter)) - sequent, _target_antec = _apply(target, [antec], counter) - # TODO: This is a unnecesarilly complex way to do this - # TODO: Fix dropped numbering - new_items = [] - for item in sequent.items: - if item.sign == sign.POSITIVE or item.fml == antec.fml: - new_items.append(item) - sequent.items = new_items - - if sequent.tautology(): - antec.subproof = NDSubproof(antec) - else: - antec.subproof = NDSubproof( - antec, children=deepcopy(target.sequent.right[0].subproof.children) - ) + # antec.subproof = NDSubproof( + # antec, + # children=[], + # parent=target.sequent.right[0].subproof, + # ) - branches.append(sequent) + sq1, _target_antec = _apply(target, [antec], counter) conseq = SequentItem(conseq, sign=sign.POSITIVE, n=next(counter)) - sequent, _target_conseq = _apply(target, [conseq], counter) - # NOTE: Connect the subproofs - sequent.right[0].subproof = target.sequent.right[0].subproof + # Attach a new subproof node + conseq.subproof = NDSubproof( + conseq, + children=[], + parent=target.sequent.right[0].subproof, + ) + conseq.subproof.derived_by = self + + target.subproof.parent = conseq.subproof - branches.append(sequent) + for item in sq1.items: + if item.sign == sign.POSITIVE and item.fml == antec.fml: + antec.subproof = item.subproof + break - new_subproof_antec = antec.subproof - new_subproof_conditional = deepcopy(target.subproof) + antec.subproof.parent = conseq.subproof - new_subproofs = [ - new_subproof_antec, - new_subproof_conditional, - ] + sq2, _target_conseq = _apply(target, [conseq], counter) - # TODO: Parent must be all right items - conseq.subproof = NDSubproof( - conseq, + if sq2.tautology(): + target.sequent.right[0].subproof.children = conseq.subproof.children + conseq.subproof.parent = None + + branches = [sq1, sq2] + + return { + "queue_items": branches, + "counter": counter, + } + + +class Universal: + class Intro(IntroductionRule): + label = "∀I" + latex_label = r"$\forall$I" + + def __init__(self, generalizing_term: str): + self.generalizing_term = generalizing_term + + def apply(self, target: SequentItem, counter=count(1)): + assert target.sign == sign.NEGATIVE, "Cannot apply introduction rule" + assert isinstance(target.fml, forms.Universal), "Not a universal formula" + + _ensure_fresh_term(self.generalizing_term, target.sequent) + + target.sequent.derived_by = self + target.subproof.derived_by = self + + instantiated = _instantiate_quantifier_body( + target.fml, self.generalizing_term + ) + instantiated_item = SequentItem( + instantiated, + sign=sign.NEGATIVE, + n=next(counter), + ) + instantiated_item.subproof = NDSubproof( + instantiated_item, + children=[target.subproof], + ) + + sequent = _apply( + target, [instantiated_item], counter, preserve_target=False + ) + + # if sequent.tautology(): + # left_item = next( + # filter( + # lambda x: str(x.fml) == str(instantiated_item.fml), + # sequent.left, + # ), + # None, + # ) + # if left_item is not None: + # instantiated_item.subproof.children = left_item.subproof.children + + # target.subproof.children = [deepcopy(instantiated_item.subproof)] + + return { + "queue_items": [sequent], + "counter": counter, + } + + class Elim(EliminationRule): + label = "∀E" + latex_label = r"$\forall$E" + + def __init__(self, replacing_term: str): + self.replacing_term = replacing_term + + def apply(self, target: SequentItem, counter=count(1)): + assert target.sign == sign.POSITIVE, "Cannot apply elimination rule" + assert isinstance(target.fml, forms.Universal), "Not a universal formula" + + target.sequent.derived_by = self + # target.subproof.derived_by = self + + instantiated = _instantiate_quantifier_body(target.fml, self.replacing_term) + instantiated_item = SequentItem( + instantiated, + sign=sign.POSITIVE, + n=next(counter), + ) + + instantiated_item.subproof = NDSubproof( + instantiated_item, + children=[target.subproof], parent=target.sequent.right[0].subproof, - children=new_subproofs, ) + instantiated_item.subproof.derived_by = self + + sequent, target = _apply(target, [instantiated_item], counter) return { - "queue_items": branches, + "queue_items": [sequent], + "counter": counter, + } + + +class Particular: + class Intro(IntroductionRule): + label = "∃I" + latex_label = r"$\exists$I" + + def __init__(self, witness_term: str): + self.witness_term = witness_term + + def apply(self, target: SequentItem, counter=count(1)): + assert target.sign == sign.NEGATIVE, "Cannot apply introduction rule" + assert isinstance( + target.fml, forms.Particular + ), "Not an existential formula" + + target.sequent.derived_by = self + target.subproof.derived_by = self + + instantiated = _instantiate_quantifier_body(target.fml, self.witness_term) + instantiated_item = SequentItem( + instantiated, + sign=sign.NEGATIVE, + n=next(counter), + ) + instantiated_item.subproof = NDSubproof( + instantiated_item, + children=[target.subproof], + ) + + sequent = _apply( + target, [instantiated_item], counter, preserve_target=False + ) + + # if sequent.tautology(): + # left_item = next( + # filter( + # lambda x: str(x.fml) == str(instantiated_item.fml), + # sequent.left, + # ), + # None, + # ) + # if left_item is not None: + # instantiated_item.subproof.children = left_item.subproof.children + + return { + "queue_items": [sequent], + "counter": counter, + } + + class Elim(EliminationRule): + label = "∃E" + latex_label = r"$\exists$E" + + def __init__(self, generalizing_term: str): + self.generalizing_term = generalizing_term + + def apply(self, target: SequentItem, counter=count(1)): + assert target.sign == sign.POSITIVE, "Cannot apply elimination rule" + assert isinstance( + target.fml, forms.Particular + ), "Not an existential formula" + + _ensure_fresh_term(self.generalizing_term, target.sequent) + + target.sequent.derived_by = self + # target.subproof.derived_by = self + + instantiated = _instantiate_quantifier_body( + target.fml, self.generalizing_term + ) + instantiated_item = SequentItem( + instantiated, + sign=sign.POSITIVE, + n=next(counter), + ) + + instantiated_item.subproof = NDSubproof( + instantiated_item, + children=[target.subproof], + parent=target.sequent.right[0].subproof, + ) + instantiated_item.subproof.derived_by = self + + sq, target = _apply(target, [instantiated_item], counter) + + return { + "queue_items": [sq], "counter": counter, }