Natural Deduction

Implication

Implication introduction:

\begin{prooftree} \LabeledAxiomC{1}{$A$} \AbbrDots \UnaryInfC{$B$} \CancelNum{1} \InferRule{\ImpIntro} \UnaryInfC{$A \limp B$} \end{prooftree}

Implication elimination:

affirming the antecedent

modus ponendo ponens (MPP): mode that by affirming affirms

\begin{prooftree} \AxiomC{$A \limp B$} \AxiomC{$A$} \InferRule{\ImpElim} \BinaryInfC{$B$} \end{prooftree}

Conjunction

Conjunction introduction:

\begin{prooftree} \AxiomC{$A$} \AxiomC{$B$} \InferRule{\ConIntro} \BinaryInfC{$A \land B$} \end{prooftree}

Conjunction elimination:

\begin{prooftree} \AxiomC{$A \land B$} \InferRule{\ConElimL} \UnaryInfC{$A$} \end{prooftree}

\begin{prooftree} \AxiomC{$A \land B$} \InferRule{\ConElimR} \UnaryInfC{$B$} \end{prooftree}

Negation

$\lnot A$ is an abbreviation for $A \limp \lfal$.

Negation introduction:

a special case of implication introduction

\begin{prooftree} \LabeledAxiomC{1}{$A$} \AbbrDots \UnaryInfC{$\lfal$} \CancelNum{1} \InferRule{\NegIntro} \UnaryInfC{$\lnot A$} \end{prooftree}

Negation elimination:

a special case of implication elimination

\begin{prooftree} \AxiomC{$A$} \AxiomC{$\lnot A$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} \end{prooftree}

Contradiction

Principle of explosion:

ex falso [sequitur] quodlibet: from falsehood, anything [follows]

\begin{prooftree} \AxiomC{$\lfal$} \InferRule{\lfal} \UnaryInfC{$A$} \end{prooftree}

Reductio ad absurdum:

proof by contradiction

\begin{prooftree} \LabeledAxiomC{1}{$\lnot A$} \AbbrDots \UnaryInfC{$\lfal$} \CancelNum{1} \InferRule{\RAA} \UnaryInfC{$A$} \end{prooftree}

Disjunction

$A \lor B$ is an abbreviation for $\lnot(\lnot A \land \lnot B)$.

Disjunction introduction:

\begin{prooftree} \AxiomC{$A$} \InferRule{\DisIntroL} \UnaryInfC{$A \lor B$} \end{prooftree}

\begin{prooftree} \AxiomC{$B$} \InferRule{\DisIntroR} \UnaryInfC{$A \lor B$} \end{prooftree}

Disjunction elimination:

proof by cases, proof by exhaustion

\begin{prooftree} \AxiomC{$A \lor B$} \LabeledAxiomC{1}{$A$}\AbbrDots\UnaryInfC{$C$} \LabeledAxiomC{1}{$B$}\AbbrDots\UnaryInfC{$C$} \CancelNum{1} \InferRule{\DisElim} \TrinaryInfC{$C$} \end{prooftree}

Equivalence

$A \liff B$ is an abbreviation for $(A \limp B) \land (B \limp A)$.

Equivalence introduction:

\begin{prooftree} \LabeledAxiomC{1}{$A$}\AbbrDots\UnaryInfC{$B$} \LabeledAxiomC{1}{$B$}\AbbrDots\UnaryInfC{$A$} \CancelNum{1} \InferRule{\EqIntro} \BinaryInfC{$A \liff B$} \end{prooftree}

Equivalence elimination:

\begin{prooftree} \AxiomC{$A \liff B$} \AxiomC{$A$} \InferRule{\EqElimL} \BinaryInfC{$B$} \end{prooftree}

\begin{prooftree} \AxiomC{$A \liff B$} \AxiomC{$B$} \InferRule{\EqElimR} \BinaryInfC{$A$} \end{prooftree}

Theorems

Hypothetical syllogism:

chain argument, chain rule, transitivity of implication

\begin{prooftree} \AxiomC{$A \limp B$} \AxiomC{$B \limp C$} \InferRule{\HS} \BinaryInfC{$A \limp C$} \end{prooftree}

Proof:

\begin{prooftree} \AxiomC{$A \limp B$} \LabeledAxiomC{1}{$A$} \InferRule{\ImpElim} \BinaryInfC{$B$} % \AxiomC{$B \limp C$} \InferRule{\ImpElim} \BinaryInfC{$C$} % \CancelNum{1} \InferRule{\ImpIntro} \UnaryInfC{$A \limp C$} \end{prooftree}

Currying:

$$ ((A \land B) \limp C) \limp (A \limp (B \limp C)) $$

Proof:

\begin{prooftree} \LabeledAxiomC{2}{$A$} \LabeledAxiomC{1}{$B$} \InferRule{\ConIntro} \BinaryInfC{$A \land B$} % \LabeledAxiomC{3}{$(A \land B) \limp C$} \InferRule{\ImpElim} \BinaryInfC{$C$} % \CancelNum{1} \InferRule{\ImpIntro} \UnaryInfC{$B \limp C$} % \CancelNum{2} \InferRule{\ImpIntro} \UnaryInfC{$A \limp (B \limp C)$} % \CancelNum{3} \InferRule{\ImpIntro} \UnaryInfC{$((A \land B) \limp C) \limp (A \limp (B \limp C))$} \end{prooftree}

Uncurrying:

$$ (A \limp (B \limp C)) \limp ((A \land B) \limp C) $$

Proof:

\begin{prooftree} \LabeledAxiomC{1}{$A \land B$} \InferRule{\ConElimL} \UnaryInfC{$A$} % \LabeledAxiomC{2}{$A \limp (B \limp C)$} \InferRule{\ImpElim} \BinaryInfC{$B \limp C$} % \LabeledAxiomC{1}{$A \land B$} \InferRule{\ConElimR} \UnaryInfC{$B$} % \InferRule{\ImpElim} \BinaryInfC{$C$} % \CancelNum{1} \InferRule{\ImpIntro} \UnaryInfC{$A \land B \limp C$} % \CancelNum{2} \InferRule{\ImpIntro} \UnaryInfC{$(A \limp (B \limp C)) \limp (A \land B \limp C)$} \end{prooftree}

Law of noncontradiction:

\begin{prooftree} \AxiomC{} \InferRule{\LNC} \UnaryInfC{$\lnot(A \land \lnot A)$} \end{prooftree}

Proof:

\begin{prooftree} \LabeledAxiomC{1}{$A \land \lnot A$} \InferRule{\ConElimL} \UnaryInfC{$A$} % \LabeledAxiomC{1}{$A \land \lnot A$} \InferRule{\ConElimR} \UnaryInfC{$\lnot A$} % \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{1} \InferRule{\NegIntro} \UnaryInfC{$\lnot(A \land \lnot A)$} \end{prooftree}

Denying the consequent:

modus tollendo tollens (MTT): mode that by denying denies

\begin{prooftree} \AxiomC{$A \limp B$} \AxiomC{$\lnot B$} \InferRule{\MTT} \BinaryInfC{$\lnot A$} \end{prooftree}

Proof:

\begin{prooftree} \AxiomC{$A \limp B$} \LabeledAxiomC{1}{$A$} \InferRule{\ImpElim} \BinaryInfC{$B$} % \AxiomC{$\lnot B$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{1} \InferRule{\NegIntro} \UnaryInfC{$\lnot A$} \end{prooftree}

Conjunctive syllogism:

modus ponendo tollens (MPT): mode that by affirming denies

\begin{prooftree} \AxiomC{$\lnot(A \land B)$} \AxiomC{$A$} \InferRule{\MPT} \BinaryInfC{$\lnot B$} \end{prooftree}

Proof:

\begin{prooftree} \AxiomC{$\lnot(A \land B)$} \AxiomC{$A$} \LabeledAxiomC{1}{$B$} \InferRule{\ConIntro} \BinaryInfC{$A \land B$} % \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \InferRule{\NegIntro} \UnaryInfC{$\lnot B$} \end{prooftree}

Double negation introduction:

\begin{prooftree} \AxiomC{$A$} \InferRule{\DNegIntro} \UnaryInfC{$\lnot\lnot A$} \end{prooftree}

Proof:

\begin{prooftree} \AxiomC{$A$} \LabeledAxiomC{1}{$\lnot A$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{1} \InferRule{\NegIntro} \UnaryInfC{$\lnot\lnot A$} \end{prooftree}

Double negation elimination:

\begin{prooftree} \AxiomC{$\lnot\lnot A$} \InferRule{\DNegElim} \UnaryInfC{$A$} \end{prooftree}

Proof:

\begin{prooftree} \AxiomC{$\lnot\lnot A$} \LabeledAxiomC{1}{$\lnot A$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{1} \InferRule{\RAA} \UnaryInfC{$A$} \end{prooftree}

Law of excluded middle:

\begin{prooftree} \AxiomC{} \InferRule{\LEM} \UnaryInfC{$A \lor \lnot A$} \end{prooftree}

Proof:

\begin{prooftree} \LabeledAxiomC{1}{$A$} \InferRule{\DisIntroL} \UnaryInfC{$A \lor \lnot A$} % \LabeledAxiomC{2}{$\lnot(A \lor \lnot A)$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{1} \InferRule{\NegIntro} \UnaryInfC{$\lnot A$} % \InferRule{\DisIntroR} \UnaryInfC{$A \lor \lnot A$} % \LabeledAxiomC{2}{$\lnot(A \lor \lnot A)$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{2} \InferRule{\RAA} \UnaryInfC{$A \lor \lnot A$} \end{prooftree}

Disjunctive syllogism:

modus tollendo ponens (MTP): mode that by denying affirms

\begin{prooftree} \AxiomC{$A \lor B$} \AxiomC{$\lnot A$} \InferRule{\MTP} \BinaryInfC{$B$} \end{prooftree}

Proof:

\begin{prooftree} \AxiomC{$A \lor B$} \AxiomC{$\lnot A$} \LabeledAxiomC{1}{$A$} \InferRule{\NegIntro} \BinaryInfC{$\lfal$} % \InferRule{\lfal} \UnaryInfC{$B$} % \LabeledAxiomC{1}{$B$} \InferRule{\DisElim} \TrinaryInfC{$B$} \end{prooftree}