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[7], 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 5, B→C 6 ⇒ A∨C 7
└── B 8, A∨B 9, B→C 10 ⇒ A∨C 11

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

A∨B 1, B→C 2 ⇒ A∨C 3 [∨E]
├── A 4, A∨B 5, B→C 6 ⇒ A∨C 7 [∨I]
│   └── A 13, A∨B 14, B→C 15 ⇒ A 12
└── B 8, 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 5, B→C 6 ⇒ A∨C 7 [∨I]
│   └── A 13, A∨B 14, B→C 15 ⇒ A 12
└── B 8, 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

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[7], 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
├── A∨C
│   └── A
├── A∨C
│   └── C
│       ├── B
│       └── B→C
└── A∨B

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

\[ \begin{prooftree} \AxiomC{$A$} \RightLabel{$\lor$I} \UnaryInfC{$A \lor C$} \AxiomC{$B$} \RightLabel{$\to$E} \AxiomC{$B \to C$} \BinaryInfC{$C$} \RightLabel{$\lor$I} \UnaryInfC{$A \lor C$} \RightLabel{$\lor$E} \AxiomC{$A \lor B$} \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