A calculus of the absurd
\(\newcommand{\footnotename}{footnote}\)
\(\def \LWRfootnote {1}\)
\(\newcommand {\footnote }[2][\LWRfootnote ]{{}^{\mathrm {#1}}}\)
\(\newcommand {\footnotemark }[1][\LWRfootnote ]{{}^{\mathrm {#1}}}\)
\(\let \LWRorighspace \hspace \)
\(\renewcommand {\hspace }{\ifstar \LWRorighspace \LWRorighspace }\)
\(\newcommand {\mathnormal }[1]{{#1}}\)
\(\newcommand \ensuremath [1]{#1}\)
\(\newcommand {\LWRframebox }[2][]{\fbox {#2}} \newcommand {\framebox }[1][]{\LWRframebox } \)
\(\newcommand {\setlength }[2]{}\)
\(\newcommand {\addtolength }[2]{}\)
\(\newcommand {\setcounter }[2]{}\)
\(\newcommand {\addtocounter }[2]{}\)
\(\newcommand {\arabic }[1]{}\)
\(\newcommand {\number }[1]{}\)
\(\newcommand {\noalign }[1]{\text {#1}\notag \\}\)
\(\newcommand {\cline }[1]{}\)
\(\newcommand {\directlua }[1]{\text {(directlua)}}\)
\(\newcommand {\luatexdirectlua }[1]{\text {(directlua)}}\)
\(\newcommand {\protect }{}\)
\(\def \LWRabsorbnumber #1 {}\)
\(\def \LWRabsorbquotenumber "#1 {}\)
\(\newcommand {\LWRabsorboption }[1][]{}\)
\(\newcommand {\LWRabsorbtwooptions }[1][]{\LWRabsorboption }\)
\(\def \mathchar {\ifnextchar "\LWRabsorbquotenumber \LWRabsorbnumber }\)
\(\def \mathcode #1={\mathchar }\)
\(\let \delcode \mathcode \)
\(\let \delimiter \mathchar \)
\(\def \oe {\unicode {x0153}}\)
\(\def \OE {\unicode {x0152}}\)
\(\def \ae {\unicode {x00E6}}\)
\(\def \AE {\unicode {x00C6}}\)
\(\def \aa {\unicode {x00E5}}\)
\(\def \AA {\unicode {x00C5}}\)
\(\def \o {\unicode {x00F8}}\)
\(\def \O {\unicode {x00D8}}\)
\(\def \l {\unicode {x0142}}\)
\(\def \L {\unicode {x0141}}\)
\(\def \ss {\unicode {x00DF}}\)
\(\def \SS {\unicode {x1E9E}}\)
\(\def \dag {\unicode {x2020}}\)
\(\def \ddag {\unicode {x2021}}\)
\(\def \P {\unicode {x00B6}}\)
\(\def \copyright {\unicode {x00A9}}\)
\(\def \pounds {\unicode {x00A3}}\)
\(\let \LWRref \ref \)
\(\renewcommand {\ref }{\ifstar \LWRref \LWRref }\)
\( \newcommand {\multicolumn }[3]{#3}\)
\(\require {textcomp}\)
\(\newcommand {\LWRmarginnote }[1][]{}\)
\(\newcommand {\marginnote }[2][]{\qquad {\small \textrm {#2}}\LWRmarginnote }\)
\(\def \LWRsidenote {1}\)
\(\newcommand {\sidenotemark }[1][\LWRsidenote ]{{}^{\mathrm {#1}}}\)
\(\newcommand {\intertext }[1]{\text {#1}\notag \\}\)
\(\let \Hat \hat \)
\(\let \Check \check \)
\(\let \Tilde \tilde \)
\(\let \Acute \acute \)
\(\let \Grave \grave \)
\(\let \Dot \dot \)
\(\let \Ddot \ddot \)
\(\let \Breve \breve \)
\(\let \Bar \bar \)
\(\let \Vec \vec \)
\(\newcommand {\nicefrac }[3][]{\mathinner {{}^{#2}\!/\!_{#3}}}\)
\(\newcommand {\unit }[2][]{#1 \mathinner {#2}}\)
\(\newcommand {\unitfrac }[3][]{#1 \mathinner {{}^{#2}\!/\!_{#3}}}\)
\(\newcommand {\bm }[1]{\boldsymbol {#1}}\)
\(\require {mathtools}\)
\(\newenvironment {crampedsubarray}[1]{}{}\)
\(\newcommand {\smashoperator }[2][]{#2\limits }\)
\(\newcommand {\SwapAboveDisplaySkip }{}\)
\(\newcommand {\LaTeXunderbrace }[1]{\underbrace {#1}}\)
\(\newcommand {\LaTeXoverbrace }[1]{\overbrace {#1}}\)
\(\newcommand {\LWRmultlined }[1][]{\begin {multline*}}\)
\(\newenvironment {multlined}[1][]{\LWRmultlined }{\end {multline*}}\)
\(\let \LWRorigshoveleft \shoveleft \)
\(\renewcommand {\shoveleft }[1][]{\LWRorigshoveleft }\)
\(\let \LWRorigshoveright \shoveright \)
\(\renewcommand {\shoveright }[1][]{\LWRorigshoveright }\)
\(\newcommand {\shortintertext }[1]{\text {#1}\notag \\}\)
\(\newcommand {\vcentcolon }{\mathrel {\unicode {x2236}}}\)
\(\newcommand {\Var }{\operatorname {Var}}\)
\(\newcommand {\Expected }{\operatorname {E}}\)
\(\newcommand {\abs }[1]{\left \lvert #1\right \rvert }\)
\(\newcommand {\norm }[1]{\left \lVert #1\right \rVert }\)
\(\newcommand {\rbrackets }[1]{\left (#1\right )}\)
\(\newcommand {\sbrackets }[1]{\left [#1\right ]}\)
\(\newcommand {\cbrackets }[1]{\left \{#1\right \}}\)
Chapter 19 Lowerlevel logic
One of the wonderful things about logic is that one can study it at many different levels. In the previous section, a “working subset” of logic which is kind of necessary (and remarkably, also sufficient) for all other mathematics was described. In this section, I write down many amazing
things I have discovered on the internet, which allow us to develop logics (yes, logics in the plural) for various purposes.
At this point we are no longer entirely in the realm of mathematics proper  it really sits on the boundary between philosophy and mathematics. There are a few fundamental questions we are interested in the answer to,

• what does it mean for something to be true?

• when is something true?

• how can we prove that something is true?

• can we mechanise our intuitions about whether or not something is true (this is essentially equivalent to the question “can we codify mathematics on a computer”, but not completely)
19.1 Proof systems
In Chapter 5 a lot of methods for proving things were given, but it was kind of given that these work, and are valid methods of proof. This begs the question (well if it doesn’t, them I’m begging it now)  “can we prove our proof techniques”?
First we can try to develop a system for telling us if something is true. There are multiple ways in which we can try to do this, but one specific idea is that we can define a “proof system”, which is a mathematical construct that allows us to reason about proofs.

Definition 19.1.1 A proof system \(\Pi \) is a fourtuple
\(\seteqnumber{0}{19.}{0}\)
\begin{equation}
\Pi = (\tau , \phi , \mathcal {P}, S).
\end{equation}
Here \(\tau \), \(\phi \), \(\mathcal {P}\) and \(S\) have specific meanings

• The set \(S\) of all possible statements in our proof system.

• The set \(\mathcal {P}\) is the set of all possible proofs in our proof system.

• The function \(\tau : S \to \{0, 1\}\) defines whether a given statement is true or not (as eone might guess, if \(\tau (x) = 1\), then the statement \(x\) is true, and otherwise it is false.

• The function \(\phi : S \times \mathcal {P} \to \{0, 1\}\) is called a verification function and takes a proof \(\mathcal {P}\) for a statement \(S\) and returns \(1\) if this is a valid proof of \(S\), and false if it is not.
There are two key attributes of proof systems that we are primarily interested in; these are soundness and completeness.

Definition 19.1.2 A proof system \(\Pi \) is sound if and only if for every \(s \in S, p \in \mathcal {P}\) such that
\(\seteqnumber{0}{19.}{1}\)
\begin{equation}
\phi (s, p) = 1,
\end{equation}
the statement \(s\) is true, i.e.
\(\seteqnumber{0}{19.}{2}\)
\begin{equation}
\tau (s) = 1.
\end{equation}
In natural language, I would read this as “a proof system is sound if and only if every statement for which there is a valid proof is true”. This is the property that we most interested in; as the name suggests unsound proof systems are not particularly useful!

Definition 19.1.3 A proof system is complete if there is a proof for every true statement; that is for every \(s \in S\) such that
\(\seteqnumber{0}{19.}{3}\)
\begin{equation}
\tau (s) = 1,
\end{equation}
there exists some \(p \in \mathcal {P}\) which is a proof of \(s\)  that is, for this \(p\)
\(\seteqnumber{0}{19.}{4}\)
\begin{equation}
\phi (s, p) = 1.
\end{equation}
This is less useful than soundness, but it is still an interesting property to think about.