cheat4.tex

\documentclass[a4paper,10pt]{article}
\usepackage{mypreamble}

%% Page setup
\geometry{
    margin=2cm,
    includehead,
    includefoot,
    headsep=8pt,
    footskip=16pt,
}
\pagestyle{fancy}
\MakeSingleHeader% {<l>}{<r>}
    {\TextCheatsheetEng: Formal Logic}%
    {\TextDiscreteMathEng, \IconFall~Fall 2024}
\fancyfoot{}
\fancyfoot[L]{\tiny Build time: \DTMnow}
\fancyfoot[R]{\tiny Source code can be found at \url{https://github.com/Lipen/discrete-math-course}}
% \fancyfoot[C]{\thepage\ of \zpageref{LastPage}}

%% Add custom setup below

% \titlespacing{\type}{left}{above}{below}[right]
\titlespacing{\section}{0pt}{*1}{*0.5}
\titlespacing{\subsection}{0pt}{*1}{*0.5}

\setlength{\tabcolsep}{0pt}

\colorlet{ColorValid}{green!70!black}
\colorlet{ColorInvalid}{red!70!black}

%% checkmark and crossmark symbols
\usepackage{pifont}
\newcommand{\cmark}{\text{\ding{51}}}
\newcommand{\xmark}{\text{\ding{55}}}

\newcommand{\Valid}{\textcolor{ColorValid}{\cmark}}
\newcommand{\Invalid}{\textcolor{ColorInvalid}{\xmark}}
\newcommand{\ValidArgument}{%
    \mathclap{\overset{\smash{\textcolor{ColorValid}{\textit{valid}}}}{\therefore}}}
\newcommand{\InvalidArgument}{%
    \mathclap{\overset{\smash{\textcolor{ColorInvalid}{\textit{invalid}}}}{\therefore}}}

%% BNF grammar
\usepackage{syntax}

%% Formal proofs
\usepackage{fitch}
% https://www.mathstat.dal.ca/~selinger/fitch/fitchdoc.pdf
% \nddim{height}{topheight}{depth}{labelsep}{indent}{hsep}{justsep}{linethickness}
% Default: \nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}
\nddim%
    {3.6ex}% <height> [4.5ex]
    {3.0ex}% <topheight> [3.5ex]
    {1.0ex}% <depth> [1.5ex]
    {0.8em}% <labelsep> [1em]
    {0.5em}% <indent> [1.6em]
    {0.5em}% <hsep> [.5em]
    {2.0em}% <justsep> [2.5em]
    {0.8pt}% <linethickness> [.2mm]

%% Autoscale missing font sizes
\usepackage{anyfontsize}

%% Silence some warnings
\WarningFilter{latexfont}{Font shape `OMS/LinuxLibertineT-TLF/m/n' undefined}
\WarningFilter{latexfont}{Some font shapes were not available, defaults substituted.}

%% Inline list
\newlist{mylist}{enumerate*}{1}
\setlist[mylist]{label=(\arabic*)}


\begin{document}

\selectlanguage{english}

\setcounter{section}{3}% +1 = actual
\section{Formal Logic Cheatsheet}

\subsection{Propositional Logic%
\texorpdfstring{\normalsize\protect\Href{https://en.wikipedia.org/wiki/Propositional_logic}}{}}

\begin{terms}
    \item \textbf{Proposition}\Href{https://en.wikipedia.org/wiki/Proposition} is a statement which can be either true or false.
    \hfill\href{https://en.wikipedia.org/wiki/Truth-bearer}{Truth-bearer}

    \item \textbf{Alphabet}\Href{https://en.wikipedia.org/wiki/Alphabet_(formal_languages)} of propositional logic consists of
    \begin{mylist}
        \item atomic symbols and
        \item operator symbols.
    \end{mylist}
    % \hfill\href{https://en.wikipedia.org/wiki/Alphabet_(formal_languages)}{Alphabet}

    % \item \textbf{Braces:} ( and ).

    % \hfill\href{https://en.wikipedia.org/wiki/Formal_language}{Formal language}

    % https://en.wikipedia.org/wiki/Atomic_formula
    \item \textbf{Atomic formula}\Href{https://en.wikipedia.org/wiki/Atomic_formula} (\textbf{atom}) is an irreducible formula without logical connectives.
    \begin{terms}
        \item Propositional \textbf{variables}: $A, B, C, \dotsc, Z$. With indices, if needed: $A_1, A_2, \dotsc, Z_1, Z_2, \dotsc$.

        \item Logical \textbf{constants}: $\top$ for always true proposition (\textit{tautology}), $\bot$ for always false proposition (\textit{contradiction}).
    \end{terms}

    \item \textbf{Logical connectives}\Href{https://en.wikipedia.org/wiki/Logical_connective} (\textbf{operators}):
    % \hfill\href{https://en.wikipedia.org/wiki/Logical_connective}{Logical connective}

    \begingroup
    \newcommand{\myA}{\mathcal{P}}
    \newcommand{\myB}{\mathcal{Q}}

    \begin{tabular}{l @{\hspace{1em}} l @{\hspace{2pt}} c}
    % \toprule
        \thead{Type} &
        \thead{Natural meaning} &
        \thead{Symbolization} \\
    \midrule
        \Href{https://en.wikipedia.org/wiki/Negation}%
        Negation
        % \hfill\Href{https://en.wikipedia.org/wiki/Negation}
        & \makecell[lt]{
            It is not the case that $\myA$. \\[-\jot]
            It is false that $\myA$. \\[-\jot]
            It is not true that $\myA$.
        }
        & $\neg \myA$ \\
    \cmidrule(r){1-3}
        \Href{https://en.wikipedia.org/wiki/Logical_conjunction}%
        Conjunction
        % \hfill\Href{https://en.wikipedia.org/wiki/Logical_conjunction}
        & \makecell[lt]{
            Both $\myA$ and $\myB$. \\[-\jot]
            $\myA$ but $\myB$. \\[-\jot]
            $\myA$, although $\myB$.
        }
        & $\myA \land \myB$ \\
    \cmidrule(r){1-3}
        \Href{https://en.wikipedia.org/wiki/Logical_disjunction}%
        Disjunction
        % \hfill\Href{https://en.wikipedia.org/wiki/Logical_disjunction}
        & \makecell[lt]{
            Either $\myA$ or $\myB$ (or both). \\[-\jot]
            $\myA$ unless $\myB$.
        }
        & $\myA \lor \myB$ \\
    \cmidrule(r){1-3}
        \Href{https://en.wikipedia.org/wiki/Exclusive_or}%
        Exclusive or (Xor)
        % ~\hfill\Href{https://en.wikipedia.org/wiki/Exclusive_or}
        & \makecell[lt]{
            Either $\myA$ or $\myB$ (but not both). \\[-\jot]
            $\myA$ xor $\myB$.
        }
        & $\myA \xor \myB$ \\
    \cmidrule(r){1-3}
        \Href{https://en.wikipedia.org/wiki/Material_conditional}%
        \makecell[lt]{Implication \\[-\jot] (Conditional)}
        % \hfill\Href{https://en.wikipedia.org/wiki/Material_conditional}
        & \makecell[lt]{
            If $\myA$, then $\myB$. \\[-\jot]
            $\myA$ only if $\myB$. \\[-\jot]
            $\myB$ if $\myA$.
        }
        & $\myA \implies \myB$ \\
    \cmidrule(r){1-3}
        \Href{https://en.wikipedia.org/wiki/Logical_biconditional}%
        Biconditional
        % \hfill\Href{https://en.wikipedia.org/wiki/Logical_biconditional}
        & \makecell[lt]{
            $\myA$, if and only if $\myB$. \\[-\jot]
            $\myA$ iff $\myB$. \\[-\jot]
            $\myA$ just in case $\myB$.
        }
        & $\myA \iff \myB$ \\
    % \bottomrule
    \end{tabular}
    \vspace{1pt}
    \endgroup

    \item \textbf{Sentence} of propositional logic is defined inductively:
    \hfill\href{https://en.wikipedia.org/wiki/Well-formed_formula}{Well-formed formula (WFF)}

    \begin{enumerate}[left=6pt .. 18pt]
        \item Every propositional variable/constant is a sentence.

        \item If $\mathcal{A}$ is a sentence, then $\neg\mathcal{A}$ is a sentence.

        \item If $\mathcal{A}$ and $\mathcal{B}$ are sentences, then $(\mathcal{A} \land \mathcal{B})$, $(\mathcal{A} \lor \mathcal{B})$, $(\mathcal{A} \implies \mathcal{B})$, $(\mathcal{A} \iff \mathcal{B})$ are sentences.

        \item Nothing else is a sentence.
    \end{enumerate}

    \item Well-formed formulae grammar:
    \hfill\href{https://en.wikipedia.org/wiki/Backus-Naur_form}{Backus-Naur form (BNF)}

    \vspace{-2pt}
    \setlength{\grammarparsep}{0pt plus 4pt}
    \setlength{\grammarindent}{6em}
    \begin{grammar}
        <sentence> ::=
             <constant>
        \alt <variable>
        \alt $\neg$ <sentence>
        \alt `(' <sentence> <binop> <sentence> `)'

        <constant> ::=
            $\top$ | $\bot$

        <variable> ::=
            $A$ | \dots | $Z$ | $A_1$ | \dots | $Z_n$

        <binop> ::=
            $\land$ | $\lor$ | $\xor$ | $\implies$ | $\impliedby$ | $\iff$
    \end{grammar}

    \item \textbf{Literal}\Href{https://en.wikipedia.org/wiki/Literal_(mathematical_logic)} is a propositional variable or its negation: $\mathcal{L}_i = X_i$ (\textit{positive} literal), $\mathcal{L}_j = \neg X_j$ (\textit{negative} literal).

    \item \textbf{Argument}\Href{https://en.wikipedia.org/wiki/Argument} is a set of logical statements, called \emph{premises}, intended to support or infer a claim (\emph{conclusion}):
    \[
        \underbrace{
            \mathcal{A}_1, \mathcal{A}_2, \dotsc, \mathcal{A}_n
        }_{\textit{premises}}
        \quad
        \begin{tikzpicture}[remember picture,overlay,on grid,baseline={(therefore.base)},inner sep=0pt]
            \node (therefore) {$\therefore$};
            \node (label) [below left=11mm and 5mm of therefore] {\small\enquote{therefore}};
            \draw[->,>={Stealth[]},shorten >=2pt] (label.north) to[out=90,in=-100,looseness=1.3] (therefore.south);
        \end{tikzpicture}
        \vrule height 0pt depth 11mm width 0pt\relax
        ~~
        \underbrace{
            \mathcal{C}_{\vphantom{n}}
        }_{\mathclap{\textit{conclusion}}}
    \]

    \item An argument is \textbf{valid} if whenever all the premises are true, the conclusion is also true.
    \hfill\href{https://en.wikipedia.org/wiki/Validity_(logic)}{Validity}

    \item An argument is \textbf{invalid} if there is a case (\textit{a counterexample)} when all the premises are true, but the conclusion is false.
\end{terms}


\newpage
\subsection{Semantics of Propositional Logic}

\begin{terms}
    \item \textbf{Valuation}\Href{https://en.wikipedia.org/wiki/Valuation_(logic)} is any assignment of truth values to propositional variables.
    \hfill\href{https://en.wikipedia.org/wiki/Interpretation_(logic)}{Interpretation}

    \item $\mathcal{A}$ is a \textbf{tautology}\Href{https://en.wikipedia.org/wiki/Tautology_(logic)} (\textbf{valid}) iff it is true on \emph{every} valuation. Might be symbolized as \enquote{${} \entails \mathcal{A}$}.

    \item $\mathcal{A}$ is a \textbf{contradiction}\Href{https://en.wikipedia.org/wiki/Contradiction} iff it is false on \emph{every} valuation. Might be symbolized as \enquote{\,$\mathcal{A} \entails {}$\,}.

    \item $\mathcal{A}$ is a \textbf{contingency}\Href{https://en.wikipedia.org/wiki/Contingency_(philosophy)} iff it is true on some valuation and false on another. In other words, a \textbf{contingent} proposition is neither a tautology nor a contradiction.

    \item $\mathcal{A}$ is \textbf{satisfiable} iff it is true on \emph{some} valuation.
    \hfill\href{https://en.wikipedia.org/wiki/Satisfiability}{Satisfiability}

    \item $\mathcal{A}$ is \textbf{falsifiable} iff it is not valid, \ie it is false on \emph{some} valuation.
    \hfill\href{https://en.wikipedia.org/wiki/Falsifiability}{Falsifiability}

    \item $\mathcal{A}$ and $\mathcal{B}$ are \textbf{equivalent}\Href{https://en.wikipedia.org/wiki/Logical_equivalence} (symbolized as $\mathcal{A} \equiv \mathcal{B}$) iff, for every valuation, their truth values agree, \ie there is no valuation in which they have opposite truth values.
    \hfill\href{https://en.wikipedia.org/wiki/Formal_equivalence_checking}{Equivalence check}

    \item $\mathcal{A}_1, \mathcal{A}_2, \dotsc, \mathcal{A}_n$ are \textbf{consistent} (\textbf{jointly satisfiable}) iff there is \emph{some} valuation which makes them all true. Sentences are \textbf{inconsistent} (\textbf{jointly unsatisfiable}) iff there is \emph{no} valuation that makes them all true.
    ~\hfill\href{https://en.wikipedia.org/wiki/Consistency}{Consistency}

    \item The sentences $\mathcal{A}_1, \mathcal{A}_2, \dotsc, \mathcal{A}_n$ \textbf{entail} the sentence $\mathcal{C}$ (symbolized as $\mathcal{A}_1, \mathcal{A}_2, \dotsc, \mathcal{A}_n \entails \mathcal{C}$) if there is no valuation which makes all of $\mathcal{A}_1, \mathcal{A}_2, \dotsc, \mathcal{A}_n$ true and $\mathcal{C}$ false.
    \hfill\href{https://en.wikipedia.org/wiki/Logical_consequence#Semantic_consequence}{Semantic entailment}

    \item If $\mathcal{A}_1, \mathcal{A}_2, \dotsc, \mathcal{A}_n \entails \mathcal{C}$, then the argument $\mathcal{A}_1, \mathcal{A}_2, \dotsc, \mathcal{A}_n \therefore \mathcal{C}$ is \textbf{valid}.

    \vspace{2pt}
    \textit{Validity check examples}:

\vspace{6pt}
\(\begin{array}{
    @{~}
    c @{~~} c % Arguments: A,B
    % A \implies B, A \therefore B
    @{~~~} |
    @{~~~} c @{\,} B @{\,} c % A \implies B
    @{~~~} B % A
    @{~~~} c % therefore
    @{~~~} B % B
    % \neg A \implies \neg B \therefore B \implies A
    @{~~~} |
    @{~~~} c @{} c @{\,} B @{\,} c @{} c % \neg A \implies \neg B
    @{~~~} c % therefore
    @{~~~} c @{\,} B @{\,} c % B \implies A
    % A \implies B, B \therefore \neg (B \implies A)
    @{~~~} |
    @{~~~} c @{\,} B @{\,} c % A \implies B
    @{~~~} B % B
    @{~~~} c % therefore
    @{~~~} B @{\,} c @{\,} c @{\,} c % \neg (B \implies A)
    @{~}
}
    A&B
    & A&\implies&B & A &\ValidArgument& B
    & \neg&A&\implies&\neg&B &\ValidArgument& B&\implies&A
    & A&\implies&B & B &\InvalidArgument& \neg&(B&\implies&A)
    \BotStrut\\
    \hline\TopStrut
    % print('\n'.join(f'{a}&{b}  &  {a}&{not a or b}&{b} & {a} &\\--& {b}  &  {not a}&{a}&{a or not b}&{not b}&{b} &\\--& {b}&{not b or a}&{a}  &  {a}&{not a or b}&{b} & {b} &\\--& {not(not b or a)}&{b}&{not b or a}&{a} \\\\'.replace('True', '1').replace('False', '0') for a,b in [(False, False), (False, True), (True, False), (True, True)]))
    0&0
    &&1& & 0 &\cdot& 0
    &1&&1&1& &\Valid& &1&
    &&1& & 0 &\cdot& 0&&1& \\
    0&1
    &&1& & 0  &\cdot& 1
    &1&&0&0& &\cdot& &0&
    &&1& & 1 &\Valid& 1&&0& \\
    1&0
    &&0& & 1 &\cdot& 0
    &0&&1&1& &\Valid& &1&
    &&0& & 0 &\cdot& 0&&1& \\
    1&1
    &&1& & 1 &\Valid& 1
    &0&&1&0& &\Valid& &1&
    &&1& & 1 &\Invalid& 0&&1& \\
\end{array}\)

\vspace{10pt}
\(\begin{array}{
    @{~}
    c @{~~} c @{~~} c % Arguments: R,S,T
    % R \lor S, S \lor T, \neg R \therefore S \land T
    @{~~~} |
    @{~~~} c @{\,} B @{\,} c % R \lor S
    @{~~~} c @{\,} B @{\,} c % S \lor T
    @{~~~} B @{\,} c % \neg R
    @{~~~} c % therefore
    @{~~~} c @{\,} B @{\,} c % S \land T
    % (R \land S) \implies T \therefore R \implies (S \implies T)
    @{~~~} |
    @{~~~} c @{\,} c @{\,} c @{\,} B @{\,} c % (R \land S) \implies T
    @{~~~} c % therefore
    @{~~~} c @{\,} B @{\,} c @{\,} c @{\,} c % R \implies (S \implies T)
    @{~}
}
    R&S&T
    & R&\lor&S & S&\lor&T & \neg&R &\InvalidArgument& S&\land&T
    & (R&\land&S)&\implies&T &\ValidArgument& R&\implies&(S&\implies&T)
    \BotStrut\\
    \hline\TopStrut
    % print('\n'.join(f'{r}&{s}&{t}  &\n{r}&{r or s}&{s} & {s}&{s or t}&{t} & {not r}&{r} &\\--& {s}&{s and t}&{t}  &\n{r}&{r and s}&{s}&{not(r and s) or t}&{t} &\\--& {r}&{not r or (not s or t)}&{s}&{not s or t}&{t} \\\\'.replace('True','1').replace('False','0') for r in B for s in B for t in B))
    0&0&0
    &&0& & &0& & 1& &\cdot& &0&
    &&0&&1&0 &\Valid& 0&1&&1& \\
    0&0&1
    &&0& & &1& & 1& &\cdot& &0&
    &&0&&1&1 &\Valid& 0&1&&1& \\
    0&1&0
    &&1& & &1& & 1& &\Invalid& &0&
    &&0&&1&0 &\Valid& 0&1&&0& \\
    0&1&1
    &&1& & &1& & 1& &\Valid& &1&
    &&0&&1&1 &\Valid& 0&1&&1& \\
    1&0&0
    &&1& & &0& & 0& &\cdot& &0&
    &&0&&1&0 &\Valid& 1&1&&1& \\
    1&0&1
    &&1& & &1& & 0& &\cdot& &0&
    &&0&&1&1 &\Valid& 1&1&&1& \\
    1&1&0
    &&1& & &1& & 0& &\cdot& &0&
    &&1&&0&0 &\cdot& 1&0&&0& \\
    1&1&1
    &&1& & &1& & 0& &\cdot& &1&
    &&1&&1&1 &\Valid& 1&1&&1& \\
\end{array}\)

    \item \textbf{Soundness\Href{https://en.wikipedia.org/wiki/Soundness}:} $\Gamma \vdash \mathcal{A} \implies \Gamma \entails \mathcal{A}$
    \quad\enquote{Every provable statement is in fact true}

    \item \textbf{Completeness:}\Href{https://en.wikipedia.org/wiki/Completeness_(logic)} $\Gamma \entails \mathcal{A} \implies \Gamma \vdash \mathcal{A}$
    \quad\enquote{Every true statement has a proof}


    % \item \dots
\end{terms}


\newpage
\subsection{Natural Deduction Rules}

\colorlet{colorbasicrule}{green!45!black}
\colorlet{colorderivedrule}{orange!70!black}

\begingroup
\newcommand{\myA}{\mathcal{A}}
\newcommand{\myB}{\mathcal{B}}
\newcommand{\myC}{\mathcal{C}}
\newcommand{\midlineheight}{.7\baselineskip}
\newcommand{\extratopskip}{8pt}
\newcommand{\myheight}{%
    \dimexpr\textheight-16pt-\extratopskip\relax}

% \hypo{<line label>}{<formula>}: line with horizontal bar
% \have{<line label>}{<formula>}: line without horizontal bar
% \open: opens a subproof
% \close: closes a subproof
% \by{<rule}{<line labels}
% \hypo[<symbol>][<offset>]{<line label>}{<formula>}
% \have[<symbol>][<offset>]{<line label>}{<formula>}

\tcbset{
    formalbox/.style={% with arg #1 = <title>
        title={\strut #1},
        fonttitle=\bfseries,
        size=title,
        boxsep=2pt,
        top=0pt,
        bottom=1mm,
        leftupper=0pt,
        rightupper=0pt,
        %%% draft,
    },
    myoverlay/.style={% with arg #1 = <text>
        enhanced,
        overlay={
            \path[
                draw=blue,
                fill=blue!75!white,
                opacity=0.8,
            ] (frame.north east)
            ++(0,-0.8)
            ++(-0.1mm,-0.1mm)
            -- ++(-0.8,0.8)
            -- ++(-0.7,0)
            -- ++(1.5,-1.5)
            -- cycle;
            \path (frame.north east) ++(-0.57,-0.57)
            node[white,rotate=-45] {#1};
        },
    },
}

\newtcolorbox{formalboxbasic}[2][]{% [<style>]{<title>}
    formalbox=#2,
    % myoverlay={Basic},
    colback=green!5,
    colframe=colorbasicrule,
    #1
}
\newtcolorbox{formalboxderived}[2][]{% [<style>]{<title>}
    formalbox=#2,
    % myoverlay={Derived},
    colback=orange!5,
    colframe=colorderivedrule,
    #1
}

\makeatletter
\newcommand{\DrawLine}[1]{% {<color>}
    \vrule height \midlineheight depth \dimexpr \midlineheight-1ex\relax width 0pt\relax
    \begin{tikzpicture}
        \path[use as bounding box] (0,0) -- (\linewidth,0);
        \draw[color=#1,dashed,dash phase=5pt]
            (0-\kvtcb@leftupper-\kvtcb@boxsep,0)
            --(\linewidth+\kvtcb@rightupper+\kvtcb@boxsep,0);
    \end{tikzpicture}}
\makeatother

\vskip\extratopskip

\begin{adjustbox}{minipage=[t][\myheight]{.3\linewidth},valign=t}
    \begin{formalboxbasic}{Reiteration}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{A}{\myA}
            \have[\therefore]{rA}{\myA} \r{A}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxbasic}{Modus ponens}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{AimpliesB}{\myA \implies \myB}
            \have[j]{A}{\myA}
            \have[\therefore]{B}{\myB} \mp{AimpliesB,A}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxderived}{Modus tollens}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{AimpliesB}{\myA \implies \myB}
            \have[j]{negB}{\neg\myB}
            \have[\therefore]{negA}{\neg\myA} \mt{AimpliesB,negB}
        \end{nd}
        \end{flusheqs}
    \end{formalboxderived}
    \vfill
    \begin{formalboxbasic}{Negation}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{negA}{\neg\myA}
            \have[j]{A}{\myA}
            \have[\therefore]{bot}{\bot} \ne{negA,A}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \open
                \hypo[i]{hypA}{\myA}
                \have[j]{bot}{\bot}
            \close
            \have[\therefore]{negA}{\neg\myA} \ni{hypA-bot}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxbasic}{Indirect proof}
        \begin{flusheqs}
        \begin{nd}
            \open
                \hypo[i]{negA}{\neg\myA}
                \have[j]{bot}{\bot}
            \close
            \have[\therefore]{A}{\myA} \ip{negA-bot}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxderived}{Double negation}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{negnegA}{\neg\neg\myA}
            \have[\therefore]{A}{\myA} \nne{negnegA}
        \end{nd}
        \end{flusheqs}
    \end{formalboxderived}
    \vfill
    \begin{formalboxderived}{Law of excluded middle}
        \begin{flusheqs}
        \begin{nd}
            \open
                \hypo[i]{A}{\myA}
                \have[j]{BfromA}{\myB}
            \close
            \open
                \hypo[k]{negA}{\neg\myA}
                \have[l]{BfromNegA}{\myB}
            \close
            \have[\therefore]{B}{\myB} \lem{A-BfromA,negA-BfromNegA}
        \end{nd}
        \end{flusheqs}
    \end{formalboxderived}
\end{adjustbox}%
\hfill%
\begin{adjustbox}{minipage=[t][\myheight]{.3\linewidth},valign=t}
    \begin{formalboxbasic}{Explosion}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{bot}{\bot}
            \have[\therefore]{A}{\myA} \x{bot}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxbasic}{Conjunction}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{A}{\myA}
            \have[j]{B}{\myB}
            \have[\therefore]{AandB}{\myA \land \myB} \ai{A,B}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{AandB}{\myA \land \myB}
            \have[\therefore]{A}{\myA} \ae{AandB} \ae{AandB}
            \have[\therefore]{B}{\myB} \ae{AandB} \ae{AandB}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxbasic}{Disjunction}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{A}{\myA}
            \have[\therefore]{AorB}{\myA \lor \myB} \oi{A}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{A}{\myA}
            \have[\therefore]{BorA}{\myB \lor \myA} \oi{A}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{AorB}{\myA \lor \myB}
            \open
                \hypo[i]{hypA}{\myA}
                \have[j]{CfromA}{\myC}
            \close
            \open
                \hypo[k]{hypB}{\myB}
                \have[l]{CfromB}{\myC}
            \close
            \have[\therefore]{C}{\myC} \oe{AorB,hypA-CfromA,hypB-CfromB}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxderived}{Disjunctive syllogism}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{AorB}{\myA \lor \myB}
            \have[j]{negA}{\neg\myA}
            \have[\therefore]{B}{\myB} \ds{AorB,negA}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{AorB}{\myA \lor \myB}
            \have[j]{negB}{\neg\myB}
            \have[\therefore]{A}{\myA} \ds{AorB,negB}
        \end{nd}
        \end{flusheqs}
    \end{formalboxderived}
    \vfill
    \begin{formalboxderived}{Hypothetical syllogism}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{AimpliesB}{\myA \implies \myB}
            \have[j]{BimpliesC}{\myB \implies \myC}
            \have[\therefore]{AimpliesC}{\myA \implies \myC} \hs{AimpliesB,BimpliesC}
        \end{nd}
        \end{flusheqs}
    \end{formalboxderived}
\end{adjustbox}%
\hfill%
\begin{adjustbox}{minipage=[t][\myheight]{.3\linewidth},valign=t}
    \begin{formalboxbasic}{Conditional}
        \begin{flusheqs}
        \begin{nd}
            \open
                \hypo[i]{hypA}{\myA}
                \have[j]{BfromA}{\myB}
            \close
            \have[\therefore]{AimpliesB}{\myA \implies \myB} \ii{hypA-BfromA}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    % \begin{formalboxderived}{Implication}
    %     \begin{flusheqs}
    %     \begin{nd}
    %         \have[m]{AimpliesB}{\myA \implies \myB}
    %         \have[\therefore]{imp}{\neg\myA \lor \myB} \imp{AimpliesB}
    %     \end{nd}
    %     \end{flusheqs}
    % \end{formalboxderived}
    % \vfill
    \begin{formalboxderived}{Contraposition}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{AimpliesB}{\myA \implies \myB}
            \have[\therefore]{contra}{\neg\myB \implies \neg\myA} \contra{AimpliesB}
        \end{nd}
        \end{flusheqs}
    \end{formalboxderived}
    \vfill
    \begin{formalboxbasic}{Biconditional}
        \begin{flusheqs}
        \begin{nd}
            \open
                \hypo[i]{hypA}{\myA}
                \have[j]{BfromA}{\myB}
            \close
            \open
                \hypo[k]{hypB}{\myB}
                \have[l]{AfromB}{\myA}
            \close
            \have[\therefore]{AiffB}{\myA \iff \myB} \ei{hypA-BfromA,hypB-AfromB}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{AiffB}{\myA \iff \myB}
            \have[j]{A}{\myA}
            \have[\therefore]{B}{\myB} \ee{AiffB,A}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[i]{AiffB}{\myA \iff \myB}
            \have[j]{B}{\myB}
            \have[\therefore]{A}{\myA} \ee{AiffB,B}
        \end{nd}
        \end{flusheqs}
    \end{formalboxbasic}
    \vfill
    \begin{formalboxderived}{De Morgan Rules}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{negAorB}{\neg(\myA \lor \myB)}
            \have[\therefore]{negAnegB}{\neg\myA \land \neg\myB} \dm{negAorB}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{negAnegB}{\neg\myA \land \neg\myB}
            \have[\therefore]{negAorB}{\neg(\myA \lor \myB)} \dm{negAnegB}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{negAandB}{\neg(\myA \land \myB)}
            \have[\therefore]{negAornegB}{\neg\myA \lor \neg\myB} \dm{negAandB}
        \end{nd}
        \end{flusheqs}
        \DrawLine{tcbcolframe}
        \begin{flusheqs}
        \begin{nd}
            \have[m]{negAornegB}{\neg\myA \lor \neg\myB}
            \have[\therefore]{negAandB}{\neg(\myA \land \myB)} \dm{negAornegB}
        \end{nd}
        \end{flusheqs}
    \end{formalboxderived}
    \vfill
    \textcolor{colorbasicrule}{\textbf{Green:} basic rules.}\par
    \textcolor{colorderivedrule}{\textbf{Orange:} derived rules.}
    \vfill
    More rules can be found in the \\
    \href{https://forallx.openlogicproject.org}{\enquote{forall~x:~Calgary}} book (\href{https://forallx.openlogicproject.org/forallxyyc.pdf#page=416}{p.~406}).
\end{adjustbox}

\endgroup


\end{document}