<! --- LETTERS --->
$$ \newcommand{\lR}{\mathbb{R}} $$
$$ \newcommand{\lZ}{\mathbb{Z}} $$
$$ \newcommand{\lN}{\mathbb{N}} $$
$$ \newcommand{\lI}{\mathbb{I}} $$
$$ \newcommand{\II}{\mathbb{I}} $$
$$ \newcommand{\bI}{\mathbf{I}} $$
$$ \newcommand{\bC}{\mathbf{C}} $$
$$ \newcommand{\bD}{\mathbf{D}} $$
$$ \newcommand{\bE}{\mathbf{E}} $$
$$ \newcommand{\bF}{\mathbf{F}} $$
$$ \newcommand{\iI}{\mathsf{I}} $$
$$ \newcommand{\iA}{\mathsf{A}} $$
$$ \newcommand{\iB}{\mathsf{B}} $$
$$ \newcommand{\iC}{\mathsf{C}} $$
$$ \newcommand{\iD}{\mathsf{D}} $$
$$ \newcommand{\iE}{\mathsf{E}} $$
$$ \newcommand{\iF}{\mathsf{F}} $$
$$ \newcommand{\iM}{\mathsf{M}} $$
<! --- SYMBOLS --->
$$ \newcommand{\eps}{\epsilon} $$
$$ \newcommand{\SetCat}{\mathrm{Set}} $$
$$ \newcommand{\Bool}{\mathrm{Bool}} $$
$$ \newcommand{\Pos}{\mathrm{Pos}} $$
$$ \newcommand{\lbl}{\mathsf{lbl}} $$
$$ \newcommand{\subdiv}{\mathsf{sd}} $$
$$ \newcommand{\Hom}{\mathrm{Hom}} $$
$$ \newcommand{\Fun}{\mathrm{Fun}} $$
$$ \newcommand{\Psh}{\mathrm{PSh}} $$
<! --- OPERATORS --->
$$ \newcommand{\dim}{\mathrm{dim}} $$
$$ \newcommand{\id}{\mathrm{id}} $$
$$ \newcommand{\src}{\partial^-} $$
$$ \newcommand{\tgt}{\partial^+} $$
$$ \newcommand{\und}[1]{\underline{#1}} $$
$$ \newcommand{\abs}[1]{\left|{#1}\right|} $$
$$ \newcommand{\op}{^{\mathrm{op}}} $$
$$ \newcommand{\inv}{^{-1}} $$
<! --- CATEGORIES, FUNCTORS AND CONSTRUCTIONS --->
$$ \newcommand{\ttr}[1]{\mathfrak{T}^{#1}} $$
$$ \newcommand{\lttr}[2]{\mathfrak{T}^{#1}{(#2)}} $$
$$ \newcommand{\truss}[1]{\mathsf{T}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\sctruss}[1]{\bar{\mathsf{T}}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\rotruss}[1]{\mathring{\mathsf{T}}\!\mathsf{rs}_{#1}} $$
$$\newcommand{\trussbun}[1]{\mathsf{TrsBun}_{#1}} $$
$$ \newcommand{\trusslbl}[1]{\mathsf{Lbl}\mathsf{T}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\blcat}[1]{\mathsf{B}\mathsf{lk}_{#1}} $$
$$ \newcommand{\blset}[1]{\mathsf{Blk}\mathsf{Set}_{#1}} $$
$$ \newcommand{\fcl}[2]{\chi^{#1}_{#2}} $$
$$ \newcommand{\Entr}{\mathsf{Entr}} $$
$$ \newcommand{\Exit}{\mathsf{Exit}} $$
<! --- ARROWS AND RELATIONS --->
$$ \newcommand{\fleq}{\preceq} $$
$$ \newcommand{\fles}{\prec} $$
$$ \newcommand{\xto}[1]{\xrightarrow{#1}} $$
$$ \newcommand{\xot}[1]{\xleftarrow{#1}} $$
$$ \newcommand{\ot}{\leftarrow} $$
$$ \newcommand{\toot}{\leftrightarrow} $$
$$ \newcommand{\imp}{\Rightarrow} $$
$$ \newcommand{\iff}{\Leftrightarrow} $$
$$ \newcommand{\iso}{\cong} $$
$$ \newcommand{\into}{\hookrightarrow} $$
$$ \newcommand{\proto}{\longrightarrow\mkern{-2.8ex}{\raisebox{.3ex}{$\tiny\vert$}}\mkern{2.5ex}} $$
<! --- DIAGRAM ARROWS --->
<! ---... should replace \rlap by \mathrlap, see KaTeX doc --->
$$ \newcommand{\ra}[1]{\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$
$$ \newcommand{\la}[1]{\xleftarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$
$$ \newcommand{\da}[1]{\downarrow\raisebox{.5ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\dra}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}}\kern-.5ex\searrow}} $$
$$ \newcommand{\dla}[1]{\swarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\ua}[1]{\uparrow\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\ura}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}\kern-.5ex\nearrow}} $$
$$ \newcommand{\ula}[1]{\nwarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
Abstract. Diagonal arguments are ubiquitious. We present them in general form, and mention how specific examples arise from this presentation.
Context
Among small things, some things are, relatively speaking, smaller than others. Diagonal arguments unveil these differences.
Key ingredients
We need two ingredients:
- The applier $f(x,y)$: some way $f$ of building a table over $\mathbb{N}^2$.
- The modifier $g$: some endo-operation on output of $f$
Example: the tuple $(x,y) \in \mathbb{N}^n$ could represent a program code $x$ from a class of programs $\mathcal{U}$ and an input $y$ and $f(x,y) = x(y)$ is the application of $x$ to $y$.
The key step
With our key ingredients at hand, we can now do the following magical thing:
- Let’s construct a new sequence: $h(x) = g(f(x,x))$.
The key cases
We can have the following cases:
- Case 1: $h$ is the $n$th row in the table, e.g. $h(x)$ is $f(p,x)$ for $p$ the $n$th programme
- Conclusion: fixpoint for $g$, namely, $g(f(n,n)) = f(n,n)$
- Case 2: $h$ is not a row in the table (e.g. because we know that $g$ cannot have a fixpoint). Then can make on of two conclusions:
- Case 2.1: the sequence $h$ cannot be of the form $f(x,-)$ (“$h$ is not among the class $\mathcal{U}$”)
- Case 2.2: Or else, the table $f$ could not have be constructed in the first place (i.e., there was no way to compute it)
There is a vague “size” interpretation of these cases. In case 1, $f$ and $g$ are size-preserving; in case 2.1, $g$ is not, in case 2.2, $f$ is not.
Some Examples
Let’s see some examples for the above cases.
- case 2.2 examples:
- Halting problem is undecidable
- Provability in strong enough proof systems undecidable
- case 1.1
- constructing a Gödel sentence (fixpoint for F(x) = (exists no proof tree for formula no. x), in other words, at the fixpoint: formula #$n$ says “exists no proof tree for formula #$n$”.)
- (constructing fixpoints of various other operators)
- case 2.1:
- Real numbers $r \in \mathbb{R}$ that are not in the image of a map from $\mathbb{N}$
Help?
This is a stub, feel free to comment with expansions!
