A Computability Proof of Gödel’s First Incompleteness Theorem
medium.com
medium.com
The way it all sort of works is:
1. A mathematical theory is called consistent if there is some model of it, a self-consistent set M of all mathematical objects for that theory. For example, a model of the natural numbers would be {0,1,2,...}, but there are other models too.
2. By some parsing method, we can encode every "first-order definable" (akin to "computable") statement and function as an element of M itself. Let (M -> M) denote the set of definable functions; by picking out an element nil from M, we can think of such a function as being a boolean-valued function, where like Lisp we say nil is the unique false value, everything else is truthy.
3. Since everything is encodable, there is a function print : (M -> M) -> M and a left inverse read : M -> (M -> M). (I imagine parse errors just return the constant-nil function.)
4. We can define lots of useful functions, like not, where not(nil) = 1 and not(x) = nil for all x != nil, where 1 is anything that's not nil. Another is iff(x,y) = (not(x) == not(y)), that is, whether both inputs are truthy in the same way.
5. An interesting function you can define is provable : (M -> M) -> M, which takes a function f and returns whether or not M contains a proof that f is non-nil for all inputs. This takes a bit of implementation, but it's not too hard.
6. Now to set up diagonalization. Define f : M -> M by
f(x) = print(lambda _ -> not(provable(read(x)))
iff (forall z -> read(x)(z))).
g(nil) = not(provable(g)) iff (forall z -> g(z)).
The way this is summarized is: either the theory is inconsistent (there is no model) or it is incomplete (the provable function can't prove all true things).
The way this ends up working in the mathematical landscape is that, if there is any model at all, there is more than one. (Something is provable if and only if it is true in all models -- Godel.)
No, not really. I mean yes, it is, if you're a mathematician. But no, it's not, if you're someone who needs to have binary encoding explained to them, which the original article attempts to do. (And if you're a mathematician you don't need Godel's theorem explained to you at all.)
Here's how I would go on with the exposition:
A formal proof is a sequence of strings, each of which can be derived from the set of strings that precede it in the sequence according to a set of rules. There is a particular set of rules called Peano arithmetic (because they were invented by a guy named Peano) that are so far mankind's best attempt at encoding the fundamental properties of the natural numbers. Ideally, a string in a formal proof under the Peano rules should correspond to a true statement about numbers, and conversely, every true statement about numbers should have a corresponding proof. But it turns out that both of these cannot be simultaneously true. In particular, we can prove that if all strings in proofs correspond to true statements about numbers, then there must be true statements about numbers that cannot appear in proofs.
Godel's original proof involved constructing a number N whose corresponding string essentially means "The string corresponding to N has no proof." Describing how N is constructed is tricky, but since we know about the halting problem we can prove this result in a much more straightforward way: suppose that we could prove any true statement about numbers. Consider an arbitrary program P. That program can be encoded as a number N. So the statement "The program corresponding to the number N halts" is a claim about numbers. It is either true or false. If it is true, then by our assumption we can prove it, and if it is false then its negation is true and we can prove that. So now all we have to do to solve the halting problem is to systematically search through the space of all possible proofs until we find a proof either of "the program corresponding to the number N halts" or its negation, at which point we will know whether or not P halts, and so we have solved the halting problem. But we already know that we can't solve the halting problem, so our assumption that all true statements about numbers can be proven must be false.
I was responding specifically to
> All the rest, all the heavy lifting, is just cranking out the tedious details of what those mathematical operations actually are, but none of that is necessary in order to understand the core idea of the proof.
The thing I'm taking issue with is calling parsing the core idea, with the rest "just"[1] being tedious details, where, as someone who has done some PL implementations, the parsing seems to me to be the tedious part. It's an important idea that's essential to the proof, but, again, that's like saying parsing is the core problem in writing a compiler (or that writing read is the core problem in implementing a Lisp interpreter). This is not exactly evidence of any kind, but notice your whole final paragraph is a diagonalization argument, and it is longer than the first paragraph of your exposition, which quickly explains how strings can represent logical statements and proofs.
Maybe this is a synthesis: the core idea is that you can write an interpreter that takes an encoding of a logical statement and returns whether or not it is provable. Since the interpreter is itself a logical statement, you can apply a diagonalization argument to produce a true statement that refutes its own provability. (When I say the core idea is the diagonalization, I mean both the interpreter and the fixed point finding. When you say the core idea is encoding, I suspect you might mean more the interpreter than how your comment reads to me.)
By the way, with the halting problem argument, it seems like if you're very careful you can write out an explicit Godel sentence, like what the Lawvere fixed point theorem would provide. I'm sort of curious what it would look like, rather than your recipe for how to construct it. (I also wonder what the shortest Godel sentence is. But only as much as I wonder what the shortest quines are.)
> "The string corresponding to N has no proof"
Small correction: it's that "N being true is equivalent to N having no proof." If N is false, then it is provable (bad), so if things are consistent it must be true, hence unprovable. It's interesting that N is a true statement.
[1] I have a banned words list in my office; one entry is "just" because of just what it lets you sweep under the rug.
From the layman's perspective the question then is: WHY is Peano Arithmetic incomplete? What does it add to the mix that makes it categorically different from those other axiom systems?
ENCODING power is the answer; that is, the expressive capacities of PA versus these other systems. In particular, PA is expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization/self-reference/Lawvere (depending on your background) are readily understood.
So to my mind, the layman would be more puzzled by the differing expressive powers of formal languages, and why exactly they lead to differences in provability. E.g., is the defineability of exponentiation a prerequisite to linguistic self-encoding? What's the relationship between quantifier elimination and self-reference? To what extent does a robust concept of 'infinity' play a role. Etc., etc.
I think what you mean by "encoding" is what I mean by "being able to write an interpreter." It's not hard to encode mathematical statements as real numbers in the axioms of a real closed field, which someone outside the theory is easily able to decode. However, the fact the theory is complete implies there is no way to write an interpreter within the theory.
There are other kinds of interpreters you might be interested in. For example, one that determines absolute truth of a statement, that is, the truth of the statement in the "Platonic universe," whether or not it is provable. You can still apply the usual kind of argument, if such an interpreter existed, to generate a sentence that is true iff it is false.
I imagine a heuristic sort of issue is that to write such an interpreter you need to be able to encode environments (like in a Scheme interpreter), but the set of possible environments is too big in a Russell's paradox sort of way. In model theory, they call such a function, when restricted to a particular model, a truth term.
> expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization [...] are readily understood
I don't really understand you here: a diagonalization/Lawvere-like argument is how the Gödel sentence is constructed in the first place.
Before picking up this book as an undergrad in pure maths, I still had romantic ideas about a separate platonic universe and the divine authority of mathematics to explain all human thought.
This book, along with studying the various geometries, each with a different choice of axioms not necessarily based in ‘reality’, destroyed the majority of that romance.
Mathematicians of the past sought perfection for the glory of God. Now we have the opportunity to give credit where it’s due: to our fellow human beings, many of whom devoted their lives to the craft of mathematics.
"Do not be overly righteous, and do not make yourself too wise." (Ecclesiastes 7:16)
"There is no distinction, for all have sinned and fall short of the glory of God, and are justified freely by His grace through the redemption that is in Christ Jesus." (Romans 3:22-23)
I wonder whether Gödel would have pursued the Proof if he did not believe in an omnipotent god.
Cantor believed that he had been chosen as a messenger by God to be the recipient of what was to become set theory.
[1] http://users.utu.fi/jkari/automata/fullnotes.pdf#page=134
[2] https://www.adobe.com/content/dam/acom/en/devnet/acrobat/pdf...
It is easiest to think about in terms of set theory, but it is possible to formalize it in a fragment of second-order arithmetic that is conservative over PA (and this conservativity is provable in PA itself). The beauty of this proof is that it first establishes semantic incompleteness without formalizing a proof system; the connection to syntactic incompleteness only uses the Completeness Theorem, which is of independent interest.
Therefore, a more general proof is needed to prove incompleteness. Such a proof can be found here:
It's hard to explain, because the idea of encoding statements about a system in terms of the system itself is weird if you haven't seen it before.
That said it can be fully covered in a single semester of undergraduate study, so its not that hard. There are many theorems that couldn't be fully proved in a semester.
“My nose will get longer”
[1] https://www.goodreads.com/book/show/1556746.Computability_an...
How can a string not be decidable?! Just search for the string in the set. It is either there, or not there.
What an I missing?
Infinity breaks a lot of things. Infinity isn't even real. So I'm not sure this counts. It seems like the article would have mentioned infinity if that were the reason for the claim. It seems like Enumeration fails for an infinite set too.
A lot of these ideas don’t require any actual “realized” infinity, however. For instance, there are infinitely many natural numbers, but natural numbers themselves are still finite. You can write a program that prints every number at some time in the nearby future (ignoring physical constraints), even though there is no point in time where it will have printed all numbers.
If you want to take away infinity, you have to draw an arbitrary upper bound somewhere, since unbounded things are infinite. Drawing that line is fairly arbitrary since there is no reason why things should no longer work if you add just one more.
Off topic: Still, you'd run out of matter in the universe (that you could use for ink), before you wrote down a finite amount of numbers while ever reaching a percentage of infinity. That's how unreal infinity is in my mind.
I know the concept of infinity is useful in math, and in this incompleteness theorem, it seems like infinity is the very reason not all truths are provable. But I thought Godel's incompleteness theorem would apply to physical reality, but since infinity doesn't exist in physical reality, I'm not sure the incompleteness theorem would apply to physical reality. Hmmm
Also, didn't Godel show his theorem to be informally true by stating, "This sentence is inprovably true."? There was no infinity invoked in that sentence.
If there were only a finite number of such "True, but unprovable using your current proof rules" sentences, then you could simply add those sentences to your list of proof rules and there would be nothing "True, but unprovable" anymore. For Gödel's theorem to work, you need at least an infinite supply of those kinds of sentences.
Also here there's no need to actually write down all of them exhaustively. It's just important to be able to find "yet another one" whenever you would like to, which requires an inexhaustible supply.
But this is how you can stress the theorem. I know it will take a long time, so consider a universe where only 1000 bits of matter actually exist, then try to use the theorem and you won't have enough ink to even hold the theorem, and sets in memory. It's the same for our universe, just with more bits.
"you could simply add those sentences to your list of proof rules " Thanks, for responding. Do you mean axioms? I don't understand why that would be a solution. I'll have to read Godel again.
Philosophically, I think it's also more interesting that Gödel's theorem would continue to produce such sentences, regardless of how large our universe happens to be. You could never have a universe that is so big that it could contain all Gödel sentences, even if our universe were bigger. This is a much more fundamental limitation.
Gödel's theorem gives you a sentence S where you can prove neither S nor its negation from the current axioms P. Of course, if you then add S (or its negation) as an axiom, then you CAN prove it. But then Gödel's theorem will just give you another sentence S', ad infinitum. You can never win this game.