How Gödel's proof works (2020)
quantamagazine.org
quantamagazine.org
It really feels to me as if the distinctions between countable vs uncountable; rational vs irrational; discrete vs continuous; all represent the boundary between physics and mathematics – an idea I wish I could elaborate more precisely, but for me stands only on a shred of intuition.
I've been interested lately in Stephen Wolfram's and Scott Aaronson's writings on related ideas.
Aaronson on Gödel, Turing, and Friends: https://www.scottaaronson.com/democritus/lec3.html
Wolfram on computational irreducibility and equivalence: https://www.wolframscience.com/nks/chap-12--the-principle-of...
I do agree that Godel’s incompleteness is effectively a statement about integers. As is our model of computation (lambda calculus and church-Turing thesis)
“These include providing a theory of information underlying classical and quantum information; generalising the theory of computation to include all physical transformations; unifying formal statements of conservation laws with the stronger operational ones (such as the ruling-out of perpetual motion machines); expressing the principles of testability and of the computability of nature (currently deemed methodological and metaphysical respectively) as laws of physics; allowing exact statements of emergent laws (such as the second law of thermodynamics); and expressing certain apparently anthropocentric attributes such as knowledge in physical terms.”
No matter what you choose to believe about the metaphysics of math and logic (i.e. an opinion on platonism) we end up in practice with limitations about _how_ we can know mathematical and logical truths, and there I feel we end up with something warm and vibrant and human, and not at all the cold and precise thing that logic is sometimes presented as.
A real number is what happens when you reach the end of an infinitely long light ray — the sum of such a journey. We don’t experience things like that.
Yet things like spinors seem to accurately model particle physics, hinting that there’s more to the story.
If you’re looking for a generalisation, these are all instances of Lawvere’s Fixed Point Theorem, although my grasp of category theory is nowhere near enough for me to claim to have any insight into this abstraction.
Here are a couple of thoughts on Godel's incompleteness theorem that helped me get there.
First, a description of the idea; consider the following two statements:
"There exists a formula with Godel number M that has the property that neither the formula nor its negation has a proof."
"Oh, by the way. The Godel number of the above formula is M."
"M" in the above is an actual number. In the first statement, one has an arithmetic expression (i.e., "3 + 4*5 + 12^100000 + ...") that is short but that evaluates to a really large number.
After developing the idea of mapping formulas and proofs of first-order logic to integers, Godel needed to use his new tool to come up with some way to express self reference. (The formula above has to have an embedded arithmetic expression "M" that unwraps and and evaluates to the Godel number of the entire formula.)
Godel devised what we would today recognize as exactly the Y combinator, expressed in first order arithmetic.
This was a shocking realization when it dawned on me, and it enabled me to gain an insight to the magnificent subtlety of Godel's mind.
I am personally comfortable with lisp, functions as first-class objects, lambda calculus, etc., as is certainly the case for many Hacker News readers.
So, at least for me, the above connection helped an awful lot to really understand the heart of Godel's insight.
Give the large number of successes that mathematics lead to, it only made sense that they would try to encode more things as numbers, including a more general method of translating _all words_ to numbers, using the most straight forward encoding they could think of -- just having the letters stand in for the numbers that the _same letters_ stood for when they were doing math.
It didn't develop this way in reality of course, but you could probably draw a fairly straight line of logical developments from numerology to word2vec and LLMs.
2. Thus we can then talk about properties of expressions as being properties of number. We can make statements which say things like "X has a proof", "Y can be proven false", "Z has no proof", where X, Y and Z are embedded numbers (literals). These literals themselves are expressed symbolically in a way that is susceptible to Gödel numbering. These entire statements are Gödel-encoded and so have numbers; e.g. the Gödel number of "X has a proof" for some given X is some other number W.
3. A Gödel sentence can be constructed which says that "G cannot be proven true", where G is the Gödel number of that sentence itself: in effect, the sentence says "I cannot be proven". The sentence contains a literal G, or perhaps some expression which calculates G. When the Gödel number of the sentence is calculated, it turns out to be G.
This is a bit like "This sentence is false", but different. It's not a direct contradiction.
"I cannot be proven true" can be taken to be true, without contradiction. The sentence says it has no proof and by golly, none can be found.
That allows us to regard it as true and add it as a new axiom.
That shows that our system wasn't complete; there are truths that can be expressed in its symbols that have to be treated as new postulates.
> Rahul #97: No, because the other point is that whether a spectral gap goes to zero as the lattice size goes to infinity is the kind of thing that real condensed-matter physicists and quantum field theorists ask all the time. It’s something they accept every day as a good mathematical idealization for what they care about. So it’s worthwhile to know that their problem secretly contains the halting problem—that for large enough constant d, there can never be a clean algorithmic criterion to tell you which nearest-neighbor qudit Hamiltonians are gapped and which are gapless.
https://scottaaronson.blog/?p=2586#comment-975416
If I read this he's clearly implying the spectral gaps problem is done by reduction to the halting problem.
(Edit, in the blog entry he explains: "Cubitt et al.’s theorem now says the following: for some fixed, constant local dimension d, there is no algorithm that takes as input the local Hamiltonian h (say, as a d2×d2 matrix of algebraic numbers), and that decides whether the material is gapped or gapless. Indeed, you can reduce the halting problem to that problem, in such a way that the material will be gapped if your Turing machine halts, or gapless if it runs forever.")
That is, we know that the integers have cardinality of “aleph null”, the smallest infinity. And we know how to construct the “next” level of infinity using something analogous to power sets. Call this “aleph one”.
Now the hypothesis: the cardinality of the real numbers is equal to aleph one.
It is known that we can never prove that hypothesis one way or the other. The US mathematician Paul Cohen established this in the 1960s.
There are probably egregious errors in my telling of this, but it could be a prompt for further reading.
For systems we actually use, such as ZFC or PA, we know a number of actually "meaningful" examples such as the Continuum Hypothesis, which is independent of ZFC. But of course, you can always just add this hypothesis (or its negation) as an axiom.
Gödel's theorem has to rely on self-reference because we can't really give a "natural" example when we're not actually looking at a specific system, but trying to say something about all possible systems.
Super fun stuff, though I'm not going to pretend I understand all of this (I mostly just gleam this stuff from what mathematicians say on Numberphile channel).
Take the halting problem for example. Imagine two algorithms for determining if a program halts. One always returns true, the other always returns false. For every single program, one of them will be the correct solver, but clearly neither of them is the correct solver for every single program.
Therefore the counter-example necessarily has to depend on the specific details of the algorithm that claims to be the universal halting decider.
Strictly speaking, there isn't an universal counter-example, since it changes depending on what the algorithm is. There are just instructions on how you can always make one, no matter what the algorithm is.
https://plato.stanford.edu/entries/goedel-incompleteness/#Co...
It ends with an interesting point about the continuum hypothesis:
> Sometimes Paul Cohen’s celebrated result that the Continuum Hypothesis (CH) is independent of ZFC (Cohen 1963, 1964; see the entry on independence and large cardinals). However, this case is very different. In all the above independence results the relevant statements are still theorems of mathematics, taken as shown to be true (the last case, which requires large cardinal axioms that go beyond ZFC, is more controversial; still, at least many set-theoreticians find such axioms plausible). And with the first incompleteness theorem itself, the truth of the unprovable statement easily follows, given that the assumption of the consistency of the system is indeed correct. However, in the case of Cohen’s result, there is absolutely no indication whether CH should be considered true, false, or perhaps lacking a truth-value.
> I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?
At any rate I'd definitely be interested in to know what is such a major inaccuracy presented that the entire video can be dismissed on that basis.
Another inaccuracy: In 8:42 he says Russell pointed out a "problem in Cantor's set theory". But Cantor's theory wasn't even axiomatized, and Russell didn't talk about Cantor's theory, but about Frege's Basic Laws of Arithmetic, which contained an inconsistency.
The thing I was pointing at (grain of salt) is basically the same as Gell-Mann amnesia[1]: Why should you trust someone in a subject you don't know anything about, when you don't overly trust him in topics where you do know something about? The trust level should arguably be the same in both subjects.
Your second point also seems like a very minor nitpick. Clearly, set theory is inconsistent if you don't impose any restrictions on what kinds of set can be formed (something that Cantor to my knowledge didn't do), which is what Russell's paradox showed. The fact that they used Frege's formalisation for setting up the paradox doesn't seem particularly relevant to me.
She was such a great math prof. Weird how one person can make you love a subject even after years of not so great teachers.
Edit: thanks for the recommendations, but I have several books that discuss the proof. I was just asking if GEB gets to it.
"I am a Strange Loop" elaborates a bit on the parts which may have been confusingly explained, notably both in the proof of the theorem and in the author's AI philosophy.
> Analogy is the core of all thinking. This is the simple but unorthodox premise that Pulitzer Prize–winning author Douglas Hofstadter and French psychologist Emmanuel Sander defend in their new work. Hofstadter has been grappling with the mysteries of human thought for over thirty years. Now, with his trademark wit and special talent for making complex ideas vivid, he has partnered with Sander to put forth a highly novel perspective on cognition. We are constantly faced with a swirling and intermingling multitude of ill-defined situations. Our brain’s job is to try to make sense of this unpredictable, swarming chaos of stimuli. How does it do so? The ceaseless hail of input triggers analogies galore, helping us to pinpoint the essence of what is going on. Often this means the spontaneous evocation of words, sometimes idioms, sometimes the triggering of nameless, long-buried memories. Why did two-year-old Camille proudly exclaim, “I undressed the banana!”? Why do people who hear a story often blurt out, “Exactly the same thing happened to me!” when it was a completely different event? How do we recognize an aggressive driver from a split-second glance in our rearview mirror? What in a friend’s remark triggers the offhand reply, “That’s just sour grapes”? What did Albert Einstein see that made him suspect that light consists of particles when a century of research had driven the final nail in the coffin of that long-dead idea? The answer to all these questions, of course, is analogy-making—the meat and potatoes, the heart and soul, the fuel and fire, the gist and the crux, the lifeblood and the wellsprings of thought. Analogy-making, far from happening at rare intervals, occurs at all moments, defining thinking from top to toe, from the tiniest and most fleeting thoughts to the most creative scientific insights. Like Gödel, Escher, Bach before it, Surfaces and Essences will profoundly enrich our understanding of our own minds. By plunging the reader into an extraordinary variety of colorful situations involving language, thought, and memory, by revealing bit by bit the constantly churning cognitive mechanisms normally completely hidden from view, and by discovering in them one central, invariant core—the incessant, unconscious quest for strong analogical links to past experiences—this book puts forth a radical and deeply surprising new vision of the act of thinking.
As a consequence (via Rice's theorem [1]), all nontrivial semantic properties of computer programs are undecidable. That is, there's no algorithm that can answer "does program x have property y?" for all programs, although obviously it's possible to prove propositions about many individual programs.
Because Turing completeness is a fairly low bar to clear, there are infamously a lot of systems that were not designed (or indeed designed not) to be Turing-complete but nevertheless turned out to be so [2]. As such, things like the Java type system is undecidable – in principle there exist Java programs that the compiler can neither reject nor accept.
[1] https://en.wikipedia.org/wiki/Rice%27s_theorem
[2] https://beza1e1.tuxen.de/articles/accidentally_turing_comple...
By now there are numerous others; this is one of the earliest & best known examples in mathematics.
It's also my understanding that Godel did not like publishing. Has his unpublished work ever been combed through and published in some form? Did he primarily write in English or German? Who has his personal papers?
Another question, do you use Cantor-style diagonalization for the fixed-point theorem? Apparently this is the case for the standard proof of incompleteness, as explained here, though this paper goes over my head: https://haimgaifman.files.wordpress.com/2016/07/22odel-to-kl...
The reason why I'm asking is that Cantor used diagonalization in his famous "diagonal argument" for the real numbers being uncountable. Some people found this argument unconvincing, because it relied on perhaps questionable assumptions, like the decimal representation of real numbers and that different decimal representations must denote a different real number. But if the diagonal argument (or his earlier powerset argument) could be formalized and checked with Coq, doubts would presumably be removed.
If you think Kleene's recursion theorem and Cantor's diagonalization are the same sort of argument, then I'd say yes.
I don't know if people historically had an issue with Cantor's argument or not. Certainly the modern presentation with decimals can be dicey if you are not careful because, as you note, some real numbers have two representations as decimals, one with repeating 9's and another with repeating 0's. But this issue can be avoided so long as you are careful. e.g convert all non-5's to 5's and convert 5's to 6's, thus staying far away from the dangerous 0/9 zone of digits. The constructed decimal sequence only has 5's and 6's and thus is a real number with a unique decimal representation.
There is no problem with Cantor's argument, and it can easily be formalized. It would be a reasonable exercise to do at some point in an introductory course for proof assistants.
Any takes on this ? Spreads doubts over godels proofs
What doubt does it spread?
What’s the key take away?
Is it just a crank video?
A famous proof published in 1931 that has had much discussion and testing is debunked and disproved on YouTube!
No way of telling except to click through and watch a 15 minute video that isn’t even vouched for or elaborated on by the commenter posting it.
I think moreso it just shows that Godel's proof is not as significant or as relevant as many people make it out to be, and on the whole I'd say I agree with that.
Chapter 7 of my thesis <https://r6.ca/thesis.pdf> has some more comments. With a bit more care using Prop/Set maybe one could compute explicitly what these Goedel sentences are (similar to <https://web.archive.org/web/20160528092209/http://tachyos.or...>). Maybe using Robinson Q instead of Hodel's obscure NN system would have been better, or maybe with a bit more abstraction it would be easier to apply the proof to other axioms systems, such as ZF, which don't use the same language that PA does. And maybe making sure the Second Incompleteness could follow more easily would be good (which has since been formalized elsewhere).
The strengthened liar paradox discussed in the video is "This statement is not true", whereas Gödel constructed a mathematical statement that says something along the lines of "This statement is not provable". Proving something is a different process than stating something.