# 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}$