Propositional Logic

Formula (Type)

Of the form $X|A\to B$.

Axioms

$$\text{K}\frac{}{A\to B\to A}$$ $$\text{S}\frac{}{(A\to B\to C)\to (A\to B)\to A\to C}$$

Application (Modus Ponens)

$$\text{@}\frac{A\to BA}{B}$$

Deduction Theorem

$$\Gamma ,A⊢B⟹\Gamma ⊢A\to B$$

Examples

Identity

$⊢A\to A$

Pierce’s Formula

$⊬((A\to B)\to A)\to A$ This is classically valid but not intuinistically provable.