Skip to content

Proof in Natural Deduction

Introduction

In Mathesis, a state of a natural deduction proof (and its subproofs) consists of the premises and the conclusion that are available to the (sub)proof at a given step. A state is displayed as <premises> ⇒ <conclusion>.

Intuitively, the formulas on the left side of ⇒ are what to come to the upper part of the final (sub)proof, and those on the right side of ⇒ are what to come to the lower part of the final (sub)proof.

Natural deduction is a proof system that consists of elimination rules and introduction rules. In Mathesis,

  • you can apply an elimination rule up-to-down to the premises of a (sub)proof to obtain new premises.
  • Similarly, you can apply an introduction rule down-to-up to the conclusion of a (sub)proof and convert it into new subproofs.
from mathesis.grammars import BasicGrammar
from mathesis.deduction.natural_deduction import NDTree, rules

grammar = BasicGrammar()

premises = grammar.parse(["A∨B", "B→C"])
conclusion = grammar.parse("A∨C")
deriv = NDTree(premises, conclusion)
print(deriv.tree())

deriv.apply(deriv[1], rules.Disjunction.Elim())
print(deriv.tree())

deriv.apply(deriv[8], rules.Disjunction.Intro("left"))
print(deriv.tree())

deriv.apply(deriv[10], rules.Conditional.Elim())
print(deriv.tree())

deriv.apply(deriv[25], rules.Disjunction.Intro("right"))
print(deriv.tree())

A ∨ B 1, B → C 2 ⇒ A ∨ C 3

A ∨ B 1, B → C 2 ⇒ A ∨ C 3 [∨E]
├── A 4, A ∨ B 6, B → C 7 ⇒ A ∨ C 8
└── B 5, A ∨ B 9, B → C 10 ⇒ A ∨ C 11

A ∨ B 1, B → C 2 ⇒ A ∨ C 3 [∨E]
├── A 4, A ∨ B 6, B → C 7 ⇒ A ∨ C 8 [∨I]
│   └── A 13, A ∨ B 14, B → C 15 ⇒ A 12
└── B 5, A ∨ B 9, B → C 10 ⇒ A ∨ C 11

A ∨ B 1, B → C 2 ⇒ A ∨ C 3 [∨E]
├── A 4, A ∨ B 6, B → C 7 ⇒ A ∨ C 8 [∨I]
│   └── A 13, A ∨ B 14, B → C 15 ⇒ A 12
└── B 5, A ∨ B 9, B → C 10 ⇒ A ∨ C 11 [→E]
    ├── B 17, A ∨ B 18, B → C 19 ⇒ B 16
    └── C 21, B 22, A ∨ B 23, B → C 24 ⇒ A ∨ C 25

A ∨ B 1, B → C 2 ⇒ A ∨ C 3 [∨E]
├── A 4, A ∨ B 6, B → C 7 ⇒ A ∨ C 8 [∨I]
│   └── A 13, A ∨ B 14, B → C 15 ⇒ A 12
└── B 5, A ∨ B 9, B → C 10 ⇒ A ∨ C 11 [→E]
    ├── B 17, A ∨ B 18, B → C 19 ⇒ B 16
    └── C 21, B 22, A ∨ B 23, B → C 24 ⇒ A ∨ C 25 [∨I]
        └── C 27, B 28, A ∨ B 29, B → C 30 ⇒ C 26

First-order logic

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.

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

∀x(P(x) → Q(x)) 1, ∃xP(x) 2 ⇒ ∃xQ(x) 3

∀x(P(x) → Q(x)) 1, ∃xP(x) 2 ⇒ ∃xQ(x) 3 [∃E]
└── P(a) 4, ∀x(P(x) → Q(x)) 5, ∃xP(x) 6 ⇒ ∃xQ(x) 7 [∀E]
    └── P(a) → Q(a) 8, P(a) 9, ∀x(P(x) → Q(x)) 10, ∃xP(x) 11 ⇒ ∃xQ(x) 12 [→E]
        ├── P(a) → Q(a) 14, P(a) 15, ∀x(P(x) → Q(x)) 16, ∃xP(x) 17 ⇒ P(a) 13
        └── Q(a) 19, P(a) → Q(a) 20, P(a) 21, ∀x(P(x) → Q(x)) 22, ∃xP(x) 23 ⇒ ∃xQ(x) 24 [∃I]
            └── Q(a) 26, P(a) → Q(a) 27, P(a) 28, ∀x(P(x) → Q(x)) 29, ∃xP(x) 30 ⇒ Q(a) 25

∃xQ(x) [∃E]
├── ∃xP(x)
└── ∃xQ(x) [∃I]
    └── Q(a) [→E]
        ├── P(a) → Q(a) [∀E]
        │   └── ∀x(P(x) → Q(x))
        └── P(a)

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.

from mathesis.grammars import BasicGrammar
from mathesis.deduction.natural_deduction import NDTree, rules

grammar = BasicGrammar()

premises = grammar.parse(["A∨B", "B→C"])
conclusion = grammar.parse("A∨C")
deriv = NDTree(premises, conclusion)
print(deriv.tree(number=False))

deriv.apply(deriv[1], rules.Disjunction.Elim())
deriv.apply(deriv[8], rules.Disjunction.Intro("left"))
deriv.apply(deriv[10], rules.Conditional.Elim())
deriv.apply(deriv[25], rules.Disjunction.Intro("right"))

print(deriv.tree(style="gentzen"))

print(deriv.latex())

A ∨ B, B → C ⇒ A ∨ C

A ∨ C [∨E]
├── A ∨ C [∨I]
│   └── A
├── A ∨ C [∨I]
│   └── C [→E]
│       ├── B → C
│       └── B
└── A ∨ B

\begin{prooftree}
\AxiomC{$[A]$}
\RightLabel{$\lor$I}
\UnaryInfC{$A \lor C$}
\AxiomC{$B \to C$}
\AxiomC{$[B]$}
\RightLabel{$\to$E}
\BinaryInfC{$C$}
\RightLabel{$\lor$I}
\UnaryInfC{$A \lor C$}
\AxiomC{$A \lor B$}
\RightLabel{$\lor$E}
\TrinaryInfC{$A \lor C$}
\end{prooftree}
\[ \begin{prooftree} \AxiomC{$[A]$} \RightLabel{$\lor$I} \UnaryInfC{$A \lor C$} \AxiomC{$B \to C$} \AxiomC{$[B]$} \RightLabel{$\to$E} \BinaryInfC{$C$} \RightLabel{$\lor$I} \UnaryInfC{$A \lor C$} \AxiomC{$A \lor B$} \RightLabel{$\lor$E} \TrinaryInfC{$A \lor C$} \end{prooftree} \]

Render as Fitch-style proof

WIP

Render as Suppes-Lemmon-style proof

WIP

Render as Sequent Calculus proof

WIP