Axioms
- $\vdash A \rightarrow A$ Identity
- $\vdash (A \wedge B) \rightarrow A$ Simplification
- $\vdash (A \wedge B) \rightarrow B$ Simplification
- $\vdash A \rightarrow (A \lor B)$ Addition
- $\vdash B \rightarrow (A \lor B)$ Addition
- $\vdash (A \wedge (B \lor C)) \rightarrow ((A \wedge B) \lor C)$ Distribution
- $\vdash ((A \rightarrow B) \land (A \rightarrow C)) \rightarrow (A \rightarrow (B \land C))$ Strong Lattice $\land$
- $\vdash ((A \rightarrow C) \lor (B \rightarrow C)) \rightarrow ((A \lor B) \rightarrow C)$ Strong Lattice $\lor$
- $\vdash \neg \neg A \rightarrow A$ Double Negation Elimination
- $\vdash (A \rightarrow \neg B) \rightarrow (B \rightarrow \neg A)$ Contraposition
- $\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ Suffixing
- $\vdash (A \rightarrow B) \rightarrow ((C \rightarrow A) \rightarrow (C \rightarrow B))$ Prefixing
- $\vdash ((A \rightarrow (A \rightarrow B)) \rightarrow (A \rightarrow B)$ Contraction
Rules
R1.
$\vdash A$
$\vdash A \rightarrow B$
$\vdash B$ Modus Ponens
R2.
$\vdash A$
$\vdash B$
$\vdash A \land B$ Adjunction