I'm always fascinated by how Gödel's incompleteness theorems, Cantor's diagonalization proof, Turing's halting problem, and Russel's paradox all seem to graze the boundaries of logic. There's something almost terrifying about how everything we know seems to "bottom out" and what we're left with is an embarrassingly small infinite set of truths to grapple with.
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.
In some sense, I find it reassuring that the practice of logic (and mathematics as well) is deeply rooted in the human condition.
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.
You may find Constructor Theory interesting. An attempt to express physical laws solely in terms of possible and impossible transformations.
“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.”
> Gödel's incompleteness theorems, Cantor's diagonalization proof, Turing's halting problem
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.
Physics only seems to be continuous when you “zoom out”.
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)
Well yeah, we’re finite beings so the things “like us” tend to be finite as well — what we study in physics.
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.
Everyone has their own way of stumbling through to a breakthrough, where suddenly things that had been confusing and complex suddenly seem clear, beautiful, and intuitive.
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.
1. Gödel encodes statements about number theory into numbers via Gödel numbering: an arithmetic encoding.
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.
Take this with the most non-serious mode: In the methods used by Gematria and various arts, there is a similar mechanism at play is there not? Transforming words into quasi-hash coordinate space that is computable and thus able to see what is related or equal?
Fascinating observation, thanks. Relevant to your comment but diverging farther from the original post: Coincidentally, I am taking a beginner's Kabbalah course right now. I wonder if some of the writers of scripture actually used steganography or other word encodings such as the ones you allude to intentionally. One obvious example of word play at the meta level might be Psalm 119.
Yeah, along those lines I’ve joked that the Bible admits it’s written by a LLM: “in the beginning was the Word and the Word was with God and the Word was God” - that rings like a recursive declaration statement with Genesis and other similar statements.
The people who invented numerological techniques knew that you could manipulate numbers using particular rules and discover new facts about the world -- for example that you could measure the length of strings and use that to determine, which ones would sound good if you plucked them at the same time.
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.
Has anyone done work on finding undecidable math beyond self-referential statements? Meaning: beyond variations of "who shaves the barber," do we have a sense that the undecidable statements are all pathologically long, or are there (we think) undecidable statements a human can comprehend that are undecidable that don't rely on self-reference?
I believe the continuum hypothesis is an example of an undecidable statement.
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.
So the most physically grounded example I know of is the undecidability of some spectral gaps[0] (is there a discrete jump between the ground state and the excited states), which as far as I can tell doesn't rely on self-reference.
Apparently it does? Check this old comment from Scott Aaronson:
> 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.
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.")
I think for mathematics a good suspect is probably the Riemann hypothesis, which many other results rely on. We don't know that it's "undecidable", but from what I've read it's probably true and (even more interestingly), we can derive meaningful results from it being "probably"/"mostly" true (e.g. "for 99>% of cases it is true"), even without knowing that it is 100% decideably true.
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).
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.
As the article mentions, the generalized continuum hypothesis has been proven to be undecidable in ZFC, and I believe specific Diophantine equations have been proven to be undecidable. Axiom of Choice of course is undecidable from the other ZF axioms/axiom schemas. Answering questions about a presentation of a group is provably undecidable in general but since it is a kind of halting problem that makes sense.
Here is the thing with that. Technically every individual instance of a problem is decidable. It's only in the universal case that they become undecidable.
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.
Gödel's first incompleteness theorem just guarantees that for every system of axioms that is computable and "strong enough", an undecidable sentence exists.
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.
In a sense _all_ of the axioms of a given system are undecidable. They're just given, and they're relatively arbitrarily chosen. You can create, for example a version of set theory where the starting axioms are different from ZFC (the "standard" set theory) and you can derive some of the axioms of ZFC from them. What Godel proved is that no matter what set of axioms you choose, as long as it's sufficient for expressing basic arithmetic, you can produce still produce new undecidable statements, or there will be true statements that you can't prove with it.
I have a blog post that does a somewhat deeper dive into how to build a self-referential sentence @ https://r6.ca/blog/20190223T161625Z.html where I attempt to answer the question:
> 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?
I remember this video containing some major inaccuracies in his presentation of Hilbert's program (which is understandable, he is not an expert), so you might want to take the rest of the video with a grain of salt as well.
What is the major inaccuracy? Usually when I hear claims like these and ask for an elaboration it turns out it's not a major inaccuracy at all, just a pedantic disagreement over what mostly amounts to style.
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.
The way he presents Hilbert's program in 13:34 would make it immediately incompatible with Gödel's theorems. But Hilbert's program was different from what is suggested in the video. It was concerned with proving the consistency of mathematics (or more specifically, arithmetic) using "finitary methods", and in a "conservative" manner using the notions of "real" and "ideal" mathematics. Whether Gödel's theorems show that this is impossible is not completely clear, as it is not established what should count as "finitary", and how to interpret Hilbert's conservativity requirement. See this section for an overview: https://plato.stanford.edu/entries/hilbert-program/#4
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.
I think you have to be really, really charitable not to see the Second Incompleteness Theorem as a complete repudiation of the Hilbert Program - at least it destroys the possibility of proving ZFC consistent in PA - to the point that I think it's a reasonable simplification to say that the Hilbert program failed, even if the paragraph you linked shows that some people have been trying to salvage Hilbert's program by relaxing it a little. I'm aware e.g. of Gentzen's proof of the consistency of PA, but I don't find it plausible to claim that it uses "finitary methods". At the very least, I don't think such arguments would have convinced the people that Hilbert was trying to convince, such as intuitionists.
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.
Not speaking to any inaccuracies as I haven't watched the video, but my main hesitancy is that he's not a mathematican, his videos aren't reviewed prior to publication, and Godel's work is very subtle and often misunderstood.
I look at videos like these as gateways to get someone excited about a subject, not as scholarly works. What you say is good to keep in mind on any video. You can’t get the full depth of anything complicated in 30 minutes, but it can make you want to learn more.
I've only had one math prof be able to articulate Gödel's Incompleteness Theorem for me in a way that I could really understand (on a superficial level of course).
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.
Nagel & Newman's Gödel's Proof is an excellent book on how the proof works. It doesn't have all the tie-ins and fun asides that GEB has, but it's stronger for it.
If you’re not entertained throughout I don’t think there’s any reason to stick with it. It’s not like there’s some huge payoff at the end where “it all clicks.” It’s a fairly meandering journey across several disciplines with a lot of experimental literary techniques, and while it’s certainly intellectually challenging and rewarding, if you’re not enjoying the process there’s no reason to stick with it!
There's better resources if you just want to know about Gödel's Incompleteness Theorem tbh. GEB is neat because of all the other ideas he ties into it.
I don't have an answer for you (I last read it so long ago that I can't actually recall the specific content - though I'd be surprised if it didn't, given the title!), but just echoing that, although I _adore_ GEB (actually, I'm over-due for a re-read!), I've tried-and-failed multiple times to get through "Le Ton Beau De Marot", by the same author. Certain books just don't click with some people, and that's OK!
I lost track of the equations and theorems, but if when I put it down and come back to it, I've lost momentum! lol. Like "Gravity's Rainbow"... someday I'll make it through that without getting utterly lost.
Yup the theorem gets proven in the book. It's very very verbose but the content is clearly there.
"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.
It "gets to the theorem" without offering a formal proof, but having read both, I find that Hofstadter's short stories and intuitions have done more for my understanding of Gödelian logic than any formal proofs have.
Not related but I have been recommending Douglas's new popular book "Surfaces and Essences: Analogy as the Fuel and Fire of Thinking". He has few lectures on youtube on this topic in case you want to explore the content of the book before jumping in.
> 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.
From a newbie here, Aside from the one (and sufficient) self referential formula, have we come up with other examples of non decidable propositions that are meaningful?
Well, famously the halting problem is undecidable.
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.
A well known example (mentioned in the article) is the Continuum Hypothesis (CH; https://en.wikipedia.org/wiki/Continuum_hypothesis). Godel proved CH is consistent with Zermelo-Fraenkel (ZF) set theory; Paul Cohen proved that CH is independent of ZF, and hence CH cannot be decided on the basis of the ZF axioms.
By now there are numerous others; this is one of the earliest & best known examples in mathematics.
Does anyone know of any material linking Godel, Turing, and John McCarthy's work, beyond their individual publications?
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?
Godel’s collected works (including much unpublished work and correspondence) have been published by Clarendon Press, with more work (including translations from German) put into them than pretty much any other mathematician’s collected works.
I thought this writeup was quite good. Anyway, anyone interested in this is also likely interested in Rosser's theorem: https://scottaaronson.blog/?p=710
I have known about Godel's work and the incompleteness theorem but never understood it much until I read this article. Can anyone recommend a book relating to Godel's work written is a similarly accessible style?
Maybe my link at https://news.ycombinator.com/item?id=38395058 will help? Though even I kinda gloss over how to define sub. It is, in my experience, the most technically challenging part of the proof to actually formally define. I'm happy to try to go over details with you. There is also Section 5.3.1 of my thesis at https://r6.ca/thesis.pdf which probably goes into more detail than you would like.
Thanks, in your case the informal definition is clear. I believe in the Quanta article the second and third argument of sub are switched relative to yours.
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.
> do you use Cantor-style diagonalization for the fixed-point theorem?
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.
I watched the video and the video does not in any way attempt to debunk Godel's proof.
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.
I didn't watch the video, but FWIW I have personally formally verified the First Incompleteness Theorem (Goedel-Rosser variant) within the Coq proof assistant.
My biggest mistake was following the traditional single variable definition of substitution. I now understand that modern CS definitions of substitution typically substitute all (free) variables simultaneously. For variables that you don't want to substitute, you are required to explicitly map them back to themselves.
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.
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...