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))
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)
eval(double(input))
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"
Nevertheless, as promised, we will prove that in general, any transformation, no matter how crazy, must have a fixed point.
const transform: (source: string) => string;
const input: string;
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 ith real number and returns its jth decimal digit: [0]
f(3)(3) => 0.23[9]841509204872018... => 9
We also create a “make it different” function δ, 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 δ to choose a different digit at each location for g: g(j)=δ(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 δ always changes its input, and the first digit of g is δ(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 δ is broken, and doesn’t actually change every digit. If δ 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, δ 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.
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 ith 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 δ 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)=δ(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 δ(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 δ, the g, and the list. It must be one of:
- δ 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 nth 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 δ does have a fixed point. In particular, eval("while (true) {}") is a fixed point of δ. If your program loops forever, and you add one to the result, it still loops forever.
Not only that, but all viable δs share this flaw. To build the “change that output” program δ, 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 δ. [1]
This constitutes a somewhat shocking proof that it’s impossible to build a function δ 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 ρ. Don’t worry if you haven’t seen them before. The upshot is that you can easily list them, numbering them sequentially:
1 => z()
2 => s()
3 => p()
...
372 => c(s, z)
373 => c(s, s)
...
We’ll choose f(i)(j) as the evaluation function, which takes the ith 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 δ(x)=x+1 that has no fixed point.
So we consult our trilemma, and decide that either (1) δ is broken, (2) the list f(i) isn’t complete, or (3) g is a new kind of object.
δ has no fixed point, and f(n) obviously enumerates all the primitive recursive functions (by definition). So it must be that g(i)=δ(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×X→Y and a function δ:Y→Y with no fixed point, there exists at least one function g:X→Y such that there exists no k such that f(k)=g.
Proof. Let g(x)=δ(f(x,x)). For any k, g=f(k), since g(k)=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×X→Y, and a function δ:Y→Y, at least one of the following three things must be true:
- δ:Y→Y has a fixed point.
- There exists some g:X→Y which isn’t found in f(n) for n∈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→Y which isn’t found in f(n) for n∈N, but f(n) obviously lists all the possible objects, so g must actually be a new and different kind of object.
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 ϕ where ϕ is only true if A(┌ϕ┐) is true, where ┌ϕ┐ is the numerical representation of the bytes in ϕ. [2]
Mathematically, we can express the same as follows, with T⊢ read “T proves:”
∀A∃ϕT⊢ϕ⟺A(┌ϕ┐)
Suppose we’re dealing with A(x):=x∗2=4. Then there’s a sentence ϕ where strong enough theories can prove that ϕ⟺┌ϕ┐∗2=4. In this case, we can choose ϕ to be the sentence 0=1. Then ┌ϕ┐=3161393, and indeed T can prove that
0=1⟺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 ψ so that T proves that ψ⟺A(┌ψ┐).
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 δ(ϕ)=A(┌ϕ┐).
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 δ has a fixed point. And that fixed point is exactly what we’re after: some ψ so that ψ and A(┌ψ┐) 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(┌x┐)= ∀p, the string p is not a proof of x. In other words, A(┌x┐) = x is unprovable. Then by the Diagonal Lemma, we can use T to prove that there exists an x with x⟺A(┌x┐), or x⟺ (x is unprovable). And ”x⟺ (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(┌x┐) = (x is not true). The Diagonal Lemma guarantees that we can prove the existence of an x such that x⟺ (x is not true). But ”x is true ⟺ 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 ┌x┐. You can imagine ┌x┐ 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"));
console.log(unGödel(2215926989203043065908n));
Diagonalization Proof
Here’s the straight math version of the general diagonalization argument.
Diagonalization. For all sets X and Y with a function f:X×X→Y and a function δ:Y→Y with no fixed point, there exists at least one function g:X→Y such that there exists no k such that f(k)=g.
Proof. Let g(x)=δ(f(x,x)). For any k, g=f(k), since g(k)=f(k)(k).
The Diagonalization Trilemma with Exposition
Diagonalization. Let’s say you have an “evaluation” function f:X×X→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 δ:Y→Y with no fixed point. You can think of δ as a “give me something different” function: it changes every y into a different y.
Then there exists a function g:X→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 δ(f(x)(x)). For any k, g=f(k), since g(k)=f(k)(k). ■
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)=f(234)(234). That’s because g(234) does equal δ(f(234)(234)), which is different from f(234)(234) because δ 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 Gö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
Once you place it, you’ll see an abstract representation of the MPU 6050 with all its pins.
To figure out what these pins do, you’ll need to take a look at the part’s datasheet (Google is your friend). These tend to be long and verbose; the MPU6050 datasheet is more than 50 pages long. A good place to start is by looking at the pin out table.
This table describes the purpose of each of the pins on the bottom of the MPU6050. Some of these descriptions are self-explanatory; pin 18 is labelled “GND” and is supposed to be connected to ground. We can start by connecting that one in our schematic editor.
Here, we can see that pin 10 (REGOUT) is supposed to be connected to a 0.1uF capacitor and then to GND. Let’s add that to the schematic (recall that 0.1uF = 100nF).
AUX_DA and AUX_CL are another I2C pair for “connecting external sensors,” which we don’t have. We shouldn’t leave them unconnected, since I2C lines need to be kept at 3.3v by default, so we connect them to our 3.3v power through another pair of 4.7k pull-up resistors.
INT is an interrupt pin; the gyroscope can activate it to quickly signal something like “this chip is in free-fall.” We won’t use it.
We therefore choose not to connect EP.
Congratulations! You’ve set up your first chip.
We’ll grab one of these 1117 chips. Digging through its datasheet, we find this wonderful typical operating circuit in Chinese.
We copy that diagram into our schematic as follows.
It’s pretty simple to connect in the schematic. Make sure you put the VBAT connection on the + side of your battery, and the GND connection for the - side.
Phew! That’s a lot of pins to connect.
According to the top of the diagram, VBAT should be connected directly to the battery.
The schematic can be deceiving; although these look like four separate circuits, the V3.3s and GNDs all link together. This is why it doesn’t matter that the 4.7uF capacitor is only graphically attached to the bottom pins; it’s electrically connected to all of them. [3]
According to the STM32F302 datasheet, NRST is active low. This means that the pin should usually be high (at 3.3v). When we push the reset button, it should temporarily drop to ground to restart the board. We’ll do that with the following circuit.
SW1 is a generic pushbutton; when you push, it connects the 1/2 side to the 3/4 side. By default, NRST is held to 3.3v, since it’s connected to V3.3 through that 47k resistor. When SW1 is held, NRST is also connected to ground through a 10k resistor. Since the ground resistor is smaller, the voltage on NRST jumps closer to ground. This gadget is called a 
So usually Boot0 should usually be low, corresponding to main flash memory, but when we hold a button, we’ll set Boot0 high to boot from system memory instead. We won’t worry about the third chart entry, embedded SRAM, for now.
If we want to boot from system memory, we’ll hold down the SW2 button during boot up.
None of our microcontroller pins are labelled “SWDIO”, but we can reference this handy table to see which pin handles that function. In our case, it looks like the PA13 pin handles SWDIO.
We also need to attach SWDCLK, SWO, and NRST. First we’ll put little tags on the relevant pins:
Then we’ll grab a 2x5 pin header with 1.27mm spacing and attach those tags to it, along with power and ground.
We now have the basics of the microcontroller fully configured. All that’s left is to attach inputs and outputs for the IMU and servos.
We connect PA9 and PA10 to the IMU with the same SDA and SCL tags we used back then.
And looking at TIM2, we’re in luck! It can drive four independent PWM channels for our four servos.
Checking the pinout table, we see that TIM2_CH1 corresponds to PA0, TIM2_CH2 to PA1, and so forth.
We connect some labels as usual.
Our servos have a 3x1 female connector with 2.54mm spaced pins. They accept power, ground, and signal on those three lines, and power in the middle. We grab four corresponding male headers from the parts library, and GND, VBAT, and each signal line.
That’s all; the finished schematic should look like this.
A word of congratulations: designing schematics is probably the hardest part of this project, especially for someone with programming background. And designing your first schematic is much harder than your second: when you design your second schematic, you’ll already understand LDOs, SWD, timers, pull-up resistors, etc. Now you’re over the hump!