In the previous blog post in this series, we looked at Gödel’s First Incompleteness Theorem, and came to the amazing conclusion that we can’t compute certain kinds of functions in formal systems (like Javascript). Specifically, we looked at a special function, \(\bar{f}(x)\), which turned out to be non-computable. In case we forgot, the first incompleteness theorem states that:
Any consistent formal system \(S\) within which a “certain amount of elementary arithmetic” can be carried out is incomplete; i.e., there are statements of the language of \(S\) which can neither be proved nor disproved in \(S\).
Keen readers already pointed out that we didn’t exactly prove it. In fact, we only proved that the set of computable functions is countably infinite, whereas the set of non-computable functions is uncountably infinite. So in this post, we’ll completely finalize the proof of the first incompleteness theorem and we’ll try to see how it implies the second incompleteness theorem, which states that:
Any consistent formal system \(S\) within which a “certain amount of elementary arithmetic” can be carried out cannot prove its own consistency.
Fair warning: this post is more technically-rigorous than the previous one.
Finishing the First Proof
Even though we’ve been working with Javascript, we’ve only been looking at functions that take in positive integers and return either a 0 or a 1. For example:
[javascript]
function isOdd(x) {
return (x % 2);
}
[/javascript]
But Javascript can return all kinds of things: strings, objects, booleans, other functions, etc. It’s a fairly expressive language. Let’s define \(\bar{f}\)-statements as the strings that look like:
[shell]
“f-bar(x) is equal to y”
[/shell]
Where x is a positive integer and y is a 0 or a 1. For example, here’s a JS program that returns an \(\bar{f}\)-statement:
[javascript]
function fBarExample() {
return ‘f-bar(145) is equal to 0’;
}
[/javascript]
It’s easy to see that \(\bar{f}\)-statements will either be “true” or “false” — in the above case, if \(\bar{f}(145) = 0\) then the \(\bar{f}\)-statement printed out by fBarExample is true, but if \(\bar{f}(145) \neq 0\) then the statement is false. I want to reiterate that there’s no magic happening here; like we’ve seen in my previous essay, \(\bar{f}(x)\) is well-defined for every positive integer \(x\) so, at the end of the day, any \(\bar{f}\)-statement will either be “true” or “false.”
So far, so good, but here comes the twist. I want you, dear reader, to write a program that returns whether or not an \(\bar{f}\)-statement is true or false. In other words, fill in the blanks:
[javascript]
function verifyStatement(fbarStatement) {
// maybe we parse the statement?
// we get the x part and the y part
// and do some stuff with it?
// lots of complicated math stuff
if (something) {
return true
} else {
return false
}
}
[/javascript]
But it’s here we run into a contradiction and finally fully prove the First Theorem. To complete this function, we need to have some way of computing \(\bar{f}(x)\). But in the previous essay, we concluded that \(\bar{f}(x)\) cannot be computed, so the function verifyStatement cannot be written. In other words, we just came up with a statement we know has a true or false value that we simply cannot prove nor disprove. Q.E.D.
Introducing Löb’s Theorem
To help us prove Gödel’s Second Incompleteness Theorem, we’re going to use a lesser-known theorem — Löb’s Theorem — which will help us intuitively understand why a sufficiently-complex formal system cannot prove its own consistency. So let’s get started. First, we introduce JS (Javascript), the cool kid on the block: ?. JS makes statements about all kinds of things, like dates, numbers, or strings:
Whenever JS says something, there is an underlying computation that took place. In formal terms, we would say that JS proves the statement. So, the idea is that we have some program:
[javascript]
function hello() {
return “Hello, world!”
}
[/javascript]
That leads to JS actually saying “Hello, world!”
This is actually a pretty nice property. Like we saw in the previous post, JS can say anything that it can compute. It can’t say anything about non-computable things (like \(\bar{f}(x)\)), but whenever it says anything about something computable, it always turns out to be true.
As it turns, out, JS can talk about itself.
Originally, Gödel devised an “arithmetic encoding” to get a formal system (like Peano Arithmetic) to talk about itself. But with Javascript, we don’t need such a hack. In fact, we already have the eval() function as part of the language itself. We can write Javascript within a Javascript program. But, if we need to, we can ever write a JS parser inside a JS program. We can check program length, check for syntax errors, investigate arbitrary bits, verify output, and so on.
Löb’s Sentence & Löb’s Hypothesis
They key to Löb’s Theorem is Löb’s Sentence, \(L\). It states: if a proof of \(L\) exists, then \(C\). This is how we would express the sentence:
\\
\\
\\
\\
\end{cases}\)?? \(\Rightarrow\) ⚡
Confused? Here’s what the sentence might sound like in English:
If the result of substituting “If the result of substituting x for ‘x’ in x is provable in JS, then C” for ‘x’ in “If the result of substituting x for ‘x’ in x is provable in JS, then C” is provable in JS, then C.
To unpack \(L\), we just need to refer to its construction:
This expansion is less daunting than it might seem. Simply put, proving the box is the same thing as proving what’s inside the box. Next, we introduce Löb’s Hypothesis:
Löb’s Hypothesis is a claim of soundness — it asserts that “A proof of \(C\) implies \(C\).”
Axioms and Rules
From now on, to conserve on space and make the proof easier to follow, we’ll say \(P_{JS}(X)\) when Javascript proves (has a program for) \(X\). Apart from \(L\) and the hypothesis, here are the tools we’ll need to finish the proof:
| \(P_{JS}(?) \Rightarrow P_{JS}(P_{JS}(?))\) | A1. If JS proves \(X\), JS proves that “JS proves \(X\)“ |
| \(P_{JS}(P_{JS}(?) \rightarrow P_{JS}(P_{JS}(?)))\) | A2. JS proves A1. |
| \(P_{JS}(?) + P_{JS}(?\blacktriangleright⚪) \Rightarrow P_{JS}(⚪)\) | MP. Modus ponens. |
| \(P_{JS}(P_{JS}(?\blacktriangleright⚪) \rightarrow (P_{JS}(?) \rightarrow P_{JS}(⚪)))\) | A3. JS proves that JS obeys MP. |
| \(P_{JS}(?\blacktriangleright⚪) + P_{JS}(⚪\blacktriangleright?) \Rightarrow P_{JS}(?\blacktriangleright?)\) | B1. MP is transitive. |
| \(P_{JS}(?\blacktriangleright⚪) + P_{JS}(?\blacktriangleright(⚪\blacktriangleright?)) \Rightarrow P_{JS}(?\blacktriangleright?)\) | B2. |
Proving Löb’s Theorem
| 1. | \(P_{JS}(P_{JS}(?)\leftrightarrow P_{JS}(P_{JS}(?)\rightarrow ⚡))\) | Unpacking \(L\), same as above. |
| 2. | \(P_{JS}(P_{JS}(⚡)\rightarrow ⚡)\) | Löb’s Hypothesis. |
| 3. | \(P_{JS}(P_{JS}(P_{JS}(\text{?})\rightarrow\text{⚡})\rightarrow(P_{JS}(P_{JS}(\text{?}))\rightarrow P_{JS}(\text{⚡})))\) | (A3) |
| 4. | \(P_{JS}(P_{JS}(\text{?})\rightarrow(P_{JS}(P_{JS}(\text{?}))\rightarrow P_{JS}(\text{⚡})))\) | (1, 3, B1) |
| 5. | \(P_{JS}(P_{JS}(\text{?})\rightarrow P_{JS}(P_{JS}(\text{?})))\) | (A2) |
| 6. | \(P_{JS}(P_{JS}(\text{?})\rightarrow P_{JS}(\text{⚡}))\) | (5, 4, B2) |
| 7. | \(P_{JS}(P_{JS}(\text{?})\rightarrow \text{⚡})\) | (6, 2, B1) |
| 8. | \(P_{JS}(P_{JS}(P_{JS}(\text{?})\rightarrow \text{⚡}))\) | (7, A1) |
| 9. | \(P_{JS}(P_{JS}(\text{?}))\) | (1, 8, MP) |
| 10. | \(P_{JS}(\text{⚡})\) | (9, 7, MP) |
| Q.E.D. |
In other words, if we claim that Javascript proves “If Javascript proves ‘\(C\)‘, then \(C\),” we can get \(C\) out of thin air.
Back to Gödel
Löb’s Theorem takes us to Gödel’s doorstep. Suppose I find a proof (i.e. write a program) in Javascript for “Javascript proves that 0 doesn’t equal 1” — we could write this as
$$P_{JS}(\neg P_{JS}(0=1))$$
After disjunction introduction and rearranging the negation, we end up with
$$P_{JS}(P_{JS}(0=1)\rightarrow (0=1))$$
And after applying Löb’s Theorem, we’re left with
$$P_{JS}(0=1)$$
Oops, it looks like JS just proved that “0=1” — but this cannot be; zero doesn’t equal one and Javascript is consistent, following basic rules of logic and arithmetic. Therefore, no consistent system can prove its own consistency. In Javascript, no computer program will ever assert “0=1” as being true, but we can never prove that consistency within Javascript itself. Q.E.D.
That was fun! To reiterate, what we proved is that JS (or any interesting-enough theory or system) can’t prove anything interesting about itself. You might be tempted to think “well, shucks, that makes formal systems absolutely useless..” — it doesn’t! What we can (and do) do is prove things about systems in other, larger, systems. You might be wondering why can’t JS prove things about itself? Obviously, we proved that it can’t, but there must be some underlying reason why it can’t. And there are several, but the most salient is the halting problem. It can be shown that to prove interesting things about itself, JS would need to solve the halting problem — which is impossible.
Parting Words
As a book-end refresher, here’s what we learned in these two blog posts:
- We discovered \(\bar{f}(x)\), a non-computable function. This helped us prove that the set of computable functions is much smaller than the set of all functions.
- We showed that even though the statement
f-bar(x) is equal to yhas a truth-value, we cannot derive it in JS. Thus, JS is incomplete. - We showed that if JS proves “If Javascript proves ‘\(C\)‘, then \(C\),” then it proves \(C\).
- We claimed that a proof exists, in JS, that says “Javascript proves that ‘0≠1’.”
- But by applying Löb’s theorem, we also proved that “0=1” and ended up with an inconsistent system.
- But we know JS is consistent, we just cannot prove that fact within JS itself.
Acknowledgements
It took me a while to write this post and I wanted to be as simple as I possibly can while trying to show an interesting way of thinking about it. Please let me know what you think in the comments below! If there are any mistakes (this was my first exposure to Löb’s Theorem), please don’t hesitate to point them out!
If you couldn’t follow along, there’s an awesome proof provided by Scott Aaronson on his blog (using Rosser’s Theorem), but I always thought it was a bit hand-wavy. The proof of Lob’s Theorem was heavily influenced by Eliezer Yudkowsky’s Cartoon Guide to Löb’s Theorem. Finally, I also used Patrick LaVictoire’s An Introduction to Löb’s Theorem in MIRI Research and Unsolvable Problems in Logic to guide me along and help me make the final leap from Löb to Gödel’s Second Incompleteness Theorem.