\[ \require{mathtools} \let\DeclarePairedDelimiter\DeclarePairedDelimiters % MathJax typo %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % symbol %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sets \newcommand{\N}{\mathbb{N}} % natural numbers \newcommand{\Z}{\mathbb{Z}} % integers \newcommand{\Q}{\mathbb{Q}} % rational numbers \newcommand{\R}{\mathbb{R}} % real numbers \newcommand{\C}{\mathbb{C}} % complex numbers % category \newcommand{\catf}[1]{{\mathbf{#1}}} \newcommand{\cA}{\catf{A}} \newcommand{\cB}{\catf{B}} \newcommand{\cC}{\catf{C}} \newcommand{\cD}{\catf{D}} \newcommand{\cE}{\catf{E}} \newcommand{\cF}{\catf{F}} \newcommand{\cG}{\catf{G}} \newcommand{\cH}{\catf{H}} \newcommand{\cI}{\catf{I}} \newcommand{\cJ}{\catf{J}} \newcommand{\cK}{\catf{K}} \newcommand{\cL}{\catf{L}} \newcommand{\cM}{\catf{M}} \newcommand{\cN}{\catf{N}} \newcommand{\cO}{\catf{O}} \newcommand{\cP}{\catf{P}} \newcommand{\cQ}{\catf{Q}} \newcommand{\cR}{\catf{R}} \newcommand{\cS}{\catf{S}} \newcommand{\cT}{\catf{T}} \newcommand{\cU}{\catf{U}} \newcommand{\cV}{\catf{V}} \newcommand{\cW}{\catf{W}} \newcommand{\cX}{\catf{X}} \newcommand{\cY}{\catf{Y}} \newcommand{\cZ}{\catf{Z}} \newcommand{\cZero}{\catf{0}} \newcommand{\cOne}{\catf{1}} \newcommand{\cTwo}{\catf{2}} \newcommand{\cArr}{\catf{Arr}} % arrow \newcommand{\cPSh}{\catf{PSh}} % presheaf \newcommand{\cCone}{\catf{Cone}} % cone \newcommand{\cCocone}{\catf{Cocone}} % cocone \newcommand{\cFin}{\catf{Fin}} % finite prefix \newcommand{\cSet}{\catf{Set}} % functions \newcommand{\cRel}{\catf{Rel}} % relations \newcommand{\cPos}{\catf{Pos}} % posets \newcommand{\cMon}{\catf{Mon}} % monoids \newcommand{\cCMon}{\catf{CMon}} % commutative monoids \newcommand{\cGrp}{\catf{Grp}} % groups \newcommand{\cAb}{\catf{Ab}} % abelian groups \newcommand{\cCat}{\catf{Cat}} % categories \newcommand{\cGrpd}{\catf{Grpd}} % groupoids \newcommand{\cVect}{\catf{Vect}} % vector spaces \newcommand{\cMat}{\catf{Mat}} % matrices \newcommand{\cTop}{\catf{Top}} % topological spaces and continuous maps \newcommand{\cMet}{\catf{Met}} % metric spaces and metric maps \newcommand{\cMeas}{\catf{Meas}} % measurable spaces and measurable functions \newcommand{\cStoch}{\catf{Stoch}} % measurable spaces and stochastic maps \newcommand{\cProb}{\catf{Prob}} % probability measures and measure-preserving functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % supscript %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\op}{^\mathrm{op}} \newcommand{\inv}{^{-1}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % function %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclareMathOperator{\lcm}{lcm} \DeclareMathOperator{\logsumexp}{log-sum-exp} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % arrow %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % morphism \newcommand{\xto}{\xrightarrow} % -> \newcommand{\xot}{\xleftarrow} % <- \newcommand{\toot}{\rightleftarrows} % <=> \newcommand{\xtoot}[2]{\xrightleftharpoons[#2]{#1}} \newcommand{\iso}{\cong} % ~= \newcommand{\klto}{\rightsquigarrow} % ~> \newcommand{\mono}{\rightarrowtail} % >-> \newcommand{\epi}{\twoheadrightarrow} % ->> \newcommand{\ihom}{\multimap} % -o % category \newcommand{\incl}{\hookrightarrow} \newcommand{\adjto}[2]{\overset{{}\xto[]{#1}{}}{\underset{{}\xot[#2]{}{}}{\bot}}} % functor \newcommand{\nat}{\Rightarrow} % => \newcommand{\xnat}{\xRightarrow} % => \newcommand{\comma}{\downarrow} \newcommand{\adj}{\dashv} % -| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % delimiter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclarePairedDelimiter{\parens}{(}{)} % parentheses ( ) \DeclarePairedDelimiter{\bracks}{[}{]} % brackets [ ] \DeclarePairedDelimiter{\braces}{\{}{\}} % braces { } \DeclarePairedDelimiter{\angles}{\langle}{\rangle} % angles \DeclarePairedDelimiter{\floor}{\lfloor}{\rfloor} \DeclarePairedDelimiter{\ceil}{\lceil}{\rceil} \newcommand{\set}{\braces} \newcommand{\singleton}{{\set{*}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % operator %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\compL}{\mathbin{\circ}} \newcommand{\compR}{\mathbin{;}} \newcommand{\Kl}{\mathrm{Kl}} \DeclareMathOperator{\Obj}{Obj} \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\Sub}{Sub} \DeclareMathOperator{\Eq}{Eq} \DeclareMathOperator{\Coeq}{Coeq} \DeclareMathOperator{\Pull}{Pull} \DeclareMathOperator{\Push}{Push} \DeclareMathOperator{\Lan}{Lan} \DeclareMathOperator{\Ran}{Ran} \DeclareMathOperator{\Lift}{Lift} \DeclareMathOperator{\Rift}{Rift} \DeclareMathOperator{\id}{id} \DeclareMathOperator{\act}{act} \DeclareMathOperator{\colim}{colim} % exponential \DeclareMathOperator{\partf}{partial} \DeclareMathOperator{\curry}{curry} % natural number \DeclareMathOperator{\zero}{zero} \DeclareMathOperator{\successor}{succ} % list \DeclareMathOperator{\nil}{nil} \DeclareMathOperator{\cons}{cons} \newcommand{\concat}{\mathbin{{+}\mspace{-8mu}{+}}} % fold \DeclareMathOperator{\fold}{fold} \DeclareMathOperator{\map}{map} \DeclareMathOperator{\filter}{filter} % bool \DeclareMathOperator{\cond}{cond} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % order %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\meet}{\wedge} \newcommand{\join}{\vee} \newcommand{\bigmeet}{\bigwedge} \newcommand{\bigjoin}{\bigvee} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % logic %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\lfal}{\bot} \newcommand{\ltru}{\top} \newcommand{\lcon}{\wedge} \newcommand{\lncon}{\uparrow} \newcommand{\ldis}{\vee} \newcommand{\lndis}{\downarrow} \newcommand{\limp}{\rightarrow} \newcommand{\lnimp}{\nrightarrow} \newcommand{\lcim}{\leftarrow} \newcommand{\lncim}{\nleftarrow} \newcommand{\leqv}{\leftrightarrow} \newcommand{\lneqv}{\nleftrightarrow} \newcommand{\lproves}{\vdash} % |- \newcommand{\lmodels}{\vDash} % |= \newcommand{\lnproves}{\nvdash} % |/- \newcommand{\lnmodels}{\nvDash} % |/= \]
\[ \require{bussproofs} \newcommand{\CancelNum}[1]{\LeftLabel{$\tiny#1$}} \newcommand{\InferRule}[1]{\RightLabel{$\;#1$}} \newcommand{\LabeledAxiomC}[2]{\AxiomC{}\CancelNum{#1}\UnaryInfC{#2}} \newcommand{\AbbrDots}{\noLine\UnaryInfC{$\vdots$}\noLine} \newcommand{\Intro}{{\mathrm{I}}} \newcommand{\Elim}{{\mathrm{E}}} \newcommand{\Left}{{\mathrm{L}}} \newcommand{\Right}{{\mathrm{R}}} % conjunction \newcommand{\ConIntro}{\lcon_\Intro} \newcommand{\ConElim}{\lcon_\Elim} \newcommand{\ConElimL}{\lcon_{\Elim_\Left}} \newcommand{\ConElimR}{\lcon_{\Elim_\Right}} % disjunction \newcommand{\DisIntro}{\ldis_\Intro} \newcommand{\DisIntroL}{\ldis_{\Intro_\Left}} \newcommand{\DisIntroR}{\ldis_{\Intro_\Right}} \newcommand{\DisElim}{\ldis_\Elim} % implication \newcommand{\ImpIntro}{\limp_\Intro} \newcommand{\ImpElim}{\limp_\Elim} % negation \newcommand{\NegIntro}{\lnot_\Intro} \newcommand{\NegElim}{\lnot_\Elim} % contradiction \newcommand{\RAA}{{\mathrm{RAA}}} \newcommand{\LEM}{{\mathrm{LEM}}} \newcommand{\LNC}{{\mathrm{LNC}}} \]
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}\]