% OWD, 2023--2024

\documentclass{article}

\usepackage[
    a4paper,
    top=1.5in,
    bottom=1.5in,
    left=1in,
    right=1in,
]{geometry}
\usepackage{ebproof, amsmath, amssymb, titlesec, mathtools}
\usepackage[en-GB]{datetime2}
\usepackage{hyperref}

\setlength\parindent{0pt}
\setlength\parskip{1em}
\titlespacing*\subsection{0pt}{1ex}{1ex}

\newenvironment{rulesection}[1]
    {
        \subsection{#1}
        \large
        \begin{center}
    }{
        \end{center}
    }

\newcommand\subproof[1]{%
    \begingroup
        \renewcommand*\arraystretch{.75}
        \ensuremath\fbox{$\begin{matrix}#1\end{matrix}$}
    \endgroup
}

\renewcommand\implies{\rightarrow}
\renewcommand\iff{\leftrightarrow}
\newcommand\txlabel[1]{\textsf{#1}}
\newcommand\oplabel[2]{$ \mathbin{#1}\text{\txlabel{#2}} $}
\newcommand\trueprem{\ensuremath\text{\txlabel{T}}}
\newcommand\invariant{\ensuremath\text{\txlabel{I}}}
\newcommand\hoare[3]{\ensuremath\left\{#1\right\}#2\left\{#3\right\}}
\newcommand\dotsep{\enspace\textbf{\textperiodcentered}\enspace}
\makeatletter
\renewcommand\tableofcontents{\@starttoc{toc}}
\makeatother

\title{Logic: Deduction Rules}
\author{Oliver Dixon}
\newcommand\email{\texttt{<\href{mailto:od641@york.ac.uk}{od641@york.ac.uk}>}}

\begin{document}
\begingroup
    \makeatletter
    \huge \@title
    \hfill \normalsize
    \parbox{.4\linewidth}{\raggedleft \@author~\email\\Compiled \today}
    \makeatother
    \vskip\parskip \hrule
\endgroup
\tableofcontents

\vfill\hrule
Unless stated otherwise, sentences in the propositional calculus are denoted by
$ \phi $, $ \psi $, and $ \chi $. The logical bottom is denoted by $ \bot $, and
$ \trueprem $ indicates an `empty set' of premises that universally hold true.
Logical name labels are set in a sans serif typeface (e.g. \txlabel{MT} for
modus tollens). Boxed premises represents sub-proofs.

In the predicate calculus, predicates are represented by capital Latin or
lowercase Greek letters, using parentheses for constant application and brackets
for substitution of a hypothetical individual; e.g. $ P(a) $, or $ \phi[x
\mapsto x_0] $. Hoare triples are composed of the precondition, followed by the
(partial) program/program name, followed by the postcondition; e.g. $ \hoare{x >
0}{x \coloneq x + 1}{x \geq 1} $. A fixed invariant is notated as $ \invariant
$.

\clearpage
\section{Propositional Calculus}
\begin{rulesection}{Conjunction}
    \begin{prooftree}
        \hypo{\phi \quad \psi}
        \infer1[\oplabel{\land}{I}]{\phi \land \psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \land \psi}
        \infer1[\oplabel{\land}{E\textsubscript{1}}]{\phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \land \psi}
        \infer1[\oplabel{\land}{E\textsubscript{2}}]{\psi}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Disjunction}
    \begin{prooftree}
        \hypo{\phi}
        \infer1[\oplabel{\lor}{I\textsubscript{1}}]{\phi \lor \psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\psi}
        \infer1[\oplabel{\lor}{I\textsubscript{2}}]{\phi \lor \psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \lor \psi \quad \subproof{\phi \\ \vdots \\ \chi}
            \quad \subproof{\psi \\ \vdots \\ \chi}}
        \infer1[\oplabel{\lor}{E}]{\chi}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Negation and Contradiction}
    \begin{prooftree}
        \hypo{\phi}
        \infer1[\oplabel{\lnot\lnot}{I}]{\lnot\lnot\phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\lnot\lnot\phi}
        \infer1[\oplabel{\lnot\lnot}{E}]{\phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \quad \lnot\phi}
        \infer1[\oplabel{\lnot}{E}]{\bot}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\subproof{\phi \\ \vdots \\ \bot}}
        \infer1[\oplabel{\lnot}{I}]{\lnot\phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\bot}
        \infer1[\oplabel{\bot}{E}]{\psi}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Conditional}
    \begin{prooftree}
        \hypo{\subproof{\phi \\ \vdots \\ \psi}}
        \infer1[\oplabel{\implies}{I}]{\phi \implies \psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \quad \phi \implies \psi}
        \infer1[\oplabel{\implies}{E}]{\psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \implies \psi \quad \lnot\psi}
        \infer1[\txlabel{MT}]{\lnot\phi}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{De Morgan's Laws}
    \begin{prooftree}
        \hypo{\lnot(\phi \lor \psi)}
        \infer1[\txlabel{DeM\textsubscript{1}}]{\lnot\phi \land \lnot\psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\lnot(\phi \land \psi)}
        \infer1[\txlabel{DeM\textsubscript{2}}]{\lnot\phi \lor \lnot \psi}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Proof-by-Contradiction and the Law of the Excluded Middle}
    \begin{prooftree}
        \hypo{\subproof{\lnot\phi \\ \vdots \\ \bot}}
        \infer1[\txlabel{PBC}]{\phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\trueprem}
        \infer1[\txlabel{LEM}]{\phi \lor \lnot\phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\subproof{\phi \\ \vdots \\ \chi} \quad \subproof{\lnot\phi \\
            \vdots \\ \chi}}
        \infer1[\txlabel{LEM-Carnap}]{\chi}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Biconditional}
    \begin{prooftree}
        \hypo{\subproof{\phi \\ \vdots \\ \psi} \quad
            \subproof{\psi \\ \vdots \\ \phi}}
        \infer1[\oplabel{\iff}{I}]{\phi \iff \psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \iff \psi \quad \phi}
        \infer1[\oplabel{\iff}{E\textsubscript{1}}]{\psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \iff \psi \quad \psi}
        \infer1[\oplabel{\iff}{E\textsubscript{2}}]{\phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\phi \iff \psi \quad \lnot\phi}
        \infer1[\txlabel{BMT}]{\lnot\psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\lnot(\phi \iff \psi)}
        \infer1[\txlabel{NBD\textsubscript{1}}]{\lnot\phi \iff \psi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\lnot(\phi \iff \psi)}
        \infer1[\txlabel{NBD\textsubscript{2}}]{\phi \iff \lnot\psi}
    \end{prooftree}
\end{rulesection}

\section{Predicate Calculus}
\begin{rulesection}{Equality}
    \begin{prooftree}
        \hypo{\trueprem}
        \infer1[\oplabel{=}{I}]{t=t}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{t_1=t_2 \quad \phi[x \mapsto t_1]}
        \infer1[\oplabel{=}{E}]{\phi[x \mapsto t_2]}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Universal Introduction and Elimination}
    \begin{prooftree}
        \hypo{\subproof{x_0 \\ \vdots \\ \phi[x \mapsto x_0]}}
        \infer1[\oplabel{\forall}{I}]{\forall x \, \phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\forall x \, \phi}
        \infer1[\oplabel{\forall}{E}]{\phi[x \mapsto t]}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Existential Introduction and Elimination}
    \begin{prooftree}
        \hypo{\phi[x \mapsto t]}
        \infer1[\oplabel{\exists}{I}]{\exists x \, \phi}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\exists x \, \phi \quad \subproof{x_0 \quad \phi[x \mapsto x_0] \\
            \vdots \\ \chi}}
        \infer1[\oplabel{\exists}{E}]{\chi}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Induction and Strong Induction}
    \begin{prooftree}
        \hypo{P[n \mapsto 0] \quad \subproof{k \quad P[n \mapsto k] \\ \vdots \\
            P[n \mapsto k+1]}}
        \infer1[\oplabel{\mathbb{N}}{I}]{\forall n \in \mathbb{N} \, P}
    \end{prooftree}\qquad
    \begin{prooftree}
        \hypo{\subproof{\forall k < m \quad P[n \mapsto k] \\ \vdots \\
            P[n \mapsto m]}}
        \infer1[\oplabel{\mathbb{N}}{SI}]{\forall n \in \mathbb{N} \, P}
    \end{prooftree}
\end{rulesection}

\section{Hoare Logic}
\begin{rulesection}{Skip}
    \begin{prooftree}
        \hypo{P \implies Q}
        \infer1[\txlabel{hskip}]{\hoare{P}{\text{skip}}{Q}}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Assignment}
    \begin{prooftree}
        \hypo{P \implies Q\left[x \mapsto e\right]}
        \infer1[\txlabel{hassign}]{\hoare{P}{x \coloneq e}{Q}}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Conditional}
    \begin{prooftree}
        \hypo{\hoare{P \land B}{C_1}{Q} \quad
            \hoare{P \land \lnot B}{C_2}{Q}}
        \infer1[\txlabel{hcond}]{\hoare{P}{\text{if } B \text{ then } C_1
            \text{ else } C_2}{Q}}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Sequential Composition}
    \begin{prooftree}
        \hypo{\hoare{P}{C_1}{Q} \quad \hoare{Q}{C_2}{R}}
        \infer1[\txlabel{hseq}]{\hoare{P}{C_1;\, C_2}{R}}
    \end{prooftree}
\end{rulesection}
\begin{rulesection}{Iteration}
    \begin{prooftree}
        \hypo{P \implies \invariant \quad \hoare{I \land B}{C}{\invariant} \quad
            \invariant \land \lnot B \implies Q}
        \infer1[\txlabel{hwhile}]{\hoare{P}{\text{while } B \text{ do } C}{Q}}
    \end{prooftree}
\end{rulesection}
%
%
%
\vfill\raggedleft\textsc{End.}
\end{document}

