# What If Turing Had Preceded Gödel?

$\mathsf{S}$ebastian $\mathsf{0}$berhoff
<EMAIL_ADDRESS>
###### Abstract

The overarching theme of the following pages is that mathematical
logic—centered around the incompleteness theorems—is first and foremost an
investigation of _computation_ , not arithmetic. Guided by this intuition we
will show the following.

  * •

First, we’ll all but eliminate the need for Gödel numbers.

  * •

Next, we’ll introduce a novel notational device for representable functions
and walk through a condensed demonstration that Peano Arithmetic can represent
every computable function. It has achieved Turing completeness.

  * •

Continuing, we’ll derive the Diagonal Lemma and First Incompleteness Theorem
using significantly simplified proofs.

  * •

Approaching the Second Incompleteness Theorem, we’ll be able to use some self-
referential trickery to avoid much of the technical morass surrounding it;
arriving at three separate versions.

  * •

Extending the analogy between the First Incompleteness Theorem and the
Unsolvability of the Halting Problem produces an equivalent of the
Nondeterministic Time Hierarchy Theorem from the field of computational
complexity.

  * •

Lastly, we’ll briefly peer into the realm of the uncomputable by connecting
our ideas to oracles.

> In March of 1977, I met the great AI pioneer Marvin Minsky for the first
> time. It was an unforgettable experience. One of the most memorable remarks
> he made to me was this one: “Gödel should just have thought up Lisp; it
> would have made the proof of his theorem much easier.” I knew exactly what
> Minksy meant by that, I could see a grain of truth in it, and moreover I
> knew it had been made with tongue semi in cheek.
>
> Douglas Hofstadter

Illustration by ManBroDude

##  1 Introduction

Ever since 1931 the main protagonist in any telling of mathematical logic has
always been Kurt Gödel and his First Incompleteness Theorem. Roughly speaking
this theorem states that any sensible, sufficiently powerful formal system is
incomplete; it’ll contain a statement that is neither provable nor
disprovable.

However, while the statement of the theorem is quite simple, the proof is a
very different matter. Entire books, both technical and non-technical, have
been devoted to it over the years; some of which, I’m assuming in the sequel,
you’re already familiar with. Where does this complexity come from? And what
can be done about it? These are questions I already addressed in [8], though
in a rather inexact manner. Indeed, back then I explicitly left important
details to “smarter people” in the conclusion. Now, some time later, and
hopefully a little smarter, I want to return to the question and provide a
more precise answer myself.

To that end let’s start with a high-level overview of the famous 1931 paper
titled “On Formally Undecidable Propositions Of Principia Mathematica And
Related Systems” [4]. In this paper Gödel dealt with a formal system he had
adapted from work by Bertrand Russel and Alfred North Whitehead published in
three volumes of the _Principia Mathematica_ between 1910 and 1913. This
system was based on type theory, a rather tedious framework which has since
fallen out of favor. But its central pillar—Peano Arithmetic—has stood the
test of time. It defines the natural numbers and is built as follows.

[Theory] A theory is a set of formal sentences which is closed under logical
consequence. Furthermore, if T' and T are theories such that
$\textbf{{T}}\emph{\textquotesingle}\subseteq\textbf{{T}}$, then we’ll say
that T is an _extension_ of T'. And if $\mathsf{A}$ is a sentence such that
$\mathsf{A}\in\textbf{{T}}$, then we’ll instead write
$\textbf{{T}}\vdash\mathsf{A}$ which reads as “T proves $\mathsf{A}$”.

We’ll only consider first-order theories with equality.

For practical purposes “being a logical consequence” is going to mean
“derivable using informal natural deduction” to us.

[Robinson Arithmetic] The theory of _Robinson Arithmetic_ , or Q for short, is
defined from the following axioms.

_Axioms Of Successorship_ :

$\forall\mathsf{x}\colon\neg\,\mathsf{S}\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$

$\forall\mathsf{x},\mathsf{y}\colon\mathsf{S}\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{y}\rightarrow\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}$

$\forall\mathsf{x}\colon\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}\lor\exists\mathsf{y}\colon\mathsf{S}\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{x}$

_Axioms Of Arithmetic_ :

$\displaystyle\forall\mathsf{x}\colon$
$\displaystyle\mathsf{x}+\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{x}$
(A0) $\displaystyle\forall\mathsf{x},\mathsf{y}\colon$
$\displaystyle\mathsf{x}+\mathsf{S}\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}(\mathsf{x}+\mathsf{y})$
(A1)

$\displaystyle\forall\mathsf{x}\colon$
$\displaystyle\mathsf{x}\times\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$
(M0) $\displaystyle\forall\mathsf{x},\mathsf{y}\colon$
$\displaystyle\mathsf{x}\times\mathsf{S}\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{x}+(\mathsf{x}\times\mathsf{y})$
(M1)

[Peano Arithmetic] The theory of _Peano Arithmetic_ , or PA for short, is
defined using all the axioms of Q as well as the following axiom schema.

_Induction_ :

$(\mathsf{P}(\mathsf{0})\land\forall\mathsf{x}\colon\mathsf{P}(\mathsf{x})\rightarrow\mathsf{P}(\mathsf{S}\mathsf{x}))\rightarrow\forall\mathsf{x}\colon\mathsf{P}(\mathsf{x})$
for any formula $\mathsf{P}$.

The main reason Q is interesting is that it is a finitely axiomatized and
fairly weak theory. It can’t even prove the commutativity of addition. Yet it
still suffices to prove many of our results. So separating it out from PA
allows us to state our theorems in their sharpest form.

With all that in mind, here are the major steps in Gödel’s 1931 proof:

_Gödel Numbering_ :

Akin to modern-day ASCII encoding, Gödel first turned every string and list of
strings into a number.

_Computability_ :

Using the model of computation known as primitive recursive functions Gödel
then implemented a proof verifier in full detail, showing that PA is
computably enumerable.111I am in full agreement with Robert I. Soare [10] that
“computably enumerable” should replace “recursively enumerable”.

_Representation_ :

Next, Gödel briefly pointed out that PA could represent—that is reason
about—primitive recursive functions, and thereby its own proof verifier.

_Diagonalization_ :

Finally, having equipped PA with the ability of introspection, Gödel
diagonalized against provability-in-PA. This produced a sentence asserting its
own unprovability, leading to the First Incompleteness Theorem: PA can’t
decide every sentence.

_Re-Representation_ :

Almost as an afterthought, Gödel noted that the proof of the First
Incompleteness Theorem could be carried out within PA. By a simple argument
this gave his Second Incompleteness Theorem: PA couldn’t prove its own
consistency.

This, in essence, is still the argument given to this day. And we’re not going
to modify its basic structure either. Rather we’ll take these items one by one
and see where simplifications can be made.

##  2 Gödel Numbering

While today there is an unending variety of computational models, stretching
from Diophantine equations to the RISC-V instruction set architecture, back in
1931 there were only very few available options. That’s why when Gödel drew
the primitive recursive functions from the shelf the very first challenge he
faced was a simple type error. The formal system he was working with was built
out of strings over an exotic character set whereas primitive recursive
functions only mapped natural numbers to natural numbers. If one wanted to
devise a proof verifier in this model of computation, some type conversion
would be unavoidable. So that’s exactly what Gödel did using a scheme that
since has become known as Gödel numbering.

Yet driven primarily by necessity as opposed to elegance, Gödel ended up
constructing a rather roundabout numbering involving products of prime numbers
raised to various powers. Considering the time at which Gödel was writing this
is obviously quite understandable. What’s more difficult to explain is the
enduring popularity of Gödel’s original scheme. After all, there’s a much more
natural mapping: read every formal string as a natural number that has been
written in base $k$ where $k$ is the size of our alphabet. To see this idea in
action just consider hexadecimal notation where the letters “A”–“F” are used
to represent the numbers 10–15. Furthermore, sequences of strings can be
handled much more straightforwardly by introducing a new-line character.

Looking at it from this angle there’s really no Gödel numbering left worth
mentioning. It’s just a change of script. And if prime numbers ever turn out
to be more convenient later on, then all that’s required is to add a pre-
processor which converts from the powers-of-$k$ to the powers-of-primes
encoding. Doing so can be done even using primitive recursive functions
without encountering major obstacles.

Okay, so maybe that is a little simpler, you might say. But _strictly
speaking_ isn’t this still a Gödel numbering? Sure. That is unless you take it
one step further. One only has to reinterpret the formal symbol “$\mathsf{0}$”
to indicate the first string and “$\mathsf{S}$” to indicate the
lexicographical successor function. At that point Gödel numbers are truly
gone.

However, as tempting as this approach towards unification may be, it also
harbors the potential for a lot of confusion. Setting up string addition and
string multiplication etc., while technically unobjectionable, brings with it
significant mental overhead, simply because we’re not used to treating strings
in this fashion. So instead of treating everything as a string let’s go the
other way and treat everything as a number. In particular, we’ll regard our
formal strings as already being natural numbers. These numbers are written
using the conventional symbols of the language of arithmetic. And the corner
quotes usually employed to denote Gödel numbers will be used to point directly
to numerals instead.

###  2.1 Numerals

When handling collections of items we’ll employ boldface variables to avoid
clutter. E.g., $\bm{x}\coloneqq x_{1},\dots,x_{k}$.

[Numeral] Let $x\in\mathbb{N}$. Then

$\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\enskip\coloneqq\enskip\mathsf{S\dots S0}$

where $\mathsf{S}$ is repeated $x$ times. We’ll call $\ulcorner$$x$$\urcorner$
the _numeral_ of $x$. Also, $\ulcorner$$\bm{x}$$\urcorner$ is to be taken
element-wise.

[Ordering] The $<$ relation is defined in terms of addition as follows.

$\displaystyle\mathsf{x}<\mathsf{y}$
$\displaystyle\enskip\coloneqq\enskip\exists\mathsf{z}\colon\mathsf{S}\mathsf{z}+\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y},$
$\displaystyle\mathsf{x}\leq\mathsf{y}$
$\displaystyle\enskip\coloneqq\enskip\mathsf{x}<\mathsf{y}\lor\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}.$

Now is a good time to collect our first batch of basic lemmas.

[Monotonicity Of Successorship]

$\textbf{{Q}}\vdash\forall\mathsf{x},\mathsf{y}\colon\mathsf{x}<\mathsf{y}\leftrightarrow\mathsf{S}\mathsf{x}<\mathsf{S}\mathsf{y}.$

###### Proof.

Let $\mathtt{x},\mathtt{y}$ and $\mathtt{z}$ be arbitrary. Then we can see
$\mathsf{S}\mathtt{z}+\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{y}\,\leftrightarrow\,\mathsf{S}(\mathsf{S}\mathtt{z}+\mathtt{x})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}\quad\text{and}\quad\mathsf{S}(\mathsf{S}\mathtt{z}+\mathtt{x})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}\,\leftrightarrow\,\mathsf{S}\mathtt{z}+\mathsf{S}\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}$
by Leibniz’s law (substitution of equals), _Axioms Of Successorship_ :, and
A1. This of course contracts to
$\mathtt{x}<\mathtt{y}\leftrightarrow\mathsf{S}\mathtt{x}<\mathsf{S}\mathtt{y}$.
∎

[Totality Of Ordering With Respect To Numerals] For any $n\in\mathbb{N}$:

$\textbf{{Q}}\vdash\forall\mathsf{x}\colon\mathsf{x}<\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\lor\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}<\mathsf{x}\lor\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}.$

###### Proof.

By induction on $n$. _Base Case_ : Suppose $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{0}$. And let $\mathtt{x}$ be
arbitrary. Then by _Axioms Of Successorship_ : we have two cases to consider.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$_ :
Then trivially
$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}$_
: Here $\mathsf{S}\mathtt{y}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}+\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{x}$
by A0 and hence $\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}<\mathtt{x}$. _Induction_ : Suppose
$\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ for some $m\in\mathbb{N}$. And let
$\mathtt{x}$ be arbitrary again. Then once more by _Axioms Of Successorship_
:. _$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$_
: Then $\mathsf{S}\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ by A0 and hence $\mathtt{x}<\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}$_
: Here we have $\mathtt{y}<\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\lor\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}<\mathtt{y}\lor\mathtt{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ by inductive hypothesis, whereby
$\mathtt{x}<\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\lor\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}<\mathtt{x}\lor\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ using monotonicity and Leibniz’s law.∎

[Non-Negativity Lemma]

$\textbf{{Q}}\vdash\forall\mathsf{x}\colon\neg\,\mathsf{x}<\mathsf{0}.$

###### Proof.

By way of contradiction, let $\mathtt{x}$ be an arbitrary object such that
$\mathtt{x}<\mathsf{0}$. Then by definition we can obtain a $\mathtt{z}$ such
that
$\mathsf{S}\mathtt{z}+\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$.
We now use _Axioms Of Successorship_ : to distinguish two cases.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$_ :
Then by A0 we have
$\mathsf{S}\mathtt{z}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{z}+\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{z}+\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$
which contradicts _Axioms Of Successorship_ :.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}$_
: Then by A1 we have
$\mathsf{S}(\mathsf{S}\mathtt{z}+\mathtt{y})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{z}+\mathsf{S}\mathtt{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{z}+\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$
which again contradicts _Axioms Of Successorship_ :.∎

[Bounded Quantifier] We’ll employ the following shorthand for any formula
$\mathsf{P}$:

$\displaystyle\forall\mathsf{x}<\mathsf{y}\colon\mathsf{P}(\mathsf{x},\mathsf{y})$
$\displaystyle\quad\coloneqq\quad\forall\mathsf{x}\colon\mathsf{x}<\mathsf{y}\rightarrow\mathsf{P}(\mathsf{x},\mathsf{y}),$
$\displaystyle\exists\mathsf{x}<\mathsf{y}\colon\mathsf{P}(\mathsf{x},\mathsf{y})$
$\displaystyle\quad\coloneqq\quad\exists\mathsf{x}\colon\mathsf{x}<\mathsf{y}\land\mathsf{P}(\mathsf{x},\mathsf{y}).$

The same goes for $\leq$. Such a quantifier is also referred to as a _bounded
quantifier_.

[Bounded Quantification Lemma] For any $n\in\mathbb{N}$:

$\textbf{{Q}}\vdash\forall\mathsf{x}<\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\colon\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}\lor\dots\lor\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}.$

###### Proof.

By induction on $n$. _Base Case_ : Suppose $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{0}$. Then we need to establish
$\mathtt{x}<\mathsf{S}\mathsf{0}\rightarrow\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$
for an arbitrary $\mathtt{x}$. By _Axioms Of Successorship_ : there are two
cases.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$_ :
This case is trivial.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}$_
: This assumption allows us to rule out the antecedent. By way of
contradiction, assume $\mathtt{x}<\mathsf{S}\mathsf{0}$. Then
$\mathtt{y}<\mathsf{0}$ by monotonicity. But this contradicts non-negativity.
_Induction_ : Suppose $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ for some $m\in\mathbb{N}$. And let
$\mathtt{x}$ be arbitrary again. Then one last time by _Axioms Of
Successorship_ :.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$_ :
This case is trivial.
_$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{y}$_
: Then $\mathtt{x}<\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ implies $\mathtt{y}<\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ by monotonicity. Therefore, by the
inductive hypothesis,
$\mathtt{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}\lor\dots\lor\mathtt{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$m$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. And so
$\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{0}\lor\dots\lor\mathtt{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$n$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$.∎

##  3 Computability

This section is the most infamous in Gödel’s original proof. It’s a chain of
46 definitions, up to 3 lines each, spread over four pages, altogether
implementing a proof verifier for PA using primitive recursive
functions.222Gödel actually gave a relation here, not a function. But that
muddles the boundary between the different sections, so I prefer to stick to
functions here. Really though, it’s nothing more than an painstaking
demonstration that proofs for PA could be checked by a computer. Back in 1931
mathematicians may have had every right to be doubtful of this claim. This was
long before we built actual computers and familiarized ourselves with high-
level programming languages. And most importantly, it was before the field of
computer science fully dawned in 1936 with the universal acceptance of the
following thesis.

[Church-Turing Thesis] Every computable function can be computed by a Turing
machine (or equivalently by a $\lambda$-calculus expression, or by a general
recursive function, etc.).

The exact status of the Church-Turing Thesis is still debated. Is it a
definition? Is it a law of nature? Regardless, for us it’s going to be nothing
more than a bridge between intuition and rigor. Rather than having to spill
pages upon pages of ink writing code in the assembly language of general
recursive functions, we’re going to allow ourselves to write simple
pseudocode. At that point we’ll exclaim “clearly, that’s computable”, and then
continue on under the assumption that, if called upon, we could always compile
our pseudocode down into any desired universal model of computation.

Using this modern perspective we can then distill this section into its
essence like so.

[✗, ✓] The symbols “✗” and “✓” indicate rejection and acceptance respectively.
They can be taken to be arbitrary constants (e.g. 0 and 1). Their only
important feature is that they’re distinct.

[Proof Verifier] A function
$\operatorname{\mathit{pv}}\colon\mathbb{N}^{2}\to\\{\text{\small\char
55},\text{\small\char 51}\\}$ is called a _proof verifier_ for some theory T
if whenever $\textbf{{T}}\vdash\mathsf{A}$, then
$\operatorname{\mathit{pv}}(p,\mathsf{A})=\text{\small\char 51}$ for some
$p\in\mathbb{N}$, and otherwise
$\operatorname{\mathit{pv}}(p,\mathsf{A})=\text{\small\char 55}$.

[Computably Enumerable Theory] A theory T is considered to be computably
enumerable if there exists a computable proof verifier for T.

Q and PA are computably enumerable theories.

###### Proof Sketch.

The following implementation of $\operatorname{\mathit{pv}}$ will do.
$\operatorname{\mathit{pv}}(p,x)$ for $l\in\text{ lines of }p$ if $l$ is not
an axiom and $l$ doesn’t follow from the previous lines  return ✗ if the last
line of $p$ isn’t $x$ return ✗ return ✓ ∎

##  4 Representation

Next, we turn to an extremely important section of the proof; the
representation of computable functions as formulas. Roughly speaking, for a
function $f$ to be represented in a theory T means that if $f(x)=y$, then T
can prove this fact. And it does so by use of a single formula called “the
representation of $f$”.

[Unique Existence] For any formula $\mathsf{P}$

$\exists!\mathsf{x}\colon\mathsf{P}(\mathsf{x})\quad\coloneqq\quad\exists\mathsf{x}\colon\mathsf{P}(\mathsf{x})\land\forall\mathsf{y}\colon\mathsf{P}(\mathsf{y})\rightarrow\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{x}.$

[Representable Function] Let T be a theory containing the axioms of
successorship. Then a partial function $f\colon\mathbb{N}^{k}\to\mathbb{N}$ is
said to be _represented_ in T if there exists a formula ‹$f$› with $k+1$ free
variables such that whenever $f(\bm{x})=y$ then

$\textbf{{T}}\vdash\exists!\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y})\land\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}).$

Informally the above sentence says “$f(\bm{x})$ _only_ outputs $y$”.

As already stated, the concept of representability will be absolutely central
for the remainder of this presentation. But notationally it’s still a bit of a
mouthful. We’re frequently going to find ourselves wanting to assert that the
output of $f(\bm{x})$ obeys some predicate $\mathsf{P}$. Wouldn’t it be nice
if we could make this assertion by simply writing $\mathsf{P}(f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}))$? We may not be able to write $f$
directly into our formulas. But no matter, we can simply declare
$\mathsf{P}(f(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}))$ to be shorthand for
$\exists\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y})\land\mathsf{P}(\mathsf{y})$.

This is something other people have already come up with and they’ve
christened such appearances of $f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})$ “pseudo-terms”. However, while it’s a
step in the right direction, pseudo-terms still have some significant
shortcomings. Most importantly, because pseudo-terms don’t guarantee the
uniqueness of $f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})$’s output Leibniz’s law breaks down.
This means that if one derives $f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}g(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{z}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})$, then one can’t easily conclude
$\mathsf{P}(f(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}))\leftrightarrow\mathsf{P}(g(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{z}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}))$. Most grievously, this has the
consequence that equalities of pseudo-terms don’t enjoy transitivity.

The situation brings to mind a wise quote by Alfred North Whitehead: “By
relieving the brain of all unnecessary work, a good notation sets it free to
concentrate on more advanced problems, and in effect increases the mental
power of the race.” In this vein, what follows may appear as a bit of a
diversion. But it’ll pay untold dividends in the long run.

[Representable Function Symbol & Representable Term] Let $f$ be represented in
T. Then we’ll allow “$f$” to appear in our formal strings anywhere a regular
function symbol could appear. We’ll refer to such function symbols as
_representable function symbols_. And terms containing representable function
symbols are called _representable terms_.

In order to disabbreviate representable function symbols from some expression
we proceed as follows. Let our expression be of the form
$\mathsf{P}(f(\bm{\mathsf{r}}))$ where $\mathsf{P}$ is the smallest sub-
formula containing $f$ and $f$ is one of the innermost occurrences of a
representable function symbol, meaning $\bm{\mathsf{r}}$ is a collection of
regular terms. Then we perform the following expansion:

$\mathsf{P}(f(\bm{\mathsf{r}}))\quad\coloneqq\quad(\exists!\mathsf{y}\colon
f(\bm{\mathsf{r}},\mathsf{y}))\land(\exists\mathsf{y}\colon
f(\bm{\mathsf{r}},\mathsf{y})\land\mathsf{P}(\mathsf{y})).$

And then we continue expanding $\mathsf{P}(\mathsf{y})$ in this way until all
representable function symbols have been eliminated.

Also, it is important that representable terms are expanded _before_ newly
introduced predicate symbols are.

That last stipulation is sadly necessary in order to resolve the following
ambiguity. (This issue is already present with pseudo-terms.) Suppose we’ve
defined
$\mathsf{P}(\mathsf{y})\coloneqq\neg\,\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}$ and $f$ is some representable
function. Then naively $\mathsf{P}(f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}))$ might have two possible expansions:

$\underset{\text{(correct)}}{(\exists!\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y}))\land(\exists\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y})\land\neg\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$})}\quad\text{or}\quad\underset{\text{(incorrect)}}{\neg((\exists!\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y}))\land(\exists\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y})\land\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}))}.$

The left side says that $f(\bm{x})$ outputs something other than ✓. The right
side says that $f(\bm{x})$ doesn’t output ✓. But that might be because
$f(\bm{x})$ doesn’t output anything at all. Some choice had to be made. And
the former struck me as more intuitive and useful. This tripwire is also the
reason I’m avoiding the use of $\neq$ in formulas.

Representable terms expand equivalently in any order.

###### Proof.

Let’s consider the case where we’re dealing with just two competing
representable function symbols:
$\mathsf{P}(f(\bm{\mathsf{r}}),g(\bm{\mathsf{s}}))$ with $\mathsf{P}$ being
some formula and $\bm{\mathsf{r}}$ and $\bm{\mathsf{s}}$ being collections of
regular terms. Then the expansions we need to compare are
$(\exists!\mathsf{y}\colon
f(\bm{\mathsf{r}},\mathsf{y}))\land(\exists\mathsf{y}\colon
f(\bm{\mathsf{r}},\mathsf{y})\land((\exists!\mathsf{z}\colon
g(\bm{\mathsf{s}},\mathsf{z}))\land(\exists\mathsf{z}\colon
g(\bm{\mathsf{s}},\mathsf{z})\land\mathsf{P}(\mathsf{y},\mathsf{z}))))\phantom{.}$
and $(\exists!\mathsf{z}\colon
g(\bm{\mathsf{r}},\mathsf{z}))\land(\exists\mathsf{z}\colon
g(\bm{\mathsf{r}},\mathsf{z})\land((\exists!\mathsf{y}\colon
f(\bm{\mathsf{s}},\mathsf{y}))\land(\exists\mathsf{y}\colon
f(\bm{\mathsf{s}},\mathsf{y})\land\mathsf{P}(\mathsf{y},\mathsf{z})))).$ These
can be checked to be equivalent by going through all four combinations of
setting $\exists!\mathsf{y}\colon f(\bm{\mathsf{r}},\mathsf{y})$ and
$\exists!\mathsf{z}\colon g(\bm{\mathsf{s}},\mathsf{z})$ to true or false. The
general case for an arbitrary number of representable terms can then be
obtained by observing that any permutation can be decomposed into a series of
transpositions. ∎

[Leibniz’s Law For Representable Terms] Let $\mathsf{r}$ and $\mathsf{s}$ be
closed representable terms. And let $\mathsf{P}$ be a formula with one free
variable. Then the following is logically valid:

$\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s}\rightarrow(\mathsf{P}(\mathsf{r})\leftrightarrow\mathsf{P}(\mathsf{s})).$

###### Proof.

By induction on the number of representable function symbols appearing in
$\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s}$.
_Base Case_ : If $\mathsf{r}$ and $\mathsf{s}$ are regular terms, then the
statement is trivial. _Induction_ : So let’s assume that the statement holds
for up to $n$ representable functions and that
$\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s}$
contains $n+1$ representable function symbols. Furthermore, without loss of
generality let’s focus only on the case where $\mathsf{r}$ contains a
representable function symbol, meaning $\mathsf{r}$ is of the form
$\mathsf{r}\emph{\textquotesingle}(f(\bm{\mathsf{t}}))$ for some open
representable term $\mathsf{r}\emph{\textquotesingle}$ and some collection of
closed regular terms $\bm{\mathsf{t}}$. Then the desired statement expands to
$(\exists!\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\bm{\mathsf{t}},\mathsf{y}))\land(\exists\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\bm{\mathsf{t}},\mathsf{y})\land\mathsf{r}\emph{\textquotesingle}(\mathsf{y})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s})\rightarrow(\exists!\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\bm{\mathsf{t}},\mathsf{y}))\land(\exists\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\bm{\mathsf{t}},\mathsf{y})\land(\mathsf{P}(\mathsf{r}\emph{\textquotesingle}(\mathsf{y}))\leftrightarrow\mathsf{P}(\mathsf{s}))).$
This can be simplified into
$\mathsf{r}\emph{\textquotesingle}(\mathtt{y})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s}\rightarrow(\mathsf{P}(\mathsf{r}\emph{\textquotesingle}(\mathtt{y}))\leftrightarrow\mathsf{P}(\mathsf{s}))$
where $\mathtt{y}$ is the unique object such that
$\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\bm{\mathsf{t}},\mathtt{y})$.
At this stage, $\mathsf{r}\emph{\textquotesingle}(\mathtt{y})=\mathsf{s}$ is
closed and contains only $n$ representable function symbols. So we can bring
the inductive hypothesis to bear which concludes the argument.∎

[Rules Of Equality For Representable Terms] Let $\mathsf{r},\mathsf{s}$, and
$\mathsf{t}$ be closed representable terms. Then the following rules of
equality for representable terms are logically valid.

_Symmetry_ :

$\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s}\rightarrow\mathsf{s}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{r}$.

_Transitivity_ :

$\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s}\rightarrow(\mathsf{s}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{t}\rightarrow\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{t})$.

###### Proof.

_Symmetry_ : Here we can expand notation, use ordinary symmetry, and then
contract notation again. _Transitivity_ : By Leibniz’s Law we have
$\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{s}\rightarrow(\mathsf{s}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{t}\leftrightarrow\mathsf{r}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{t})$
which implies the desired statement.∎

Reflexivity is conspicuously absent in the these rules. This could be remedied
by replacing the central “$\land$” in the definition of representable terms
with a “$\rightarrow$”. But that brings its own issues. For example, one can
then no longer use representable terms to introduce existential quantifiers.
Besides, we’re going to be able to introduce equalities using the following
lemma instead.

[Runtime Lemma] Let $f$ be a function which is represented in T. And suppose
$f(\bm{x})=y\neq z$. Then

$\textbf{{T}}\vdash f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\quad\text{and}\quad\textbf{{T}}\vdash\neg\,f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}.$

###### Proof.

After expanding notation and minor simplification $f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ can be turned into
$\exists!\mathsf{y}\colon\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y})\land\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}),$ which is provable in T by the
definition of representable functions. This also allows T to disprove
$f(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ since if it were true, then by
transitivity we’d have $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. And that is false by the axioms of
successorship alone. ∎

###  4.1 Turing Completeness of Q

There are of course many kinds of functions out there which one might want to
represent. But for us there’s one kind in particular which is of primary
concern: the computable functions. A theory which represents all computable
functions has in a quite literal sense achieved Turing completeness. It has a
fully-fledged programming language embedded within it. And a computable
function’s representation is none other than its source code in this language.
This is why I chose the notation ‹$f$›, as it’s reminiscent of how the code
for a Turing machine $M$ is often denoted $\langle M\rangle$. Furthermore, in
order to “execute” a representation ‹$f$› on input $\bm{x}$ one can, for
example, go through all possible strings and check if any of them proves a
theorem of the form $f(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ for some $y$. If so, $y$ is the output.
Naturally, one would hope that this isn’t the most efficient way of running a
representation. But it proves the point.

This allows us to make the central observation of this section: Q (and
consequently PA) represents every computable function. The way I like to think
of this is that the axioms of successorship describe what data is and the
axioms of arithmetic delineate a universal gate set. To check this claim we’re
going to need a Turing complete model of computation. The following one is
particularly convenient.

[Arithmetic Functions] The following functions of type
$\mathbb{N}^{k}\to\mathbb{N}$ are arithmetic functions.

  * •

$\operatorname{\mathit{nil}}(x)=0$

  * •

$\operatorname{\mathit{inc}}(x)=x+1$

  * •

$\operatorname{\mathit{prj}}_{k,i}(x_{1},\dots,x_{k})=x_{i}$

  * •

$\operatorname{\mathit{eq}}(x,y)=\begin{cases}1&\text{if }x=y,\\\
0&\text{otherwise}\end{cases}$

  * •

$\operatorname{\mathit{add}}(x,y)=x+y$

  * •

$\operatorname{\mathit{mul}}(x,y)=x\times y$

Furthermore, if $g,g_{1},\dots,g_{l}$ are arithmetic functions, then the
following are also arithmetic functions.

  * •

$f(\bm{x})=g_{0}(g_{1}(\bm{x}),\dots,g_{l}(\bm{x}))$

  * •

$f(\bm{x})=\operatorname*{arg\,min}_{y}g(\bm{x},y)=0$

This model of computation is almost identical to the general recursive
functions. The only difference is that we’ve replaced recursion with addition
and multiplication. As Gödel pointed out towards the end of his 1931 paper,
this model of computation is in fact able to emulate recursion. That allows it
to inherit computational universality from the general recursive functions.
But it is much easier to represent.

Q represents every computable function.

###### Proof.

We begin by using the Church-Turing Thesis to assert that any computable
function can be constructed using arithmetic functions. This allows us to
proceed by structural induction, stating the representation to be used and
then verifying it in turn. _Base Cases_ : _Nil_ :
$\text{\T1\guilsinglleft$\operatorname{\mathit{nil}}$\T1\guilsinglright}(x,y)\enskip\coloneqq\enskip\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}$
Suppose $\operatorname{\mathit{nil}}(x)=y$. Then $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\raise
0.76207pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 55}$}\raise
0.76207pt\hbox{\footnotesize$\urcorner$}=\mathsf{0}$. Thus, trivially
$\textbf{{Q}}\vdash\exists!\mathsf{y}\colon\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}\land\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$.
_Increment_ :
$\text{\T1\guilsinglleft$\operatorname{\mathit{inc}}$\T1\guilsinglright}(\mathsf{x},\mathsf{y})\enskip\coloneqq\enskip\mathsf{S}\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}$
Suppose $\operatorname{\mathit{inc}}(x)=y$. Then $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. Thus, trivially
$\textbf{{Q}}\vdash\exists!\mathsf{y}\colon\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}\land\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. _Projection_ :
$\text{\T1\guilsinglleft$\operatorname{\mathit{prj}}_{k,i}$\T1\guilsinglright}(\mathsf{x}_{1},\dots,\mathsf{x}_{k},\mathsf{y})\enskip\coloneqq\enskip\mathsf{x}_{i}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}$
Suppose $\operatorname{\mathit{prj}}_{k,i}(\bm{x})=y$. Then $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x_{i}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. Thus, trivially
$\textbf{{Q}}\vdash\exists!\mathsf{y}\colon\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x_{i}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}\land\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x_{i}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x_{i}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. _Equality_ :
$\text{\T1\guilsinglleft$\operatorname{\mathit{eq}}$\T1\guilsinglright}(\mathsf{x},\mathsf{y},\mathsf{z})\enskip\coloneqq\enskip(\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}\land\mathsf{z}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{0})\lor(\neg\,\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}\land\mathsf{z}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0})$
Suppose $\operatorname{\mathit{eq}}(x,y)=z$. Then we have two cases. _$\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ and $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{S}\mathsf{0}$_: Here the sought
claim reduces to the once again trivial
$\textbf{{Q}}\vdash\exists!\mathsf{z}\colon\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\land\mathsf{z}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{0}\land\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\land\mathsf{S}\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{0}.$
_$\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\neq\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ and $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{0}$_: Here the sought claim
reduces to the once again trivial
$\textbf{{Q}}\vdash\exists!\mathsf{z}\colon\neg\,\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\land\mathsf{z}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}\land\neg\,\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\land\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}.$
_Addition_ :
$\text{\T1\guilsinglleft$\operatorname{\mathit{add}}$\T1\guilsinglright}(\mathsf{x},\mathsf{y},\mathsf{z})\enskip\coloneqq\enskip\mathsf{x}+\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{z}$
We first show by induction on $y$ that $\textbf{{Q}}\vdash\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$ for any $x,y\in\mathbb{N}$. _Base
Case_ : $\textbf{{Q}}\vdash\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ follows immediately from A0. _Induction_
: Let $y=z+1$ so that $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. Then $\textbf{{Q}}\vdash\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+z$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$ by A1, followed by the inductive
hypothesis, and finally simple equality. Suppose
$\operatorname{\mathit{add}}(x,y)=z$. Then $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$. Thus, after substituting $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$, we trivially get
$\textbf{{Q}}\vdash\exists!\mathsf{z}\colon\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{z}\land\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}.$ _Multiplication_ :
$\text{\T1\guilsinglleft$\operatorname{\mathit{mul}}$\T1\guilsinglright}(\mathsf{x},\mathsf{y},\mathsf{z})\enskip\coloneqq\enskip\mathsf{x}\times\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{z}$
Similar to addition, we first show by induction on $y$ that
$\textbf{{Q}}\vdash\mathsf{\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\times\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x\times y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}}$ for any $x,y\in\mathbb{N}$. _Base
Case_ : $\textbf{{Q}}\vdash\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\times\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$
follows immediately from M0. _Induction_ : Let $y=z+1$ so that $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\mathsf{S}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$. Then $\textbf{{Q}}\vdash\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\times\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\times\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x\times z$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+x\times z$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x\times y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$ by M1, followed by the inductive
hypothesis, the previously established fact that $\textbf{{Q}}\vdash\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}+\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x+y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$, and finally simple equality.
Suppose $\operatorname{\mathit{mul}}(x,y)=z$. Then $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$z$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x\times y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$. Thus, after substituting $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\times\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x\times y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}$, we trivially get
$\textbf{{Q}}\vdash\exists!\mathsf{z}\colon\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\times\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{z}\land\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\times\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}=\raise
0.29541pt\hbox{\footnotesize$\ulcorner$}\hbox{$x\times y$}\raise
0.29541pt\hbox{\footnotesize$\urcorner$}.$ _Inductions_ : _Composition_ : Here
we use the inductive hypothesis to assume that $g_{0},\dots,g_{l}$ are already
represented which allows us to represent $f$ as follows.
$\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\bm{\mathsf{x}},\mathsf{y})\enskip\coloneqq\enskip
g_{0}(g_{1}(\bm{\mathsf{x}}),\dots,g_{l}(\bm{\mathsf{x}}))\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}$
Suppose $f(\bm{x})=y$. Then for some $y_{1},\dots,y_{l}$ we must have
$g_{1}(\bm{x})=y_{1},\quad\dots,\quad g_{l}(\bm{x})=y_{l},\quad\text{and}\quad
g_{0}(y_{1},\dots,y_{l})=y.$ So by the Runtime Lemma $\textbf{{Q}}\vdash
g_{1}(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y_{1}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\quad\dots,\quad\textbf{{Q}}\vdash
g_{l}(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y_{l}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\quad\text{and}\quad\textbf{{Q}}\vdash
g_{0}(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y_{1}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\dots,\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y_{l}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}.$ Thus, we can take the trivial
$\textbf{{Q}}\vdash\mathsf{\exists!y\colon\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}y\land\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}}$ and repeatedly replace representable
terms using Leibniz’s Law until we arrive at
$\textbf{{Q}}\vdash\exists!\mathsf{y}\colon g_{0}(g_{1}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}),\dots,g_{l}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}))\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}y\land
g_{0}(g_{1}(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}),\dots,g_{l}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}))\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}.$ _Minimization_ : Again, by the
inductive hypothesis $g$ is already represented, permitting this
representation of $f$:
$\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\bm{\mathsf{x}},\mathsf{y})\enskip\coloneqq\enskip
g(\bm{\mathsf{x}},\mathsf{y})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}\land\forall\mathsf{z}<\mathsf{y}\colon\neg
g(\bm{\mathsf{x}},\mathsf{z})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$
Suppose $f(\bm{x})=y$. Then $g(\bm{x},y)=0$ and $g(\bm{x},z)\neq 0$ for all
$z<y$. _$\textbf{{Q}}\vdash\text{$f$}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})$_ : The first conjunct $g(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$
easily follows by the Runtime Lemma. And using the Bounded Quantification
Lemma we can turn the second conjunct into a finite number of cases which can
then be treated similarly. (If $y=0$, non-negativity can be used instead.)
_$\textbf{{Q}}\vdash\exists!\mathsf{y}\colon\text{$f$}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{y})$_ : Existence has already
been handled. And for uniqueness let $\mathtt{y}$ be an arbitrary object such
that $g(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathtt{y})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}\land\forall\mathsf{z}<\mathtt{y}\colon\neg
g(\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\mathsf{z})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{0}$.
Then together with $\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})$ we can easily rule out
$\mathtt{y}<\raise 0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$ and $\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}<\mathtt{y}$ which by the totality of
ordering leaves only $\mathtt{y}=\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}$.∎

##  5 Diagonalization

With the technical groundwork laid, we can now proceed to the main event. As
already pointed out, the representation of a computable function is simply its
source code in formal language. Moreover, it is a standard trick in computer
science to achieve diagonalization by running a program on itself. So then,
let’s run a program on its own representation and see what happens.

Writing $A(\text{\T1\guilsinglleft$f$\T1\guilsinglright})$ in the signature of
an algorithm $A$ means that $A$ expects a representation as input, akin to
pattern matching. For invalid inputs (which we’ll avoid) the algorithm is
allowed to arbitrarily misbehave.

[Diagonal Lemma] Let T be a theory which represents every computable function.
And let $\mathsf{P}$ be a formula with one free variable. Then there exists a
sentence $\mathsf{A}$ referred to as a “fixed point” such that
$\textbf{{T}}\vdash\mathsf{A}\leftrightarrow\mathsf{P}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$.

###### Proof.

Consider the following algorithm.
$D(\text{\T1\guilsinglleft$f$\T1\guilsinglright})$ return $\mathsf{P}(f(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$f$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$}))$ Then $\textbf{{T}}\vdash D(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$D$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{P}(D(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$D$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$}))\\!$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}$ by the Runtime Lemma and hence
$\textbf{{T}}\vdash\mathsf{P}(D(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$D$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$}))\leftrightarrow\mathsf{P}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{P}(D(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$D$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$}))\\!$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})$ by Leibniz’s Law, giving fixed
point $\mathsf{P}(D(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$D$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$}))$. ∎

The main use of the Diagonal Lemma is to produce the Gödel sentence. Consider
the following predicate. [$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$] Let T
be a computably enumerable theory which represents every computable function.
And let $\operatorname{\mathit{pv}}$ be a proof verifier for T. Then

$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\mathsf{x})\enskip\coloneqq\enskip\exists\mathsf{p}\colon\operatorname{\mathit{pv}}(\mathsf{p},\mathsf{x})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}.$

If one applies the Diagonal Lemma to
$\neg\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$, one produces a sentence
$\mathsf{G}$ such that PA proves
$\mathsf{G}\leftrightarrow\neg\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{G}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$. Informally this sentence states: “I
am not provable.” which, assuming that PA is consistent, turns out to be true.
Furthermore, one can also show that $\neg\mathsf{G}$ can’t be provable either.
Though this needs the stronger assumption that PA is _correct_ (also referred
to as _sound_); if PA proves something, then it is actually so. Or to be
pedantic it at least requires $\omega$-consistency; if PA proves that some
unbounded search terminates, then it actually does. So in summary, if PA is
$\omega$-consistent, it is incomplete.

For the audience in 1931 this already settled the matter. Still, in 1936 John
B. Rosser found a way to iron out the last wrinkle as well by using this
predicate instead [9]: [Concatenation]
$\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}$ is the computable
function which concatenates two numbers. I.e., it returns the number which is
written using the digits of the first number followed by the digits of the
second number. Furthermore, we’ll use left-associative infix notation for this
function, so
$x\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}y\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}z\coloneqq(x\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}y)\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}z$.
The fact that this function is associative won’t be needed.

[$\operatorname{\textsf{{Pvb}}}_{\mathsf{R}}$] Let T be a computably
enumerable extension of Q. And let $\operatorname{\mathit{pv}}$ be a proof
verifier for T. Then

$\operatorname{\textsf{{Pvb}}}_{\mathsf{R}}(\mathsf{x})\enskip\coloneqq\enskip\exists\mathsf{p}\colon\operatorname{\mathit{pv}}(\mathsf{p},\mathsf{x})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}\land\forall\mathsf{q}\leq\mathsf{p}\colon\neg\,\operatorname{\mathit{pv}}(\mathsf{q},\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{x})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}.$

If one applies the Diagonal Lemma to
$\neg\operatorname{\textsf{{Pvb}}}_{\mathsf{R}}$, it produces the Rosser
sentence $\mathsf{R}$ which can be paraphrased as: “For every proof of me
there exists a shorter disproof.” This sentence, unlike $\mathsf{G}$, can be
demonstrated to be neither provable nor disprovable assuming only the
consistency of PA, giving us the much nicer formulation: if PA is consistent,
it is incomplete.

Rosser’s argument comes with the minor drawback that just to have $\leq$
available one already has to narrow the discussion from theories which
represent every computable function to just extensions of Q. And one also
still has spell out a few more details. For starters, one has to invoke the
Bounded Quantification Lemma. This brings us then to another way of proving
the First Incompleteness Theorem which in my mind fully captures the essence
with beautiful concision. [First Incompleteness Theorem] Let T be a consistent
and computably enumerable theory which represents every computable function.
Then T is incomplete.

###### Proof.

First, we construct the following algorithm.
$X(\text{\T1\guilsinglleft$f$\T1\guilsinglright})$ for $p\in\mathbb{N}$ if $p$
proves $\neg\,f(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$f$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}$ return ✓ if $p$ proves
$\hphantom{\neg\,}f(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$f$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}$ return ✗ This lets us produce
$\mathsf{R}\enskip\coloneqq\enskip\neg\,X(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$X$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.69225pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\small\char 51}$}\raise
0.69225pt\hbox{\footnotesize$\urcorner$}.$ Now suppose that $\mathsf{R}$ was
decidable. Then there must exist a _first_ $p\in\mathbb{N}$ which decides
$\mathsf{R}$. This leads to two cases.
_$p$ proves $\mathsf{R}$_: Then
$X(\text{\T1\guilsinglleft$X$\T1\guilsinglright})$ returns ✓ upon finding $p$
and so $\textbf{{T}}\vdash\neg\mathsf{R}$ by the Runtime Lemma; an
inconsistency. _$p$ proves $\neg\mathsf{R}$_: Then
$X(\text{\T1\guilsinglleft$X$\T1\guilsinglright})$ returns ✗ upon finding $p$
and so $\textbf{{T}}\vdash\mathsf{R}$ by the Runtime Lemma; an inconsistency.∎

The sentence $\mathsf{R}$ used in the above proof carries its name for a
reason. It’s because, as some reflection will reveal, $\mathsf{R}$ is in fact
a Rosser sentence, claiming: “For every proof of me there exists a shorter
disproof.” Furthermore, in order to recover the original “I am not provable”
one only needs to drop the last two lines of $X$.

##  6 Re-Representation

At a high level the Second Incompleteness Theorem isn’t all that hard to
grasp. We’ve already seen that if PA is consistent, then $\mathsf{G}$ isn’t
provable and thereby true. In short,
$\operatorname{\textsf{{Con}}}\rightarrow\mathsf{G}$ where
$\operatorname{\textsf{{Con}}}$ expresses the consistency of PA. What’s more,
as Gödel first noted in 1931, this fact can be proved in PA as well since it
can step through the proof of the First Incompleteness Theorem just the same.
To coin a phrase, PA represents that it represents—or _re-represents_ —its own
proof verifier. But that means that if PA could prove
$\operatorname{\textsf{{Con}}}$, then PA could also prove $\mathsf{G}$ by
modus ponens which is impossible. That’s the Second Incompleteness Theorem: if
PA is consistent, then it can’t prove this to be so.

Alas, the crucial fact that
$\operatorname{\textsf{{Con}}}\rightarrow\mathsf{G}$ can be proved in PA is
notoriously difficult to establish rigorously. Gödel himself famously
concluded his 1931 paper stating: “The results will be stated and proved in
fuller generality in a forthcoming sequel. There too, the mere outline proof
we have given of [the Second Incompleteness Theorem] will be presented in
detail.” Such a sequel never came. Instead, the first rigorous demonstration
appeared in 1939 in the second volume of Foundations of Mathematics [1]
written by David Hilbert and his assistant Paul Bernays—Bernays being the main
author.

But besides technical issues, there are also conceptual ones. First and
foremost, what exact expression should we choose for
$\operatorname{\textsf{{Con}}}$? Gödel had the obvious in mind:
[$\operatorname{\textsf{{Con}}}_{\mathsf{G}}$]
$\operatorname{\textsf{{Con}}}_{\mathsf{G}}\enskip\coloneqq\enskip\neg\exists\mathsf{x}\colon\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\mathsf{x})\land\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{x})$
However, Gödel had many freedoms when making his construction. What made the
choice he arrived at the right one? This question is brought to a head when
one examines the alternative derived from Rosser’s predicate.
[$\operatorname{\textsf{{Con}}}_{\mathsf{R}}$]
$\operatorname{\textsf{{Con}}}_{\mathsf{R}}\enskip\coloneqq\enskip\neg\exists\mathsf{x}\colon\operatorname{\textsf{{Pvb}}}_{\mathsf{R}}(\mathsf{x})\land\operatorname{\textsf{{Pvb}}}_{\mathsf{R}}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{x})$
If one were to use this consistency statement instead, then PA actually
_could_ prove its own consistency. This happens for the simple reason that
_every_ theory, whether consistent or not, is “consistent” according to the
Rosser definition. To address this conundrum Hilbert and Bernays decided to
put down three conditions which after some modification by Martin Löb became
these:

[Derivability Conditions] A predicate $\operatorname{\textsf{{Pvb}}}$ obeys
the _derivability conditions_ for a theory T if the following holds for any
sentences $\mathsf{A},\mathsf{B}$:

_Representability_ :

If $\textbf{{T}}\vdash\mathsf{A}$, then
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$.

_Distributivity_ :

$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$})\rightarrow(\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{B}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}))$.

_Re-Representability_ :

$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\operatorname{\textsf{{Pvb}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})$.

From these three conditions—also known as the HBL-derivability conditions
(Hilbert, Bernays, Löb)—the Second Incompleteness Theorem can be derived in
short order. This both shuts the door on Rosser’s predicate and provides a
helpful layer of abstraction, similar to the representability of computable
functions.

The only question left on the table is then: does some proposed provability
predicate such as $\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$ actually meet
the criteria? This is where all the fearsome details end up hiding; details
which crucially rely upon the exact representation of the proof verifier
$\operatorname{\mathit{pv}}$ underlying
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$, lest any Rosserian shenenigans
take place under the hood. The standard approach runs roughly as follows.

_Representability_ :

This part carries over from studying the First Incompleteness Theorem and is
basically free.

_Distributivity_ :

Here one can show that PA recognizes the modus ponens inference rule in
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$. That is to say, PA can prove a
concatenation of a proof of $\mathsf{A}\rightarrow\mathsf{B}$, a proof of
$\mathsf{A}$, and the list containing only $\mathsf{B}$ to be a proof of
$\mathsf{B}$. Doing so requires some cursory inspection of
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$ as well as wading through a fair
number of details involving elementary features of lists. But it’s still
manageable.

_Re-Representability_ :

This is the true villain of the story. In outline the strategy is to show that

$\textbf{{PA}}\vdash\mathsf{A}\rightarrow\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$

for any sentence $\mathsf{A}$ built without unbounded universal quantifiers.
Re-representability is then obtained as a special case. But checking the above
demands an exceedingly elaborate structural induction on the construction of
$\mathsf{A}$, during each stage of which one has to x-ray
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$. And if that wasn’t enough,
realize that as soon as one moves on from PA to any of its extensions one is
presented with a new provability predicate for that theory and one has to
start all over again.

The challenge ahead of us is daunting. So instead of charging straight ahead
let’s pause for a moment and try to figure out what is fundamentally causing
the difficulty. It’s that, whereas the modus ponens inference rule is usually
coded into $\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$ at a high level, re-
representability emerges piece by piece from the entirety of the construction.
But picking $\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$ as our provability
predicate was a deliberate choice; a choice which we can amend. If only we
could find a provability predicate which carried the re-representability
property at the surface, then we might save ourselves a lot of grief during
the verification.

Indeed, why not simply pick the following provability predicate and declare
victory?

$\operatorname{\textsf{{Pvb}}}_{\top}(\mathsf{x})\enskip\coloneqq\enskip\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{x}$

This predicate trivially satisfies all three conditions. Yet something is
clearly amiss here. According to $\operatorname{\textsf{{Pvb}}}_{\top}$
everything is provable. In other words, $\operatorname{\textsf{{Pvb}}}_{\top}$
encodes the belief that our theory is inconsistent. Yes, the Second
Incompleteness Theorem still applies to this predicate. But it has degenerated
into the trite observation that a consistent theory which believes itself to
be inconsistent can’t simultaneously assert its own consistency. Evidently
we’re still missing a basic requirement.

[Provability Predicate] A predicate $\operatorname{\textsf{{Pvb}}}$ is
considered a _provability predicate_ for a theory T if it obeys the following
condition for any sentence $\mathsf{A}$.

_Correctness_ :

$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ is true (in the intended
interpretation) if and only if $\textbf{{T}}\vdash\mathsf{A}$.

I’ve seen others make the alternative mandate that if
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$, then
$\textbf{{T}}\vdash\mathsf{A}$. But this ends up roping in the assertion that
T is a correct theory and would conflict with our aim to rest the Second
Incompleteness Theorem on consistency alone.

[Weak Provability Predicate] A predicate $\operatorname{\textsf{{Pvb}}}$ is
considered a _weak_ or _representable provability predicate_ for a theory T if
it is a provability predicate for T which also obeys the following condition
for any sentence $\mathsf{A}$.

_Representability_ :

If $\textbf{{T}}\vdash\mathsf{A}$, then
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$.

[Strong Provability Predicate] A predicate $\operatorname{\textsf{{Pvb}}}$ is
considered a _strong provability predicate_ for a theory T if it is a
provability predicate for T which also obeys the derivability conditions. To
repeat, for any sentences $\mathsf{A},\mathsf{B}$:

_Representability_ :

If $\textbf{{T}}\vdash\mathsf{A}$, then
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$.

_Distributivity_ :

$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$})\rightarrow(\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{B}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}))$.

_Re-Representability_ :

$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\operatorname{\textsf{{Pvb}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})$.

Assembling a predicate with the correctness property all the way from scratch
would take a while. So let me set up an intermediate abstraction to build on
top of.

[Correctly Representable Function] A function $f$ is considered to be
correctly represented in a theory T if it is represented in T by a formula
‹$f$› and $\text{\T1\guilsinglleft$f$\T1\guilsinglright}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\bm{x}$}\raise
0.0pt\hbox{\footnotesize$\urcorner$},\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$y$}\raise
0.0pt\hbox{\footnotesize$\urcorner$})$ is true if and only if $f(\bm{x})=y$.
The following should then come with little surprise. Q correctly represents
every computable function.

###### Proof Sketch.

All that’s required for this result is to retrace the argument by which Q
represents every computable function and check that correctness is satisfied
at each step. ∎

It’s worth bearing in mind that the ability of a theory T to correctly
represent a function by no means implies that T is a correct theory. For
instance, since Q correctly represents every computable function so does every
extension of it, including the inconsistent ones.

We can then immediately check off the first two boxes by noting that
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$ (and
$\operatorname{\textsf{{Pvb}}}_{\mathsf{R}}$ provided our theory is
consistent) is a weak provability predicate as long as it has been constructed
with a correct representation of $\operatorname{\mathit{pv}}$. But now for the
heart of the matter: can we find a _strong_ provability predicate which is
also easily recognized as such? Actually, we can, starting with the following
idea.

Take a closer look at this example consequent of the re-representability
condition: $\operatorname{\textsf{{Pvb}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{S}\mathsf{0}+\mathsf{S}\mathsf{0}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{S}\mathsf{0}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})$. Antropomorphizing our provability
predicate lets us rephrase this in English as: “I believe that I believe that
$1+1=2$.” Now answer me this: if I ever asked you if you believed this
statement yourself, would you then dutifully proceed to simulate your own
brain as it is pondering whether $1+1=2$? I doubt it. More likely you’d just
ponder the question directly. But then why not permit
$\operatorname{\textsf{{Pvb}}}$ the same liberty? Or more generally, why
couldn’t $\mathsf{A}$ be used to derive $\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ straight away? In customary notation
we’ll then have these two inference rules built into our provability
predicate:

$\text{Modus Ponens:}\quad\frac{\mathsf{A}\rightarrow\mathsf{B}\hskip
16.0pt\mathsf{A}}{\mathsf{B}}\hskip
85.35826pt\text{Representability:}\quad\frac{\mathsf{A}}{\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})}$

We’re going to have to meet the representability condition—if $\mathsf{A}$ is
a theorem, so is $\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$—anyway. So this is a completely
sound inference to make. The only puzzle this leaves us with is to find a way
for $\operatorname{\textsf{{Pvb}}}$ to recognize itself. But at this point
that’s a well-practiced routine. The solution, as always, is to run a program
on its own source code.

[Totality Of Ordering]

$\textbf{{PA}}\vdash\forall\mathsf{x},\mathsf{y}\colon\mathsf{x}<\mathsf{y}\lor\mathsf{y}<\mathsf{x}\lor\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y}.$

###### Proof Sketch.

Repeat the proof for the totality of ordering w.r.t. numerals while carrying
out the induction within PA. ∎

[List] A _list_ is a single number which contains a finite ordered set of
other numbers via some coding. Furthermore, we’ll write $[x_{1},\dots,x_{k}]$
to denote the list whose items are $x_{1},\dots,x_{k}$. Strictly speaking,
this is an infinite set of computable functions, one for each number of
inputs. So there are $[\cdot],[\cdot,\cdot]$, $[\cdot,\cdot,\cdot]$, etc.

[List Access] Further extending our use of computer programming notation we’ll
use $\cdot[\cdot]$ to denote the computable function which given a list
$[\bm{x}]$ and index $i$ retrieves the corresponding item, namely $x_{i}$. In
short: $[\bm{x}][i]=x_{i}$.

[List Length] $\lVert\cdot\rVert$ denotes the computable function which
determines the length of a list.

[List Concatenation]
$\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}$
denotes the computable function which concatenates two lists. And analogously
to basic concatenation we’ll use left-associative infix notation for this
function.

[Basic Properties Of Lists] For some correct representations of
$\cdot[\cdot]$, $\lVert\cdot\rVert$, and
$\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}$
we have:
$\displaystyle\textbf{{PA}}\vdash\forall\mathsf{x},\mathsf{i}\colon\exists\mathsf{y}\colon\mathsf{x}[\mathsf{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{y},$
(L0)
$\displaystyle\textbf{{PA}}\vdash\forall\mathsf{x}\colon\exists\mathsf{n}\colon\lVert\mathsf{x}\rVert=\mathsf{n},$
(L1)
$\displaystyle\textbf{{PA}}\vdash\forall\mathsf{x},\mathsf{y}\colon\exists\mathsf{z}\colon\mathsf{x}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\mathsf{y}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{z},$
(L2)
$\displaystyle\textbf{{PA}}\vdash\forall\mathsf{x},\mathsf{y}\colon\forall\mathsf{i}<\lVert\mathsf{x}\rVert\colon\mathsf{x}[\mathsf{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}(\mathsf{x}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\mathsf{y})[\mathsf{i}],$
(L3)
$\displaystyle\textbf{{PA}}\vdash\forall\mathsf{x},\mathsf{y}\colon\forall\mathsf{i}<\lVert\mathsf{y}\rVert\colon\mathsf{y}[\mathsf{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}(\mathsf{x}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\mathsf{y})[\lVert\mathsf{x}\rVert+\mathsf{i}],$
(L4)
$\displaystyle\textbf{{PA}}\vdash\forall\mathsf{x},\mathsf{y}\colon\lVert\mathsf{x}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\mathsf{y}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\lVert\mathsf{x}\rVert+\lVert\mathsf{y}\rVert.$
(L5)

###### Proof.

Omitted. ∎

The preceding lemma is already baked into the definition of concatenation in
Gödel’s original construction. Or at least the right half of it is. Perhaps
that’s also the reason why Hilbert and Bernays left out further details when
they listed the right half on page 321 of their second volume. Also, L0 is
never used. I only added it to complete the set.

[Existence Theorem For Strong Provability Predicates] Let T be a computably
enumerable extension of PA. Then there exists a strong provability predicate
for T.

###### Proof.

We start with an arbitrary predicate which we know to be a weak provability
predicate. $\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$ will do nicely. We can
then bolt on the distributivity and re-representability properties by first
constructing the following algorithm.
$Q(\text{\T1\guilsinglleft$f$\T1\guilsinglright},x)$ return $\begin{aligned}
\exists\mathsf{p},\mathsf{m}\colon&\mathsf{p}[\mathsf{m}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$x$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\,\land\\\
&\lVert\mathsf{p}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{m}\,\land\\\
&\forall\mathsf{i}<\lVert\mathsf{p}\rVert\colon\begin{aligned}
&\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}(\mathsf{p}[\mathsf{i}])\,\lor\\\
&\exists\mathsf{j},\mathsf{k}<\mathsf{i}\colon\begin{aligned}
&\mathsf{p}[\mathsf{j}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{p}[\mathsf{k}]\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{p}[\mathsf{i}]\,\lor\\\
&\mathsf{p}[\mathsf{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}f(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$f$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\mathsf{p}[\mathsf{j}])\end{aligned}\end{aligned}\end{aligned}$
And then we have the accompanying provability predicate:
$\operatorname{\textsf{{Pvb}}}(\mathsf{x})\enskip\coloneqq\enskip\begin{aligned}
\exists\mathsf{p},\mathsf{m}\colon&\mathsf{p}[\mathsf{m}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{x}\,\land\\\
&\lVert\mathsf{p}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathsf{m}\,\land\\\
&\forall\mathsf{i}<\lVert\mathsf{p}\rVert\colon\begin{aligned}
&\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}(\mathsf{p}[\mathsf{i}])\,\lor\\\
&\exists\mathsf{j},\mathsf{k}<\mathsf{i}\colon\begin{aligned}
&\mathsf{p}[\mathsf{j}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{p}[\mathsf{k}]\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{p}[\mathsf{i}]\,\lor\\\
&\mathsf{p}[\mathsf{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}Q(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$Q$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\mathsf{p}[\mathsf{j}])\end{aligned}\end{aligned}\end{aligned}$
Onwards to the verfication. In what follows we’ll be using Leibniz’s Law for
representable terms, the Runtime Lemma, and the various properties of lists
all over the place. I’ve omitted references for brevity. Additionally, we’ll
postpone correctness to the end. _Representability_ : If
$\textbf{{T}}\vdash\mathsf{A}$, then $[\mathsf{A}]$ by itself already
constitutes a “proof” and we’re naturally led to the claim $\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{A}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}[\mathsf{0}]=\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}\land\lVert\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{[A]}$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}\rVert=\mathsf{S}\mathsf{0}\land\forall\mathsf{i}<\lVert\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{A}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}\rVert\colon\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{A}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}[\mathsf{i}])$ which can be seen to be
provable through the Bounded Quantification Lemma and the representability
property of $\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}$. The
desired conclusion $\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ follows without effort.
_Distributivity_ : For this case we need to establish that T can argue from
the assumptions $\operatorname{\textsf{{Pvb}}}(\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$})$ and
$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ to the conclusion
$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{B}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$. More concretely, we’ll want to show
that if we instantiate the two existentials
$\operatorname{\textsf{{Pvb}}}(\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$})$ and
$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ with
$\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}$ and $\mathtt{p}_{\mathsf{A}}$ respectively,
then we can obtain
$\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}},\mathtt{p}_{\mathsf{B}}$, and
$\mathtt{m}_{\mathsf{B}}$ such that
$\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\mathtt{p}_{\mathsf{A}},\quad\mathtt{p}_{\mathsf{B}}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{B}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$},\quad\text{and}\quad\mathtt{m}_{\mathsf{B}}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\lVert\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\rVert$
and that $\mathtt{p}_{\mathsf{B}},\mathtt{m}_{\mathsf{B}}$ will then be able
to serve as witnesses for $\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{B}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$. To that end we can immediately get
the assertion that $\ulcorner$$\mathsf{B}$$\urcorner$ is the last item of
$\mathtt{p}_{\mathsf{B}}$ out of the way by observing that
$\mathtt{p}_{\mathsf{B}}[\mathtt{m}_{\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}(\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{B}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})[\lVert\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\rVert+\mathsf{0}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{B}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}[\mathsf{0}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{B}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}\qquad\text{and}\qquad\lVert\mathtt{p}_{\mathsf{B}}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\lVert\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\rVert+\lVert\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{B}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{m}_{\mathsf{B}}.$
What’s left then is to verify that every item of $\mathtt{p}_{\mathsf{B}}$ is
valid, i.e.:
$\forall\mathsf{i}<\lVert\mathtt{p}_{\mathsf{B}}\rVert\colon\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}(\mathtt{p}_{\mathsf{B}}[\mathsf{i}])\;\lor\;\exists\mathsf{j},\mathsf{k}<\mathsf{i}\colon\;\mathtt{p}_{\mathsf{B}}[\mathsf{j}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{B}}[\mathsf{k}]\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathtt{p}_{\mathsf{B}}[\mathsf{i}]\;\lor\;\mathtt{p}_{\mathsf{B}}[\mathsf{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}Q(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$Q$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\mathtt{p}_{\mathsf{B}}[\mathsf{j}]).$
This can be established for an arbitrary $\mathtt{i}$ such that
$\mathtt{i}<\lVert\mathtt{p}_{\mathsf{B}}\rVert$ by using the totality of
ordering to break the argument down into three cases. _$\mathtt{i}
<\lVert\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm
0mm 0mm}{$\rightarrow$}}}\mathsf{B}}\rVert$_: Here we can carry out the
following conversion: $\begin{aligned}
&\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}(\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm 0mm}{$\rightarrow$}}}\mathsf{B}}[\mathtt{i}])\,\lor\\\
&\exists\mathsf{j},\mathsf{k}<\mathtt{i}\colon\begin{aligned}
&\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathsf{j}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathsf{k}]\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm 0mm}{$\rightarrow$}}}\mathsf{B}}[\mathtt{i}]\,\lor\\\
&\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathtt{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}Q(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$Q$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathsf{j}])\end{aligned}\end{aligned}\qquad\leftrightarrow\qquad\begin{aligned}
&\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}(\mathtt{p}_{\mathsf{B}}[\mathtt{i}])\,\lor\\\
&\exists\mathsf{j},\mathsf{k}<\mathtt{i}\colon\begin{aligned}
&\mathtt{p}_{\mathsf{B}}[\mathsf{j}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{B}}[\mathsf{k}]\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathtt{p}_{\mathsf{B}}[\mathtt{i}]\,\lor\\\
&\mathtt{p}_{\mathsf{B}}[\mathtt{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}Q(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$Q$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\mathtt{p}_{\mathsf{B}}[\mathsf{j}])\end{aligned}\end{aligned}$
Of course having obtained the left-hand side from
$\operatorname{\textsf{{Pvb}}}(\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$})$. Let’s consider an example to
illustrate; the substitution of
$\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathsf{k}]$ on the left with
$\mathtt{p}_{\mathsf{B}}[\mathsf{k}]$ on the right. Suppose we had
instantiated $\mathsf{k}$ on the left with
$\mathtt{k}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}$. Then since
$\mathtt{k}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}<\mathtt{i}<\lVert\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}\rVert<\lVert\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\rVert$
we can deduce
$\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathtt{k}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}(\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\mathtt{p}_{\mathsf{A}})[\mathtt{k}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}[\mathtt{k}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}(\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\mathsf{B}]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})[\mathtt{k}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{B}}[\mathtt{k}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm 0mm}{$\rightarrow$}}}\mathsf{B}}].$ This permits the substitution
we’ve aimed for. We then simply repeat this process for all the other
representable terms and finally reintroduce existential quantifiers to arrive
at the right-hand side.
_$\lVert\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm
0mm 0mm}{$\rightarrow$}}}\mathsf{B}}\rVert\leq\mathtt{i}
<\lVert\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\rVert$_: Here we
evidently have
$\mathtt{i}=\lVert\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm 0mm}{$\rightarrow$}}}\mathsf{B}}\rVert+\mathtt{i}_{\mathsf{A}}$ for
some $\mathtt{i}_{\mathsf{A}}<\lVert\mathtt{p}_{\mathsf{A}}\rVert$ which
allows us to proceed the same way we did in the previous case, this time
lifting over the items of $\mathtt{p}_{\mathsf{A}}$.
_$\mathtt{i}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\lVert\mathtt{p}_{\mathsf{B}\emph{\textquotesingle}}\rVert$_
: Finally, for the last item we can use $\operatorname{\textsf{{Pvb}}}(\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$})$ and
$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ to obtain
$\mathtt{m}_{\mathsf{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm 0mm}{$\rightarrow$}}}\mathsf{B}}}$ and $\mathtt{m}_{\mathsf{A}}$ such
that $\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm
0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathtt{m}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$},\quad\lVert\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{m}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}},\quad\mathtt{p}_{\mathsf{A}}[\mathtt{m}_{\mathsf{A}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$},\quad\text{and}\quad\lVert\mathtt{p}_{\mathsf{A}}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{m}_{\mathsf{A}}.$
Thus, after obtaining $\mathtt{m}_{\mathsf{B}\emph{\textquotesingle}}$ such
that
$\mathtt{m}_{\mathsf{B}\emph{\textquotesingle}}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\lVert\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm 0mm}{$\rightarrow$}}}\mathsf{B}}\rVert+\mathtt{m}_{\mathsf{A}}$ we can
gather together
$\mathtt{p}_{\mathsf{B}}[\mathtt{m}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}[\mathtt{m}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$},\quad\mathtt{p}_{\mathsf{B}}[\mathtt{m}_{\mathsf{B}\emph{\textquotesingle}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{A}}[\mathtt{m}_{\mathsf{A}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$},\quad\text{and}\quad\mathtt{p}_{\mathsf{B}}[\mathtt{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{B}}[\mathtt{m}_{\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{B}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}.$ And so in all we get
$\mathtt{p}_{\mathsf{B}}[\mathtt{m}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm
0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\rightarrow\mathsf{B}$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{B}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{B}}[\mathtt{m}_{\mathsf{B}\emph{\textquotesingle}}]\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathtt{p}_{\mathsf{B}}[\mathtt{i}].$
Thus, noting
$\mathtt{m}_{\mathsf{A}\mathrel{\scalebox{0.8}[0.8]{\clipbox{1.75mm 0mm 0mm
0mm}{$\rightarrow$}}}\mathsf{B}}<\mathtt{m}_{\mathsf{B}\emph{\textquotesingle}}<\mathtt{i}$,
we find
$\exists\mathsf{j},\mathsf{k}<\mathtt{i}\colon\mathsf{p}_{\mathsf{B}}[\mathsf{j}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{p}_{\mathsf{B}}[\mathsf{k}]\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\raise
1.60652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\rightarrow$}\raise
1.60652pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{p}_{\mathsf{B}}[\mathtt{i}]$
which satisfies the consequent. _Re-Representability_ : Here we need to guide
T from the assumption $\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ to the conclusion
$\operatorname{\textsf{{Pvb}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})$. With our new inference rule in
place this is now as simple as observing that
$\mathtt{p}_{\mathtt{p}_{\mathsf{A}}}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{A}}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$[\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$},$ where $\mathtt{p}_{\mathsf{A}}$ has
been obtained from $\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$, serves as the desired proof. The
verification proceeds along exactly the same lines as it did for the
distributive property, so we’ll skip most of it. The only novelty occurs when
checking the final item at index
$\mathtt{i}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\lVert\mathtt{p}_{\mathsf{A}}\rVert$.
Here the assumption provides an $\mathtt{m}_{\mathsf{A}}$ such that
$\mathtt{p}_{\mathsf{A}}[\mathtt{m}_{\mathsf{A}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}\quad\text{and}\quad\lVert\mathtt{p}_{\mathsf{A}}\rVert\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathsf{S}\mathtt{m}_{\mathsf{A}}.$
So because $\mathtt{m}_{\mathsf{A}}<\lVert\mathtt{p}_{\mathsf{A}}\rVert$ we
get
$\mathtt{p}_{\mathtt{p}_{\mathsf{A}}}[\mathtt{m}_{\mathsf{A}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\mathtt{p}_{\mathsf{A}}[\mathtt{m}_{\mathsf{A}}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}.$ Of course, we also have
$\mathtt{p}_{\mathtt{p}_{\mathsf{A}}}[\lVert\mathtt{p}_{\mathsf{A}}\rVert]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}$. Therefore,
$\mathtt{p}_{\mathtt{p}_{\mathsf{A}}}[\mathtt{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}Q(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$Q$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}Q(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$Q$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\mathtt{p}_{\mathtt{p}_{\mathsf{A}}}[\mathtt{m}_{\mathsf{A}}])$
and that gives the sought after
$\exists\mathsf{j}<\mathtt{i}\colon\mathtt{p}_{\mathtt{p}_{\mathsf{A}}}[\mathtt{i}]\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}Q(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\text{\T1\guilsinglleft$Q$\T1\guilsinglright}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$},\mathtt{p}_{\mathtt{p}_{\mathsf{A}}}[\mathsf{j}]).$
_Correctness_ : Lastly, the correctness of $\operatorname{\textsf{{Pvb}}}$
follows from a straightforward inductive argument. In the forward direction,
suppose $\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ is true. Then there really does
exist a proof $p$ with the outlined characteristics. In particular, we can see
that every item of $p$—which includes $\mathsf{A}$—must be a theorem. By
induction on the index $i$: _Base Case_ : If $i=0$, then we must have
$\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$p[i]$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})$ which makes $p[i]$ provable by the
correctness of $\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}$.
_Induction_ : Now let’s assume that the items of $p$ up to index $i$ are known
to be theorems. Then so is the $i+1$st item since
$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ assures us that at least one of the
following is true: _•_ : The $i+1$st item is provable by the correctness of
$\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}$. _•_ : The $i+1$st
item follows by modus ponens from a pair of previous items which we know to be
theorems by inductive assumption. _•_ : The $i+1$st item is of the form
$\operatorname{\textsf{{Pvb}}}(\raise
1.46208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}\emph{\textquotesingle}$}\raise
1.46208pt\hbox{\footnotesize$\urcorner$})$ for some preceding theorem
$\mathsf{A}\emph{\textquotesingle}$, making the $i+1$st item a theorem by the
already demonstrated representability property of
$\operatorname{\textsf{{Pvb}}}$. And in the other direction, if
$\textbf{{T}}\vdash\mathsf{A}$, then arguing as we did for
representability—except relying on correctness instead of provability—we can
see that $[\mathsf{A}]$ satisfies the existential claim expressed by
$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$, making it true.∎

Phew! With that slog behind us let’s take the scenic route past Löb’s Theorem
towards the Second Incompleteness Theorem.

[Löb’s Theorem] Let $\operatorname{\textsf{{Pvb}}}$ be a predicate obeying the
derivability conditions for some theory T which represents every computable
function. Then the following holds for any sentence $\mathsf{A}$.

$\text{If }\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\mathsf{A},\text{ then
}\textbf{{T}}\vdash\mathsf{A}.$

###### Proof.

We begin by using the Diagonal Lemma to construct a fixed point $\mathsf{L}$
of $\operatorname{\textsf{{Pvb}}}(\mathsf{x})\rightarrow\mathsf{A}$ so that
$\textbf{{T}}\vdash\mathsf{L}\leftrightarrow(\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{L}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\mathsf{A}).$ We can then
use the representability and distributivity conditions of
$\operatorname{\textsf{{Pvb}}}$, giving
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{L}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\leftrightarrow(\operatorname{\textsf{{Pvb}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{L}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})\rightarrow\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})).$ Next, the fact that
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{L}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\operatorname{\textsf{{Pvb}}}(\raise
1.96208pt\hbox{\footnotesize$\ulcorner$}\hbox{$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{L}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$}\raise
1.96208pt\hbox{\footnotesize$\urcorner$})$ (re-representability) and
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\mathsf{A}$ (assumption)
combines with the previous to produce
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{L}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})\rightarrow\mathsf{A}.$ This, of
course, establishes $\textbf{{T}}\vdash\mathsf{L}$ by equivalency which in
turn yields $\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{L}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ via the representability of
$\operatorname{\textsf{{Pvb}}}$ and thus finally
$\textbf{{T}}\vdash\mathsf{A}$ by detachement from the above. ∎

[Second Incompleteness Theorem] Let T be a computably enumerable extension of
PA. Then there exists a consistency statement of the form

$\operatorname{\textsf{{Con}}}\enskip\coloneqq\enskip\neg\exists\mathsf{x}\colon\operatorname{\textsf{{Pvb}}}(\mathsf{x})\land\operatorname{\textsf{{Pvb}}}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{x})$

where $\operatorname{\textsf{{Pvb}}}$ is a strong provability predicate for T.
And furthermore, if T is consistent, then any such statement is unprovable in
T.

###### Proof.

The construction of $\operatorname{\textsf{{Con}}}$ directly falls out of our
previously demonstrated Existence Theorem. Suppose then for the sake of
contradiction that $\textbf{{T}}\vdash\operatorname{\textsf{{Con}}}$. And set
$\mathsf{\top}$ to be some provable sentence, e.g.,
$\mathsf{0\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}0}$. Then by
$\operatorname{\textsf{{Pvb}}}$’s representability condition
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.40652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{\top}$}\raise
1.40652pt\hbox{\footnotesize$\urcorner$})$ which together with
$\textbf{{T}}\vdash\operatorname{\textsf{{Con}}}$ implies
$\textbf{{T}}\vdash\neg\operatorname{\textsf{{Pvb}}}(\raise
1.40652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg\mathsf{\top}$}\raise
1.40652pt\hbox{\footnotesize$\urcorner$})$. From this we can get
$\textbf{{T}}\vdash\operatorname{\textsf{{Pvb}}}(\raise
1.40652pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg\mathsf{\top}$}\raise
1.40652pt\hbox{\footnotesize$\urcorner$})\rightarrow\neg\mathsf{\top}$. Hence,
by Löb’s Theorem $\textbf{{T}}\vdash\neg\mathsf{\top}$; an inconsistency. ∎

###  6.1 A Second Second Incompleteness Theorem (And A Third)

Despite our innovations engineering a strong provability predicate was still a
lengthy undertaking. One of the rewards was that we got to visit Löb’s Theorem
on our way towards the Second Incompleteness Theorem. More importantly though,
there’s an air of authority surrounding the HBL-derivability conditions. They
offer a stamp of approval that our consistency statement is _proper_ in some
sense. However, there’s a result due to Robert G. Jeroslow [7] which trades
away the distributivity condition in return for a slightly stronger variant of
the re-representability condition and which still manages to achieve the
Second Incompleteness Theorem. And this result is happily cited in the
literature from time to time. It would appear then that formulations of the
Second Incompleteness Theorem giving less assurances about their consistency
statement are still legitimate. Just how far can we conceivably lower this
bar? Let’s test those limits.

The key is to realize that demanding the distributivity and re-
representability condition for arbitrary sentences is to use a sledgehammer to
crack a nut. What we require is merely to make our predicate see the truth of
certain arguments involving $\mathsf{G}$. This is something we can accomplish
with far less surgery.

[Little Second Incompleteness Theorem—Gödel’s Version] Let T be a consistent
and computably enumerable theory which correctly represents every computable
function. Then there exists an unprovable consistency statement of the form

$\operatorname{\textsf{{Con}}}\enskip\coloneqq\enskip\neg\exists\mathsf{x}\colon\operatorname{\textsf{{Pvb}}}(\mathsf{x})\land\operatorname{\textsf{{Pvb}}}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{x})$

where $\operatorname{\textsf{{Pvb}}}$ is a weak provability predicate for T.

###### Proof.

Using the Diagonal Lemma on
$\neg\operatorname{\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}}$ we can obtain
an unprovable Gödel sentence $\mathsf{G}$ and then put
$\operatorname{\textsf{{Pvb}}}(\mathsf{x})\enskip\coloneqq\enskip\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\mathsf{x})\lor\neg\mathsf{G}.$
First, let’s check that $\operatorname{\textsf{{Pvb}}}$ is indeed a weak
provability predicate. We know from discussing the First Incompleteness
Theorem that $\neg\mathsf{G}$ is false. Therefore,
$\operatorname{\textsf{{Pvb}}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ is true if and only if
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{A}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ is true, allowing
$\operatorname{\textsf{{Pvb}}}$ to effortlessly inherit
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$’s correctness property.
Representability is similarly trivial. And as for the unprovability of
$\operatorname{\textsf{{Con}}}$, just expanding definitions and simple logic
reveals
$\operatorname{\textsf{{Con}}}\leftrightarrow(\operatorname{\textsf{{Con}}}_{\mathsf{G}}\land\mathsf{G})$.
Thus, we have $\operatorname{\textsf{{Con}}}\rightarrow\mathsf{G}$, making
$\operatorname{\textsf{{Con}}}$ unprovable because $\mathsf{G}$ is. ∎

The predicate $\operatorname{\textsf{{Pvb}}}$ used in the above proof probably
appeared to some readers like a rabbit out of a hat. So let me try to motivate
it a little further. Using the equivalency
$\mathsf{G}\leftrightarrow\neg\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{G}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$ we can rewrite
$\operatorname{\textsf{{Pvb}}}(\mathsf{x})$ as
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\mathsf{x})\lor\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{G}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$. Without disrupting the argument
this can then be complicated further into

$\operatorname{\textsf{{Pvb}}}(\mathsf{x})\enskip\colonapprox\enskip(\neg\,\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg\mathsf{G}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}\land\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\mathsf{x}))\lor(\mathsf{x}\mathrel{\leavevmode\resizebox{1.15pt}{1.15pt}{=}}\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg\mathsf{G}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$}\land\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{G}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})).$

Now let me antropomorphize $\operatorname{\textsf{{Pvb}}}$ once again.
Whenever it encounters an ordinary sentence $\operatorname{\textsf{{Pvb}}}$
simply turns around and queries $\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$.
However, when presented with $\neg\mathsf{G}$ our predicate reasons: “Oh, you
want to know whether I believe $\neg\mathsf{G}$? Well, that’s the same as
asking whether I believe $\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}(\raise
1.2954pt\hbox{\footnotesize$\ulcorner$}\hbox{$\mathsf{G}$}\raise
1.2954pt\hbox{\footnotesize$\urcorner$})$. Certainly I’d believe that if
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$ assured me of $\mathsf{G}$.” The
intuition is exactly the same as it is behind the Existence Theorem. It has
only been narrowed down to a special case and stripped of all redundancies.

Notice also that if one actually managed to complete the herculean task of
demonstrating the derivability conditions for
$\operatorname{\textsf{{Pvb}}}_{\mathsf{G}}$, then
$\operatorname{\textsf{{Pvb}}}$ would be able to inherit those just as well.
And ultimately, after confirming
$\operatorname{\textsf{{Con}}}_{\mathsf{G}}\rightarrow\mathsf{G}$, we’d come
full circle to reveal
$\operatorname{\textsf{{Con}}}\leftrightarrow\operatorname{\textsf{{Con}}}_{\mathsf{G}}$.
You could say that all we’ve done is take a drastic shortcut.

Finally, there’s one more obvious idea we need to try. Actually, you try it.

[Little Second Incompleteness Theorem—Rosser’s Version] Let T be a consistent
and computably enumerable extension of PA. Then there exists an _undecidable_
consistency statement of the form

$\operatorname{\textsf{{Con}}}\enskip\coloneqq\enskip\neg\exists\mathsf{x}\colon\operatorname{\textsf{{Pvb}}}(\mathsf{x})\land\operatorname{\textsf{{Pvb}}}(\raise
0.0pt\hbox{\footnotesize$\ulcorner$}\hbox{$\neg$}\raise
0.0pt\hbox{\footnotesize$\urcorner$}\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\frown$}}}\mathsf{x})$

where $\operatorname{\textsf{{Pvb}}}$ is a weak provability predicate for T.

###### Proof.

Exercise. ∎

##  7 A Hierarchy Theorem

Next up, I want to broaden our horizons a little by looking at some more novel
connections to complexity theory. Truth be told, this section was the original
motivation for writing all of this. I just couldn’t bring myself to beeline
straight to this point without filling in the bigger picture. In the process
of doing so one thing led to another till at this point I consider this
section to possibly be the least interesting. At the same time, I didn’t want
to leave it on the cutting room floor.

The thing is, similarities between the First Incompleteness Theorem and the
Halting Problem have long been noted. But looking at our simplified proof of
the Incompleteness Theorem they stand out more than ever. The Halting problem
is proved undecidable by running a certain program on its own source code. And
the First Incompleteness Theorem follows from running a very similar program
on its own representation.

This might bring to mind then that the Halting Problem was famously modified
by Juris Hartmanis and Richard E. Stearns in 1965 in order to establish the
Time Hierarchy Theorem [6]. A question thus arises: can the same modification
be performed on the First Incompleteness Theorem? This is something Gödel
himself already undertook for his so called Speedup Theorem [5]. But by
generalizing to sets of sentences and adding a padding trick we can take this
idea even further and establish an analogue of the Nondeterministic Time
Hierarchy Theorem, originating from Stephen A. Cook [3]. Here’s how.

To start with we’re going to have to be more restrictive as to what
constitutes a proof. Mere computable enumerability doesn’t cut it anymore.

[Canonical Proof Verifier] A proof verifier $\operatorname{\mathit{pv}}$ for
some theory T is considered a _canonical proof verifier_ if for any
$p\in\mathbb{N}$ such that
$\operatorname{\mathit{pv}}(p,\mathsf{A})=\text{\small\char 51}$ for some
sentence $\mathsf{A}$ the following holds:

  * •

$p$ is a list containing only theorems of T or valid sub-proofs.

  * •

If $\mathsf{B}$ follows from the items in $p$ by the usual rules of inference,
then
$\operatorname{\mathit{pv}}(p\operatorname*{\mathrel{\scalebox{0.6}[0.7]{$\raisebox{1.07639pt}{$\frown$}\mkern-17.0mu\raisebox{-1.07639pt}{$\frown$}$}}}[\mathsf{B}],\mathsf{B})=\text{\small\char
51}$.

I’m neglecting to fully spell out the details of the above definition because,
as we’ll see, all we’re going to need is the ability to turn a proof of
$\mathsf{A}$ and a proof of $\mathsf{B}$ into a proof of
$\mathsf{A}\land\mathsf{B}$ and vice versa. I hope you’ll grant that the above
definition covers that.

We’ll also need to define the analogue of a computational problem.

[String Length] $\lvert\cdot\rvert$ denotes the computable function which
determines the length of a number. (The number of digits required to write
it.)

[Proof Problem] Fix a theory T and a proof verifier
$\operatorname{\mathit{pv}}$. Then any set of sentences
$\textbf{{A}}\subseteq\textbf{{T}}$ will be considered a _proof problem_.