= Case-elimination Hilbert calculus
One presentation of <classical propositional logic> uses the schemes $A\to(B\to A)$, $(A\to(B\to C))\to((A\to(\neg B\to C))\to(A\to C))$, and $(A\to B)\to(A\to(\neg B\to C))$, together with <modus ponens rule> and the case rule from $A\to B$ and $\neg A\to B$ to $B$. Its <deduction theorem for propositional logic> follows by induction on <logical derivations>: <conditional modus ponens> handles a <modus ponens rule> line, and the second scheme handles a case-rule line.
Back to article page
