On The Unreasonably Broad Uses of Diagonalization

Think of any program which mangles source code. This program should take source code as a string and do something with it: hash it, encrypt it, append it to itself, delete it, or anything else.

Here’s a very surprising result. Each of those mangling transformations is weak to a specific string of source code, whose runtime behavior will be completely unchanged by the mangling.

In other words, regardless of how intense your mangling is, it is guaranteed to not to be able to affect some strangely strong and robust program. We call that specific program a fixed point of your transformation.

Your transformation might be “encrypt the source code, interpret that as an integer, then print the third largest prime factor of that integer twelve times.” And yet, I tell you, you’re in luck: I have a program in my back pocket which will behave exactly the same before and after.

Let’s take a basic example: the transformation that swaps ‘a’ and ‘z’. What are its fixed points? As expected console.log("hello"), as well as every other program with neither ‘a’s nor ‘z’s, are unchanged.

const swapAandZ = (input: string) =>
  input.replace(/[az]/g, c => c === 'a' ? 'z' : 'a')

const input = 'console.log("hello")'

eval(input) === eval(swapAandZ(input))
// our === implies the same return value, console outputs, error text, etc.

Some source transformations are slightly more stubborn; can you think of a program which will be unchanged by “append the source to itself?”

It turns out that while (true) {...} (or the empty program) are both fixed points of the doubling transformation.

const double = (source: string) => source + source

const input = "while (true) {console.log('loop');} "

eval(input) // => loop loop loop loop loop ...
eval(double(input)) // => loop loop loop loop loop ...

But then there are transformations whose fixed points are extremely non-obvious. Can you think of a fixed point of “hash the source and execute that hash”? The program would need to behave exactly the same hashed and unhashed.

const hash = (source: string) => 
  createHash('sha256').update(source).digest('hex');

const input = "some crazy program"

// eval(input) === eval(hash(input))

Nevertheless, as promised, we will prove that in general, any transformation, no matter how crazy, must have a fixed point.

// for any transformation
const transform: (source: string) => string;

// there exists an input
const input: string;

// where executing the program is the same as executing its transformation
eval(input) === eval(transform(input))

The technique we’ll use to prove this remarkable truth is a diagonalization trilemma. To warm up to the technique, we’ll start with a reminder of the proof that there are more reals than natural numbers. Then we’ll prove the above result, that all code transformation programs have a fixed point. This result is called Rogers’s Theorem. Finally, we’ll prove that a seemingly powerful class of functions, the primitive recursive functions, can’t be complete.

We’ll then examine a terse and opaque piece of math called the Diagonal Lemma, which we will understand by analogy, as Rogers’s theorem applied to math instead of code. We’ll then prove it with our familiar diagonalization trilemma technique.

Finally, with the powerful Diagonal Lemma in hand, we’ll sketch a pair of excellent proofs of Gödel’s First Incompleteness Theorem (all theories must be either incomplete or inconsistent) and Tarski’s Undefinability of Truth (theories cannot define an internal notion of truth).

Warm Up: Cantor

You might recognize diagonalization from the famous proof that there are more real numbers than natural numbers. We’ll walk through it again here, with an eye towards introducing the trilemma that will guide us through Rogers and the Diagonal Lemma, into Gödel and Tarski.

The argument starts by building a complete numbered list of every real number between 0 and 1:

1 => 0.139042986720983745...
2 => 0.349857294587293845...
3 => 0.239841509204872018...

We’ll define an evaluation function $f(i)(j)$ that takes the $i$ th real number and returns its $j$ th decimal digit: [0]

f(3)(3) => 0.23[9]841509204872018... => 9

We also create a “make it different” function $\delta$ , which takes a digit and returns a different digit. Many rules works; we’ll map everything to 1, except 1 gets mapped to 2:

const delta = (x: number) => x === 1 ? 2 : 1

Now, we’ll build a new real number $g$ by going through the diagonal values ( $f(1)(1)$ , $f(2)(2)$ , etc) and applying $\delta$ to choose a different digit at each location for $g$ : $g(j) = \delta(f(j)(j))$ . Reading the 1st digit of the 1st number, the 2nd digit of the 2nd, the 3rd of the 3rd, and so on, the diagonal starts 1, 4, 9, and so $g$ starts 0.211…

d(f(1)(1)) => d(0.[1]39042986720983745...)  => d(1) => 2
d(f(2)(2)) => d(0.3[4]9857294587293845...)  => d(4) => 1
d(f(3)(3)) => d(0.23[9]841509204872018...)  => d(9) => 1

$g$ differs from the first number at digit 1 (it must differ, because $\delta$ always changes its input, and the first digit of g is $\delta$ (the first digit of f), the second number at digit 2, and so on. But we started by listing all the rational numbers between zero and one, so how could $g$ not be in this list?

One of three things must have gone wrong:

Maybe $\delta$ is broken, and doesn’t actually change every digit. If $\delta$ has a fixed point, $g$ might simply be hidden somewhere in the list.
Maybe $g$ is a new kind of object, and does not belong in the list.
Maybe the list is incomplete.

This is the diagonalization trilemma.

Well, $\delta$ is clearly not broken, and $g$ is definitely a real number, so it must that our list of real numbers is incomplete.

And since every natural number is listed on the left side of the list, but there’s at least one real number not listed on the right side of the list, there must be more reals than naturals.

Rogers’ Theorem: Fixed Points of Program Transformations

Now let’s try the exact same trick, but on programs.

This time we’re going to list all the JavaScript programs, alphabetically:

1 => eval('a')
2 => eval('b')
3 => eval('c')
...
10348423 => eval('x => x + x')

Our evaluation function $f(i)(j)$ takes the $i$ th program in the list and runs it on the input $j$ .

f(10348423)(1)
  => eval('x => x + x')(eval('a'))
  => 'aa'

We’re going to use const delta = (x: string) => x + " + 1". Recall that $\delta$ operates on the source, so for example

delta(f(10348423)(1))
  => eval('x => x + x')((eval('a')) + 1
  => 'aa' + 1
  => 'aa1'

Just like before, we build a new object $g$ (in this case a program and not a real number), with $g(j) = \delta(f(j)(j))$ . And just like before, $g$ can’t be any program on our list — it disagrees with every program at the diagonal position.

Check this by arguing to yourself: why is $g$ not the program x => x + 4, for example? Because that program appears in our list at position 10521488, and when evaluated at 10521488 returns 10521488 + 4 = 10521492. But $g(10521488)$ returns $\delta(10521492)$ , which is anything other than 10521492. So they can’t be the same program.

So $g$ isn’t on the list. What went wrong? Again, our three suspects are the $\delta$ , the $g$ , and the list. It must be one of:

$\delta$ has a fixed point. It doesn’t, right?
$g$ might be misbehaved or not writable in JavaScript. But we can describe how to compute $g$ : “look up the $n$ th program, run it on input $n$ , append 1.” That sure sounds like something you could write in JavaScript.
Our list of JavaScript programs might not be exhaustive. But surely we’ll eventually print out even the longest of JavaScript programs by iterating alphabetically?

Do you see the issue? It turns out that our $\delta$ does have a fixed point. In particular, eval("while (true) {}") is a fixed point of $\delta$ . If your program loops forever, and you add one to the result, it still loops forever.

Not only that, but all viable $\delta$ s share this flaw. To build the “change that output” program $\delta$ , you need to know whether your original program halts or not. And in general, you can’t know whether it halts or loops, so you can’t build a good $\delta$ . [1]

This constitutes a somewhat shocking proof that it’s impossible to build a function $\delta$ that takes any program and modifies it to produce a different result. In other words, all programs mapping functions to functions have a fixed point. This result is called Rogers’s Theorem.

There’s a nice immediate corollary: any language allows you either solve the halting problem or build an interpreter for itself. JavaScript allows interpreters but not halting-solvers. Primitive recursive functions, which we’ll examine next, allow halting-solvers (all P.R. functions halt), but can’t build their own interpreters. These correspond to the (1) and (3) branches of the trilemma respectively.

Example: Primitive Recursion

Next, we’ll look at primitive recursive functions. Primitive recursive functions are all the functions made of combinations five functional building blocks: $z, s, p, c$ and $\rho$ . Don’t worry if you haven’t seen them before. The upshot is that you can easily list them, numbering them sequentially:

1 => z() // zero function
2 => s() // +1 function
3 => p() // "projection" function
...
372 => c(s, z) // composition of 0 and +1 (1)
373 => c(s, s) // composition of +1 and +1 (+2)
...

We’ll choose $f(i)(j)$ as the evaluation function, which takes the $i$ th primitive recursive function and computes it on $j$ . For example, evaluating the 373rd function at the value 3:

f(373, 3) 
  => c(s, s)(3)
  => s(s(3))
  => 3 + 1 + 1
  => 5

We can easily build a function $\delta(x) = x + 1$ that has no fixed point.

So we consult our trilemma, and decide that either (1) $\delta$ is broken, (2) the list $f(i)$ isn’t complete, or (3) $g$ is a new kind of object.

$\delta$ has no fixed point, and $f(n)$ obviously enumerates all the primitive recursive functions (by definition). So it must be that $g(i) = \delta(f(i)(i))$ is a new kind of object: a non-primitive-recursive (but computable) function.

This might surprise you if you’ve only played with primitive recursive functions for a little bit: they can compute functions like plus, times, isPrime, nthPrime, ifElse, and more. But it turns out that they aren’t Turing complete, since they can’t simulate the eval function.

Diagonalization Trilemma

We’re going to prove this by asserting that one of three things must always be true. Situation: you have a list of all the objects of some type, and a “make it different” function, which takes an output value and returns a different output value in that group. We will build a new object “g”, which has the same shape but is definitely not on the list. Therefore, we live in one of three worlds:

The list is broken and does not include every object in the group. “g” is a well behaved object of the type which you somehow failed to list.
“g” is somehow of a different type from the list objects, even though it looks similar.
The “make it different” function is broken, and does not always “make it different”; for some objects it actually returns the same thing.

Trilemma Proof

We’ll make a quick stop to formalize and prove this trilemma that we’ve been using.

Diagonalization. For all sets $X$ and $Y$ with a function $f: X \times X \rightarrow Y$ and a function $\delta: Y \rightarrow Y$ with no fixed point, there exists at least one function $g: X \rightarrow Y$ such that there exists no $k$ such that $f(k) = g$ .

Proof. Let $g(x) = \delta(f(x, x))$ . For any $k$ , $g \neq f(k)$ , since $g(k) \neq f(k)(k)$ .

The important part of this proof is that it sets up our favorite trilemma:

Trilemma. For all sets $X$ and $Y$ with a function $f: X \times X \rightarrow Y$ , and a function $\delta: Y \rightarrow Y$ , at least one of the following three things must be true:

$\delta: Y \rightarrow Y$ has a fixed point.
There exists some $g: X \rightarrow Y$ which isn’t found in $f(n)$ for $n \in \mathbb{N}$ , but $g$ is obviously the right kind of object, so the list of objects $f(n)$ must not be exhaustive.
There exists some $g: X \rightarrow Y$ which isn’t found in $f(n)$ for $n \in \mathbb{N}$ , but $f(n)$ obviously lists all the possible objects, so $g$ must actually be a new and different kind of object.

New Tool: Diagonal Lemma

We’ve just seen that all programs that map programs to other programs have a fixed point. Next, we’re going to see a very similar result, but this time applied to mathematical theorems. It’s wrapped up in an opaque piece of math called the Diagonal Lemma. But once we understand the Diagonal Lemma, it opens the door to amazingly short demonstrations of Godel’s Theorem and Tarski’s Theorem.

Let’s say you’re working in some proof system, which is basically some laws (“axioms”) plus some deductive rules. Call that system $T$ .

Give me a statement $A(x)$ . Then $T$ can prove that there exists a sentence $\phi$ where $\phi$ is only true if $A(\ulcorner \phi \urcorner)$ is true, where $\ulcorner \phi \urcorner$ is the numerical representation of the bytes in $\phi$ . [2]

Mathematically, we can express the same as follows, with $T \vdash$ read “T proves:”

\forall A \, \exists \phi \quad T \vdash \phi \iff A(\ulcorner \phi \urcorner)

Suppose we’re dealing with $A(x) := x * 2 = 4$ . Then there’s a sentence $\phi$ where strong enough theories can prove that $\phi \iff \ulcorner \phi \urcorner * 2 = 4$ . In this case, we can choose $\phi$ to be the sentence $0 = 1$ . Then $\ulcorner \phi \urcorner = 3161393$ , and indeed $T$ can prove that

0 = 1 \iff 3161393 * 2 = 4

since both sides are false.

In the domain of programs, we’ve seen that any program you can name that transform programs into other programs has a fixed point. The Diagonal Lemma says something extremely similar for math: any statement you can name that maps the numerical representation of a statement to another statement has a fixed point. And as a bonus, strong enough theories can prove that.

Proof Sketch: Diagonal Lemma

Consider a sufficiently strong theory $T$ and any arbitrary formula $A$ with one free variable. Then there exists a $\psi$ so that $T$ proves that $\psi \iff A(\ulcorner \psi \urcorner)$ .

The set of formulas with one free variable are enumerable (for example, by printing all strings and then discarding any that have more than one variable symbol):

274 => "x = 1"
...
672 => "x = x"
...
1837501 => "5x = x && 4 = 5"

We’re going to define a function $f(s)(s')$ which evaluates $s$ on the byte-representation of $s'$ . For example, f( $x$ is prime)( $x$ * $x$ = 100) evaluates to “33823693116354608 is prime” (the string x*x=100 in UTF-8 has the decimal representation 33823693116354608). Notice that $f$ maps two formulas with a free variable into a single sentence with no free variables.

Let $\delta(\phi) = A(\ulcorner \phi \urcorner)$ .

Now for the trilemma. All the formulas in our system definitely have a written representation, and all written representations with one free variable definitely count as formulas in our system.

So it must be that $\delta$ has a fixed point. And that fixed point is exactly what we’re after: some $\psi$ so that $\psi$ and $A(\ulcorner \psi \urcorner)$ are logically equivalent. (Notice that we’ve shifted from “output equivalence” to “logical equivalence.”)

So we’ve seen how we can prove this. We’re going to omit the proof that $T$ itself can also prove this, since it’s a bit too hairy for our taste. If you look into it, it basically involves proving that $T$ can construct and prove this same argument inside itself.

Proof Sketch: Gödel’s Incompleteness Theorem

We’ve finally arrived at Gödel’s Incompleteness Theorem. Here’s a quick reminder of the statement.

Gödel’s First Incompleteness Theorem. Any sufficiently powerful theory must be either inconsistent or incomplete.

The core idea is to construct a sentence $S$ like “this sentence is unprovable.” Then if $S$ is provable, it’s wrong (the surrounding theory can prove things that are contradictory; this is called being inconsistent). If $T$ can’t prove $S$ , then $S$ is true (the surrounding theory has truths that it can’t prove; this is called being incomplete).

That’s a slick argument, but all of the complexity hides inside questions like, are sentences like “this sentence is unprovable” even allowed? How do you express something like “this sentence” formally? To our happy surprise, the Diagonal Lemma allows us to build precisely these sentences.

Let $A(\ulcorner x \urcorner) =$ $\forall p$ , the string $p$ is not a proof of $x$ . In other words, $A(\ulcorner x \urcorner)$ = $x$ is unprovable. Then by the Diagonal Lemma, we can use $T$ to prove that there exists an $x$ with $x \iff A(\ulcorner x \urcorner)$ , or $x \iff$ ( $x$ is unprovable). And ” $x \iff$ ( $x$ is unprovable)” is exactly “this sentence is unprovable.” So we can build these sentences!

Proof Sketch: Tarski’s Theorem

Here’s a quick reminder of what Tarski’s Theorem says.

Tarski’s Theorem. Any sufficiently powerful theory cannot define its internal notion of truth.

To prove it, we take $A(\ulcorner x \urcorner)$ = ( $x$ is not true). The Diagonal Lemma guarantees that we can prove the existence of an $x$ such that $x \iff$ ( $x$ is not true). But ” $x$ is true $\iff$ $x$ is not true” is obviously contradictory.

The only thing we can point to is our original $A$ , which must have been flawed. It must be that theories cannot define predicates like $x$ is true or $x$ is not true.

Conclusion

I hope you’re convinced that diagonalization is an extremely powerful tool.

From our original diagonalization trilemma, we were able to immediately show that primitive recursive functions aren’t complete, that there are more reals than naturals, and that program-transforming-programs must all have fixed points.

Then we used the same trilemma to construct a new tool, the Diagonal Lemma, and closed out the post by using it to construct the strange sentences required for Gödel and Tarski’s famous theorems.

We’ve kept the math relatively light, leaning on intuition and code where necessary. If you want a more rigorous treatment of this topic, I highly recommend continuing with Yanofsky [0], upon which this post is based.

Notes

[0] Note that we’ll use the curried $f(3)(5)$ and uncurried $f(3, 5)$ forms interchangeably in this post.

[1] A delightful corollary: if your language is weak enough that you can solve the halting problem, then it must not be able to build an interpreter for itself. That’s what happens with P.R. functions, which all halt.

Appendix

Gödel Numbers

Gödel numbers are a way of converting formula into numbers. We denote the Gödel number of $x$ as $\ulcorner x \urcorner$ . You can imagine $\ulcorner x \urcorner$ just interpreting the underlying bytes of $x$ as an integer instead of a string.

const gödel = (s: string): bigint => {
  const byteArray = new TextEncoder().encode(s);
  const hexString = Array.from(byteArray)
    .map((byte) => byte.toString(16).padStart(2, "0"))
    .join("");
  return BigInt(`0x${hexString}`);
};

const unGödel = (n: bigint): string => {
  const hexString = n.toString(16);
  const byteArray = new Uint8Array(
    hexString.match(/.{1,2}/g)!.map((byte) => parseInt(byte, 16)),
  );
  return new TextDecoder().decode(byteArray);
};

console.log(gödel("x * 2 = 4")); // 2215926989203043065908n
console.log(unGödel(2215926989203043065908n)); // x * 2 = 4

Diagonalization Proof

Here’s the straight math version of the general diagonalization argument.

Proof. Let $g(x) = \delta(f(x, x))$ . For any $k$ , $g \neq f(k)$ , since $g(k) \neq f(k)(k)$ .

The Diagonalization Trilemma with Exposition

Diagonalization. Let’s say you have an “evaluation” function $f: X \times X \rightarrow Y$ . You can think of $f(3)(5)$ as selecting the 3rd object from a long list of objects, and evaluating it on 5. [0]

Let’s say you also have a $\delta: Y \rightarrow Y$ with no fixed point. You can think of $\delta$ as a “give me something different” function: it changes every $y$ into a different $y$ .

Then there exists a function $g: X \rightarrow Y$ that isn’t equal to $f(k)$ for any $k$ . In other words, there’s at least one new object $g$ that isn’t equal to $f(3)$ or $f(55)$ or $f(574)$ , or any other object $f(x)$ in the original list of objects. (Note that $f(55)$ and $g$ are both functions representing objects.)

Proof. Take $g(x)$ as $\delta(f(x)(x))$ . For any $k$ , $g \neq f(k)$ , since $g(k) \neq f(k)(k)$ . $\blacksquare$

Spelling out the proof, if you’re concerned that maybe $g = f(234)$ , you can check that at $g$ and $f(234)$ differ at index 234: $g(234) \neq f(234)(234)$ . That’s because $g(234)$ does equal $\delta(f(234)(234))$ , which is different from $f(234)(234)$ because $\delta$ is the “give me something different” function.

The most important part of this proof is that it establishes a crucial trilemma, which we’ve used repeatedly above.

Acknowledgements

This post (and the primitive recursive post) were prepared as part of my final work for the MIT class Seminar in Logic (18.504). Thanks to Henry Cohn, Lisa Kondrich, and Laker Newhouse for their extensive suggestions, feedback, and help with both this post and the primitive recursive introduction post.

References

[0] Noson S. Yanofsky (2003). A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points*. Bulletin of Symbolic Logic, 9(3), 362–386.*

[1] Garrabrant, S., & Eisenstat, S. (n.d.). Diagonalization fixed point exercises. Retrieved from https://www.lesswrong.com/posts/FZkLa3GRLW97fpknG/diagonalization-fixed-point-exercises

[2] Kelly, K. T. (n.d.). Computability and Learnability.

[3] Primitive recursive function. (2023). Retrieved from https://en.wikipedia.org/wiki/Primitive_recursive_function

[4] Smith, P. (2013). An Introduction to Gödel’s Theorems. Cambridge, England: Cambridge University Press.

[5] Solomon, E. (1958). Unpacking the diagonal lemma. Retrieved from https://math.stackexchange.com/questions/127852/unpacking-the-diagonal-lemma