Documentation

An axiom (Axiom (g |- a)) represents the inference of the judgement \(g \vdash a\), where \(a \in g\):

\[ \frac{}{ g \vdash a } \, (\text{Axiom}) \]

Falsity elimination (principle of explosion). (FalseElim (g |- a) p) represents the inference of the judgement \(g \vdash a\) given a proof \(p\) of \(g \vdash \bot\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash \bot } }{ g \vdash a } \, ({\bot}\text{E}) \]

Truth introduction. (TrueIntr (g |- Lit True)) represents the vacuous inference of the judgement \(g \vdash \top\):

\[ \frac{}{ g \vdash \top } \, (\top\text{I}) \]

Negation elimination. (NotElim (g |- Lit False) p q) represents the inference of the judgement \(g \vdash \bot\) given a proof \(p\) of \(g_1 \vdash \lnot a\) and a proof \(q\) of \(g_2 \vdash a\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash \lnot a } \qquad \displaystyle\frac{ q }{ g_2 \vdash a } }{ g \vdash \bot } \, ({\lnot}\text{E}) \]

Negation introduction. (NotIntr (g |- (Not a)) p) represents the inference of the judgement \(g \vdash \lnot a\) given a proof \(p\) of \(g, a \vdash \bot\):

\[ \frac{ \displaystyle\frac{ p }{ g, a \vdash \bot } }{ g \vdash \lnot a } \, ({\lnot}\text{I}) \]

Implication elimination (modus ponens). (ImpElim (g |- b) p q) represents the inference of the judgement \(g \vdash b\) given a proof \(p\) of \(g_1 \vdash a \rightarrow b\) and a proof \(q\) of \(g_2 \vdash a\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \rightarrow b } \qquad \displaystyle\frac{ q }{ g_2 \vdash a } }{ g \vdash b } \, ({\rightarrow}\text{E}) \]

Implication introduction. (ImpIntr (g |- (Imp a b) p) represents the inference of the judgement \(g \vdash a \rightarrow b\) given a proof \(p\) of \(g, a \vdash b\):

\[ \frac{ \displaystyle\frac{ p }{ g, a \vdash b } }{ g \vdash a \rightarrow b } \, ({\rightarrow}\text{I}) \]

Disjunction elimination. (OrElim (g |- c) p q r) represents the inference of the judgement \(g \vdash c\) given proofs \(p\) of \(g_1 \vdash a \lor b\), \(q\) of \(g_2, a \vdash c\), and \(r\) of \(g_3, b \vdash c\), where \(g = g_1 \cup g_2 \cup g_3\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \lor b } \qquad \displaystyle\frac{ q }{ g_2, a \vdash c } \qquad \displaystyle\frac{ r }{ g_3, b \vdash c } }{ g \vdash c } \, ({\lor}\text{E}) \]

Left disjunction introduction. (OrIntrL (g |- (Or a b)) p) represents the inference of the judgement \(g \vdash a \lor b\) given a proof \(p\) of \(g \vdash a\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a } }{ g \vdash a \lor b } \, ({\lor}\text{IL}) \]

Right disjunction introduction. (OrIntrR (g |- (Or a b)) p) represents the inference of the judgement \(g \vdash a \lor b\) given a proof \(p\) of \(g \vdash b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash b } }{ g \vdash a \lor b } \, ({\lor}\text{IR}) \]

Left conjunction elimination. (AndElimL (g |- a) p) represents the inference of the judgement \(g \vdash a\) given a proof \(p\) of \(g \vdash a \land b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \land b } }{ g \vdash a } \, ({\land}\text{EL}) \]

Right conjunction elimination. (AndElimR (g |- b) p) represents the inference of the judgement \(g \vdash b\) given a proof \(p\) of \(g \vdash a \land b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \land b } }{ g \vdash b } \, ({\land}\text{ER}) \]

Conjunction introduction. (AndIntr (g |- (And a b)) p) represents the inference of the judgement \(g \vdash a \land b\) given a proof \(p\) of \(g_1 \vdash a\) and a proof \(q\) of \(g_2 \vdash b\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a } \qquad \displaystyle\frac{ q }{ g_2 \vdash b } }{ g \vdash a \land b } \, ({\land}\text{I}) \]

Left equivalence elimination. (IffElimL (g |- (Imp a b)) p) represents the inference of the judgement \(g \vdash a \rightarrow b\) given a proof \(p\) of \(g \vdash a \leftrightarrow b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \leftrightarrow b } }{ g \vdash a \rightarrow b } \, ({\leftrightarrow}\text{EL}) \]

Right equivalence elimination. (IffElimR (g |- (Imp b a)) p) represents the inference of the judgement \(g \vdash b \rightarrow a\) given a proof \(p\) of \(g \vdash a \leftrightarrow b\):

\[ \frac{ \displaystyle\frac{ p }{ g \vdash a \leftrightarrow b } }{ g \vdash b \rightarrow a } \, ({\leftrightarrow}\text{ER}) \]

Equivalence introduction. (IffIntr (g |- (Iff a b)) p) represents the inference of the judgement \(g \vdash a \leftrightarrow b\) given a proof \(p\) of \(g_1 \vdash a \rightarrow b\) and a proof \(q\) of \(g_2 \vdash b \rightarrow a\), where \(g = g_1 \cup g_2\):

\[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \rightarrow b } \qquad \displaystyle\frac{ q }{ g_2 \vdash b \rightarrow a } }{ g \vdash a \leftrightarrow b } \, ({\leftrightarrow}\text{I}) \]