\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{incompleteness theorem}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{category_theory}{}\paragraph*{{$(0,1)$-Category theory}}\label{category_theory}

[[!include (0,1)-category theory - contents]]

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{incompleteness_theorems}{}\section*{{Incompleteness theorems}}\label{incompleteness_theorems}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{gdels_incompleteness_theorems}{G\"o{}del's incompleteness theorems}\dotfill \pageref*{gdels_incompleteness_theorems} \linebreak
\noindent\hyperlink{categorical_preliminaries}{Categorical preliminaries}\dotfill \pageref*{categorical_preliminaries} \linebreak
\noindent\hyperlink{syntactic_terminology_and_notation}{Syntactic terminology and notation}\dotfill \pageref*{syntactic_terminology_and_notation} \linebreak
\noindent\hyperlink{diagonalization}{Diagonalization}\dotfill \pageref*{diagonalization} \linebreak
\noindent\hyperlink{incompleteness}{Incompleteness}\dotfill \pageref*{incompleteness} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In [[logic]], an incompleteness theorem expresses limitations on provability within a (consistent) formal [[theory]]. Most famously it refers to a pair of theorems due to [[Kurt Gödel]]; the first incompleteness theorem says roughly that for any [[consistent theory]] $T$ containing [[Peano arithmetic|arithmetic]] and whose [[axioms]] form a [[recursive set]], there is an arithmetic sentence which is true for the [[natural numbers]] $\mathbb{N}$ that cannot be proven in $T$. The second incompleteness theorem shows that for such theories $T$, the sentence can be taken to be a suitable arithmetization of the statement of consistency of $T$ itself, i.e., that no such theory ``can demonstrate its own consistency'' -- can prove an arithmetic statement that encodes the assertion of its consistency.

An incompleteness theorem can be read as an [[undecidable proposition|undecidability result]]: there are formal propositions $p$ in the theory such that neither $p$ nor its [[negation]] $\neg{p}$ have [[proofs]] in the theory. As such, it is part of a long history; for example, axiom systems for [[Euclidean geometry]] not including the [[parallel postulate]] might not decide the parallel postulate, as shown by models for both Euclidean and non-Euclidean geometry. What was novel about G\"o{}del's results is that they worked directly at the level of syntax and applied to any (effectively generated) extension of arithmetic, producing sentences which in effect imply their unprovability.

To some extent, G\"o{}del's incompleteness theorems have always had an air of mystery about them, or at least a reputation of being exceedingly difficult or subtle. The major insight of G\"o{}del, that items in formal logic can be encoded within the recursive structures afforded by arithmetic ([[Gödel numbering]]), is of course a signal achievement not to be underestimated, and the detailed working out of the result that the provability predicate can be encoded as a [[recursive set]] can be said to form the technical core of this work. But the punchline, in the form of his [[diagonalization argument]] that produces a true\footnote{Assuming that the theory is consistent. If the theory is inconsistent, then it can prove falsity and thence anything, including any internal statements of consistency.}  but unprovable sentence, should be seen for what it is: one of many [[diagonalization arguments]] (including for example [[Cantor's theorem]]) that are essentially alike in structure, and familiar to all mathematicians.

In an interview (\href{William+Lawvere#Interview07}{Lawvere 07}) not long after G\"o{}del's 100th birthday, [[William Lawvere]] answered the question

\begin{quote}%
We have recently celebrated Kurt G\"o{}del's 100th birthday. What do you think about the extra-mathematical publicity around his incompleteness theorem?


\end{quote}
by saying (reproduced in \hyperlink{Lawvere69}{Lawvere 69 reprint, p. 2}):

\begin{quote}%
``In `Diagonal arguments and Cartesian closed categories' (\hyperlink{Lawvere69}{Lawvere 69}) we demystified the incompleteness theorem of G\"o{}del and the truth-definition theory of Tarski by showing that both are consequences of some very simple algebra in the Cartesian-closed setting. It was always hard for many to comprehend how Cantor's mathematical theorem could be re-christened as a ''paradox`` by Russell and how G\"o{}del's theorem could be so often declared to be the most significant result of the 20th century. There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for science. Now, one hundred years after G\"o{}del's birth, the organized attempts to harness his great mathematical work to such an agenda have become explicit.


\end{quote}
[[Yuri Manin]] writes in \hyperlink{Manin02}{Manin02, p. 7}:

\begin{quote}%
Baffling discoveries such as G\"o{}del's incompleteness of arithmetic lose some of their mystery once one comes to understand their content as a statement that a certain algebraic structure simply is not finitely generated with respect to the allowed composition laws.


\end{quote}
This diagonalization result, so often obscured, should be laid bare as the simple piece of algebra that it is. We give one approach here, based on the algebra of [[hyperdoctrines]].

\hypertarget{gdels_incompleteness_theorems}{}\subsection*{{G\"o{}del's incompleteness theorems}}\label{gdels_incompleteness_theorems}

\hypertarget{categorical_preliminaries}{}\subsubsection*{{Categorical preliminaries}}\label{categorical_preliminaries}

We define the [[equational theory]] $\mathbf{PRA}$ ([[primitive recursive arithmetic]]) to be [[initial object|initial]] among [[Lawvere theories]] whose generator $1$ is a parametrized [[natural numbers object]]. The [[hom-set]] of morphisms $0 \to 1$ in $\mathbf{PRA}$ is the set of equivalence classes of closed [[terms]], and is identified with the set $\mathbb{N}$ of [[numerals]]. (This $\mathbb{N}$ will serve double duty in a moment, as being also the set of objects of the Lawvere theory.)

The [[first-order theory]] of [[Peano arithmetic]], PA for short, can be presented as a [[Boolean hyperdoctrine]]

\begin{displaymath}
T: \mathbf{PRA}^{op} \to BooleanAlgebra
\end{displaymath}
taking $j \in Ob(\mathbf{PRA}) = \mathbb{N}$ to the set $T(j)$ consisting of $j$-ary [[predicates]] in the language of PA, modulo provable equivalence in PA. If $f: j \to k$ is a morphism of $\mathbf{PRA}$ and $R \in T(k)$, we let $f^\ast (R)$ denote $T(f)(R) \in T(j)$; it can be described as the result of substituting or pulling back $R$ along $f$. There is a corresponding ``action'' of $\mathbf{PRA}$ on $T$,

\begin{displaymath}
\mathbf{PRA}(j, k) \times T(k) \stackrel{action}{\to} T(j)
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
(f, R) \mapsto f^\ast(R),
\end{displaymath}
which allows us to regard $T$ as a $\mathbf{PRA}$-module.

\hypertarget{syntactic_terminology_and_notation}{}\subsubsection*{{Syntactic terminology and notation}}\label{syntactic_terminology_and_notation}

Let $Form(PA)$ be the set of all formulas of PA, with $\Phi(j)$ the set of formulas with $j$ [[free variables]]. There is an equivalence relation on $\Phi(j)$, where two formulas $F, F'$ belong to the same equivalence class $[F]$ if they are provably equivalent in PA. Thus $[-]: \Phi(j) \to T(j)$ is the corresponding quotient map. Let $Term(0)$ denote the set of closed terms in the logical theory $PRA$; morphisms $0 \to 1$ in the Lawvere theory $\mathbf{PRA}$ are equivalence classes of terms, and we let $ev: Term(0) \to \mathbf{PRA}(0, 1)$ be the corresponding quotient map. The map $ev$ has a section $num: \mathbf{PRA}(0, 1) \to Term(0)$ which sends each morphism $0 \stackrel{'n'}{\to} 1$ to the corresponding numeral term (the $n$-fold successor of the zero term). Finally, we have a substitution map

\begin{displaymath}
sub: Term(0) \times \Phi(1) \to \Phi(0)
\end{displaymath}
that substitutes a closed term $\tau$ in for the free variable of $F \in \Phi(1)$, giving a closed formula $sub(\tau, F) \in \Phi(0)$.

There is a standard G\"o{}del coding taking formulas to numerals,

\begin{displaymath}
code: Form(PA) \to \mathbf{PRA}(0, 1),
\end{displaymath}
and we define an application pairing $\cdot$ to be the composite along the top of the following commutative diagram:

\begin{displaymath}
\itexarray{
Form(PA) \times \Phi(1) & \stackrel{code \times 1}{\to} & \mathbf{PRA}(0, 1) \times \Phi(1) & \stackrel{num \times 1}{\to} & Term(0) \times \Phi(1) &  \stackrel{sub}{\to} & \Phi(0) \\ 
 & & & _\mathllap{1 \times [-]} \searrow & \downarrow _\mathrlap{ev \times [-]} & & \downarrow _\mathrlap{[-]} \\ 
 & & & & \mathbf{PRA}(0, 1) \times T(1) & \underset{action}{\to} & T(0).
}
\end{displaymath}
In other words, for all formulas $F \in Form(PA)$ and $R \in \Phi(1)$, we define the pairing $F \cdot R \coloneqq sub(num (code(F)), R)$, and according to the commutative diagram, we have the equation

\begin{equation}
[F \cdot R] = code(F)^\ast ([R])
\label{eqn1}\end{equation}
which will be used in our diagonalization result.

\hypertarget{diagonalization}{}\subsubsection*{{Diagonalization}}\label{diagonalization}

The following result is routine from general recursive-arithmetic properties of G\"o{}del coding; it applies to any extension of PA (or just [[Robinson arithmetic]]) whose formulas can be recursively (computably) enumerated.

\begin{lemma}
\label{}\hypertarget{}{}
There is a primitive recursive function (i.e., a morphism $d: 1 \to 1$ in $\mathbf{PRA}$) such that for all $t \in \Phi(1)$, we have $d \circ code(t) = code (t \cdot t)$.\footnote{This and the next lemma demonstrate the essential truth of Paul Taylor's quip (Practical Foundations of Mathematics, p. 192): ``Lemmas do the work in mathematics: Theorems, like management, just take the credit. A good lemma also survives a philosophical or technological revolution.''} 

\end{lemma}
\begin{theorem}
\label{fix}\hypertarget{fix}{}
For every $R \in \Phi(1)$ there is a fixed point in $\Phi(0)$, i.e., a closed formula $s \in \Phi(0)$ such that $s \Leftrightarrow s \cdot R$ ($s$ is provably equivalent to $s \cdot R$).

\end{theorem}
\begin{proof}
Pick a formula $t \in \Phi(1)$ such that $[t] = d^\ast [R]$, and then put $s = t \cdot t$. We want to show $[s] = [s \cdot R]$. We have

\begin{displaymath}
\itexarray{
[t \cdot t] & = & code(t)^\ast ([t]) & equation\; (1) \\ 
 & \coloneqq & code(t)^\ast (d^\ast [R]) & \\ 
 & = & (d \circ code(t))^\ast ([R]) & (functoriality) \\ 
 & = & (code (t \cdot t))^\ast ([R]) & (by\; the\; lemma)\\ 
 & = & [(t \cdot t) \cdot R] & equation\; (1) 
}
\end{displaymath}
as required.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
The proof of theorem \ref{fix} was written to lay bare its provenance as a special case of [[Lawvere's fixed point theorem]], and its essential kinship with the structure of the standard fixpoint combinator in [[combinatory algebra]]. See \hyperlink{Yanofsky03}{Yanofsky 03}.

\end{remark}
\hypertarget{incompleteness}{}\subsubsection*{{Incompleteness}}\label{incompleteness}

Recall there is also a G\"o{}del coding of PA proofs (certain sequences of PA formulas), $code: Proof(PA) \to \mathbf{PRA}(0, 1)$. The following result applies in fact to any theory like PA that extends basic Robinson arithmetic and whose axioms form a recursive set.

\begin{lemma}
\label{}\hypertarget{}{}
There is a binary primitive recursive predicate $Pf$ such that $Pf(p, x)$ is true in $\mathbb{N}$ if $p$ is the code of a proof of a sentence (a closed formula) with code $x$. Thus there is an unary recursive predicate $Prov \coloneqq \exists_p Pf(p, x) \in T(1)$. Similarly, there is an unary recursive predicate $R = \neg Prov \in T(1)$.

\end{lemma}
\begin{theorem}
\label{}\hypertarget{}{}
\textbf{(G\"o{}del's First Incompleteness Theorem)} There exists a sentence $s$ in the language of PA such that $s$ is logically equivalent to the PA-sentence $code(s)^\ast (\neg Prov)$ (whose interpretation in the model $\mathbb{N}$ is that $s$ has no PA proof).

\end{theorem}
Thus, if $s$ is false in $\mathbb{N}$, then $s$ has a PA proof (so that PA proves a false statement in a model: is inconsistent). In classical logic, the only other alternative is that $s$ is true in $\mathbb{N}$, but then this true sentence (in the language of PA) has no PA proof.

\begin{proof}
Indeed, let $R$ be a formula that represents the unary predicate $\neg Prov$, and let $s$ be a fixed point in the sense $[s] = [s \cdot R]$, which is guaranteed to exist by theorem \ref{fix}. The equality here is logical equivalence, and $[s \cdot R] = code(s)^\ast (\neg Prov)$ by equation \eqref{eqn1}.

\end{proof}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[Löb's theorem]]


\item [[Lawvere's fixed point theorem]]


\item [[Chaitin's incompleteness theorem]]


\item [[Deligne completeness theorem]]


\item [[foundations of mathematics]]


\item [[platonism]]


\item [[arithmetic universe]]



\end{itemize}
\hypertarget{References}{}\subsection*{{References}}\label{References}

\begin{itemize}%
\item [[William Lawvere]], \emph{Diagonal Arguments and Cartesian Closed Categories}, Lecture Notes in Mathematics, 92 (1969), 134-145 (\href{http://tac.mta.ca/tac/reprints/articles/15/tr15abs.html}{TAC})


\item [[Yuri Manin]], \emph{Georg Cantor and his heritage}, \href{http://arxiv.org/abs/math/0209244}{arXiv:math/0209244}


\item Noson S. Yanofsky, \emph{A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points}, arXiv:math/0305282 (\href{http://arxiv.org/abs/math/0305282}{web})



\end{itemize}
A brief review discussion explicitly in the context of [[type theory]]/[[topos theory]] is in

\begin{itemize}%
\item Erik Gregersen, \emph{\href{http://www.britannica.com/EBchecked/topic/369221/foundations-of-mathematics/35468/Internal-language}{Internal lanuage}}, Encylcopedia Britannica

\end{itemize}
A [[formal proof]] of the G\"o{}del-Rosser incompleteness theorem in [[Coq]] is given in

\begin{itemize}%
\item [[Russell O'Connor]], \emph{Essential Incompleteness of Arithmetic Verified by Coq} (\href{http://r6.ca/Goedel/goedel1.html}{web})

\end{itemize}
Formal proof of the second incompleteness theorem is discussed in

\begin{itemize}%
\item Lawrence Paulson, \emph{A Mechanised Proof of G\"o{}del's Incompleteness Theorems using Nominal Isabelle} (\href{https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/Goedel-ar.pdf}{pdf})

\end{itemize}
The following contains a careful discussion of the incompleteness theorem in the context of categorical foundations using the [[free topos]]:

\begin{itemize}%
\item [[Jim Lambek]], [[Phil Scott]], \emph{Reflections on Categorical Foundations of Mathematics} , pp.171-185 in Sommaruga (ed.), \emph{Foundational Theories of Classical and Constructive Mathematics}, Springer New York 2011. (\href{https://www.site.uottawa.ca/~phil/papers/LS11.final.pdf}{draft})

\end{itemize}
A \emph{bref survol technique} of G\"o{}del's theorem within the landscape of [[Hilbert's program]] can be found in the first chapters of

\begin{itemize}%
\item [[Jean-Yves Girard]], \emph{Le point aveugle I} , Hermann Paris 2006. (\href{http://iml.univ-mrs.fr/~girard/cours/hermann.pdf.gz}{chapters 1-2})

\end{itemize}
See also the discussion in [[list-arithmetic pretoposes]]

\begin{itemize}%
\item [[Maria Maietti]], \emph{Joyal's arithmetic universe as list-arithmetic pretopos}, Theory and Applications of Categories, Vol. 24, 2010, No. 3, pp 39-83. (\href{http://www.tac.mta.ca/tac/volumes/24/3/24-03abs.html}{TAC})

\end{itemize}
[[!redirects incompleteness theorem]] [[!redirects incompleteness theorems]] [[!redirects Gödel incompleteness theorem]] [[!redirects Gödel incompleteness theorems]] [[!redirects Gödel's incompleteness theorem]] [[!redirects Gödel's incompleteness theorems]] [[!redirects Gödel's incompleteness theorem]] [[!redirects Gödel's incompleteness theorems]] [[!redirects Gödel's incompleteness theorem]] [[!redirects Gödel's incompleteness theorems]]

[[!redirects Gödel's theorem]] [[!redirects Gödel's theorems]] [[!redirects Gödel's theorem]] [[!redirects Gödel's theorems]] [[!redirects Gödel's theorem]] [[!redirects Gödel's theorems]]



\end{document}