Merge pull request #7 from DigitalFormalLogic/feat/nd-fol

FEAT: Natural deduction for first-order logic

Author: ozekik

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.

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"]

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"<NDSubproof name='{str(self.name)}' children={[self.children]}>"
+
+    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):