1 Connectives

1.1 Conjunction

Conjunction introduction

\[\begin{prooftree} \AxiomC{$A$} \AxiomC{$B$} \InferRule{\ConIntro} \BinaryInfC{$A \lcon B$} \end{prooftree}\]

Conjunction elimination

\[\begin{prooftree} \AxiomC{$A \lcon B$} \InferRule{\ConElimL} \UnaryInfC{$A$} \end{prooftree} \quad \begin{prooftree} \AxiomC{$A \lcon B$} \InferRule{\ConElimR} \UnaryInfC{$B$} \end{prooftree}\]

Commutativity of conjunction

\[A \lcon B \lproves B \lcon A\]

\[\begin{prooftree} \LabeledAxiomC{1}{$A \lcon B$} \InferRule{\ConElimR} \UnaryInfC{$B$} % \LabeledAxiomC{1}{$A \lcon B$} \InferRule{\ConElimL} \UnaryInfC{$A$} % \CancelNum{1} \InferRule{\ConIntro} \BinaryInfC{$B \lcon A$} \end{prooftree}\]

Associativity of conjunction

\[(A \lcon B) \lcon C \lproves A \lcon (B \lcon C)\]

\[\begin{prooftree} \AxiomC{$(A \lcon B) \lcon C$} \InferRule{\ConElimL} \UnaryInfC{$A \lcon B$} \InferRule{\ConElimL} \UnaryInfC{$A$} % \AxiomC{$(A \lcon B) \lcon C$} \InferRule{\ConElimL} \UnaryInfC{$A \lcon B$} \InferRule{\ConElimR} \UnaryInfC{$B$} % \AxiomC{$(A \lcon B) \lcon C$} \InferRule{\ConElimR} \UnaryInfC{$C$} % \InferRule{\ConIntro} \BinaryInfC{$B \lcon C$} % \InferRule{\ConIntro} \BinaryInfC{$A \lcon (B \lcon C)$} \end{prooftree}\]

1.2 Implication

Implication introduction

\[\begin{prooftree} \LabeledAxiomC{}{$A$} \AbbrDots \UnaryInfC{$B$} \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$} \AxiomC{$A \limp B$} \InferRule{\ImpElim} \BinaryInfC{$B$} \end{prooftree}\]

Hypothetical syllogism, transitivity of implication

\[A \limp B, B \limp C \lproves A \limp C\]

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

Currying

\[A \lcon B \limp C \lproves A \limp (B \limp C)\]

\[\begin{prooftree} \LabeledAxiomC{2}{$A$} \LabeledAxiomC{1}{$B$} \InferRule{\ConIntro} \BinaryInfC{$A \lcon B$} % \AxiomC{$A \lcon 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)$} \end{prooftree}\]

Uncurrying

\[A \limp (B \limp C) \lproves A \lcon B \limp C\]

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

1.3 Negation

Negation introduction

\[\begin{prooftree} \LabeledAxiomC{}{$A$} \AbbrDots \UnaryInfC{$\lfal$} \InferRule{\NegIntro} \UnaryInfC{$\lnot A$} \end{prooftree}\]

Negation elimination

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

Double negation introduction

\[A \lproves \lnot\lnot A\]

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

Law of noncontradiction (LNC)

\[\lproves \lnot (A \lcon \lnot A)\]

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

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

\[\lnot(A \lcon B), A \lproves \lnot B\]

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

Denying the consequent, modus tollendo tollens (MTT): mode that by denying denies

\[A \limp B, \lnot B \lproves \lnot A\]

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

1.4 Disjunction

Disjunction introduction

\[\begin{prooftree} \AxiomC{$A$} \InferRule{\DisIntroL} \UnaryInfC{$A \ldis B$} \end{prooftree} \quad \begin{prooftree} \AxiomC{$B$} \InferRule{\DisIntroR} \UnaryInfC{$A \ldis B$} \end{prooftree}\]

\[\lnot (A \ldis B) \lproves \lnot A \lcon \lnot B\]

\[\begin{prooftree} \LabeledAxiomC{1}{$A$} \InferRule{\DisIntroL} \UnaryInfC{$A \ldis B$} \LabeledAxiomC{}{$\lnot(A \ldis B)$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{1} \InferRule{\NegIntro} \UnaryInfC{$\lnot A$} % \LabeledAxiomC{2}{$B$} \InferRule{\DisIntroR} \UnaryInfC{$A \ldis B$} \LabeledAxiomC{}{$\lnot(A \ldis B)$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \CancelNum{2} \InferRule{\NegIntro} \UnaryInfC{$\lnot B$} % \InferRule{\ConIntro} \BinaryInfC{$\lnot A \lcon \lnot B$} \end{prooftree}\]

Disjunction elimination

\[\begin{prooftree} \AxiomC{$A \ldis B$} \LabeledAxiomC{}{$A$}\AbbrDots\UnaryInfC{$C$} \LabeledAxiomC{}{$B$}\AbbrDots\UnaryInfC{$C$} \InferRule{\DisElim} \TrinaryInfC{$C$} \end{prooftree}\]

\[A \ldis B \lproves \lnot(\lnot A \lcon \lnot B)\]

\[\begin{prooftree} \AxiomC{$A \ldis B$} % \LabeledAxiomC{3}{$A$} \LabeledAxiomC{1}{$\lnot A \lcon \lnot B$} \InferRule{\ConElimL} \UnaryInfC{$\lnot A$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} \CancelNum{1} \InferRule{\NegIntro} \UnaryInfC{$\lnot(\lnot A \lcon \lnot B)$} % \LabeledAxiomC{3}{$B$} \LabeledAxiomC{2}{$\lnot A \lcon \lnot B$} \InferRule{\ConElimR} \UnaryInfC{$\lnot B$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} \CancelNum{2} \InferRule{\NegIntro} \UnaryInfC{$\lnot(\lnot A \lcon \lnot B)$} % \CancelNum{3} \InferRule{\DisElim} \TrinaryInfC{$\lnot(\lnot A \lcon \lnot B)$} \end{prooftree}\]

Distribution of conjunction over disjunction

\[A \lcon (B \ldis C) \lproves (A \lcon B) \ldis (A \lcon C)\]

\[\begin{prooftree} \AxiomC{$A \lcon (B \ldis C)$} \InferRule{\ConElimR} \UnaryInfC{$B \ldis C$} % \AxiomC{$A \lcon (B \ldis C)$} \InferRule{\ConElimL} \UnaryInfC{$A$} % \LabeledAxiomC{1}{$B$} \InferRule{\ConIntro} \BinaryInfC{$A \lcon B$} % \InferRule{\DisIntroL} \UnaryInfC{$(A \lcon B) \ldis (A \lcon C)$} % \AxiomC{$A \lcon (B \ldis C)$} \InferRule{\ConElimL} \UnaryInfC{$A$} % \LabeledAxiomC{1}{$C$} \InferRule{\ConIntro} \BinaryInfC{$A \lcon C$} % \InferRule{\DisIntroR} \UnaryInfC{$(A \lcon B) \ldis (A \lcon C)$} % \CancelNum{1} \InferRule{\DisElim} \TrinaryInfC{$(A \lcon B) \ldis (A \lcon C)$} \end{prooftree}\]

1.5 Contradiction

Principle of explosion

ex falso [sequitur] quodlibet (EFQ)

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

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

\[A \ldis B, \lnot A \lproves B\]

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

Proof by contradiction

reductio ad absurdum (RAA)

\[\begin{prooftree} \LabeledAxiomC{}{$\lnot A$} \AbbrDots \UnaryInfC{$\lfal$} \InferRule{\RAA} \UnaryInfC{$A$} \end{prooftree}\]

Double negation elimination

\[\lnot\lnot A \lproves A\]

\[\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 (LEM)

\[\lproves A \ldis \lnot A\]

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

Peirce’s Law

\[\lproves ((A \limp B) \limp A) \limp A\]

\[\begin{prooftree} \InferRule{\LEM} \LabeledAxiomC{}{$A \ldis \lnot A$} % \LabeledAxiomC{2}{$A$} % \LabeledAxiomC{1}{$A$} \LabeledAxiomC{2}{$\lnot A$} \InferRule{\NegElim} \BinaryInfC{$\lfal$} % \InferRule{\lfal} \UnaryInfC{$B$} % \CancelNum{1} \InferRule{\ImpElim} \UnaryInfC{$A \limp B$} % \LabeledAxiomC{3}{$(A \limp B) \limp A$} \InferRule{\ImpElim} \BinaryInfC{$A$} % \CancelNum{2} \InferRule{\DisElim} \TrinaryInfC{$A$} % \CancelNum{3} \InferRule{\ImpIntro} \UnaryInfC{$((A \limp B) \limp A) \limp A$} \end{prooftree}\]