Proof in Sequent Calculus

Sequent calculus (plural: calculi) is a formal proof system based on sequents, which normally are expressions of the form \(\Gamma \vdash \Delta\), where \(\Gamma\) and \(\Delta\) are lists or sets of formulas.

Sequent trees and applications of rules

mathesis.deduction.sequent_calculus.SequentTree is a class for sequent trees (proof trees, proof diagrams). It is initialized with an inference, given as a list of premises and of conclusions. Rules are applied to a sequent in a sequent tree with st.apply(node, rule) where st is a sequent tree.

from mathesis.deduction.sequent_calculus import SequentTree, rules
from mathesis.grammars import BasicGrammar

grammar = BasicGrammar()
premises = grammar.parse(["¬A", "A∨B"])
conclusions = grammar.parse(["B"])

st = SequentTree(premises, conclusions)

print(st.tree())
st.apply(st[1], rules.Negation.Left())
print(st.tree())
st.apply(st[5], rules.Disjunction.Left())
print(st.tree())
st.apply(st[9], rules.Weakening.Right())
print(st.tree())
st.apply(st[12], rules.Weakening.Right())
print(st.tree())

¬A 1, A∨B 2 ⇒ B 3

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6 [∨L]
    ├── A 7 ⇒ A 8, B 9
    └── B 10 ⇒ A 11, B 12

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6 [∨L]
    ├── A 7 ⇒ A 8, B 9 [wR]
    │   └── A 13 ⇒ A 14
    └── B 10 ⇒ A 11, B 12

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6 [∨L]
    ├── A 7 ⇒ A 8, B 9 [wR]
    │   └── A 13 ⇒ A 14
    └── B 10 ⇒ A 11, B 12 [wR]
        └── B 15 ⇒ A 16

Render the proof in LaTeX

A sequent tree object can be rendered in LaTeX with st.latex(). The LaTeX output uses a prooftree environment of bussproofs package. MathJax supports bussproofs package, so you can render the LaTeX output on a Web page.

from mathesis.deduction.sequent_calculus import SequentTree, rules
from mathesis.grammars import BasicGrammar

grammar = BasicGrammar()
premises = grammar.parse(["¬A", "A∨B"])
conclusions = grammar.parse(["B"])

st = SequentTree(premises, conclusions)

print(st.tree())
print(st.latex(number=False), "\n")

st.apply(st[1], rules.Negation.Left())
# print(st.tree())
st.apply(st[5], rules.Disjunction.Left())
# print(st.tree())
st.apply(st[9], rules.Weakening.Right())
# print(st.tree())
st.apply(st[12], rules.Weakening.Right())
print(st.tree())
print(st.latex(number=False))

¬A 1, A∨B 2 ⇒ B 3

\begin{prooftree}
\AxiomC{$\neg A, A \lor B \Rightarrow B$}
\end{prooftree} 

¬A 1, A∨B 2 ⇒ B 3 [¬L]
└── A∨B 5 ⇒ A 4, B 6 [∨L]
    ├── A 7 ⇒ A 8, B 9 [wR]
    │   └── A 13 ⇒ A 14
    └── B 10 ⇒ A 11, B 12 [wR]
        └── B 15 ⇒ A 16

\begin{prooftree}
\AxiomC{$A \Rightarrow A$}
\RightLabel{$wR}
\UnaryInfC{$A \Rightarrow A, B$}
\AxiomC{$B \Rightarrow A$}
\RightLabel{$wR}
\UnaryInfC{$B \Rightarrow A, B$}
\RightLabel{$\lor$L}
\BinaryInfC{$A \lor B \Rightarrow A, B$}
\RightLabel{$\neg$L}
\UnaryInfC{$\neg A, A \lor B \Rightarrow B$}
\end{prooftree}

\[ \begin{prooftree} \AxiomC{$\neg A, A \lor B \Rightarrow B$} \end{prooftree} \]

\[ \begin{prooftree} \AxiomC{$A \Rightarrow A$} \RightLabel{wR} \UnaryInfC{$A \Rightarrow A, B$} \AxiomC{$B \Rightarrow A$} \RightLabel{wR} \UnaryInfC{$B \Rightarrow A, B$} \RightLabel{$\lor$L} \BinaryInfC{$A \lor B \Rightarrow A, B$} \RightLabel{$\neg$L} \UnaryInfC{$\neg A, A \lor B \Rightarrow B$} \end{prooftree} \]