I took a full semester course on Godel's Incompleteness Theorems in college and found it rewarding. It was one of those experiences that convinced me that hand-wavy familiarity with stuff sometimes pales by contrast to a deep dive.
One of the professors also had a very old newspaper clipping taped up (it was brown then and that was quite a while ago), about several mathematicians committing suicide in the wake of those proofs. I've looked for corroboration of this and have never found it. A bit difficult to comprehend from a modern perspective, but more plausible with an appreciation of the 19th Century faith in rationalism / logical positivism that Godel helped overturn.
Not many people are aware that Godel spent much of his life secretly working on a modern update of an ontological argument for God's existence, and didn't reveal this until late in life -- https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_pro...
As far as I know it's not like the proofs caused a wave of suicides, but mathematicians studying this topic often became mentally unstable, including Godel (who starved himself in a sanatorium) and others like Georg Cantor.
I'm curious where you studied; I also took a semester course on "logic and computability" where the main text we read was 'Godel, Escher, Bach'
We briefly talked about Godel's proofs, but they are nontrivial. Henkin's proof of completeness is hard enough[1]. I don't mean to sound dismissive, but a class where Godel, Escher, Bach is the text does not seem very rigorous. Logic is very tricky stuff. And once you get into infinities, it's not even intuitive.
This article referenced some guys jumping off buildings... maybe it was more of the journalist's interpretation, connecting the sort of thing you mentioned with the suicides in a less direct way than I recall. I have wondered if it was a real news clipping (it looked like one), or some kind of old joke.
To answer your question, I went to one of the so-called "elite" American colleges that still has a primarily classical/analytic philosophy program (as opposed to what is known as a "Continental" program). Would rather not say which one, but I was able to take some great logic courses through the philo department.
We used Godel's work directly, and if memory serves also some Goldfarb.
Though not a proof of the existence of God as worked on by Godel, but Al Platinga is known for his work for the logical discussion of the rationality or religious belief
Somewhat related excerpt: https://www.princeton.edu/~hhalvors/restricted/plantinga-Rea...
Plantinga is known for his proof of God's existence, and in fact a proof of any sentence you like, using the modal logic operators of possibility and necessity: "possibly necessarily pigs fly, therefore pigs fly". (Where "possibly" is shorthand for "in some possible world", and "necessarily" is shorthand for "in all possible worlds".) It's a valid proof if you buy the assumption, but the assumption is dubious at best.
Of course it's valid! A world-renowned philosopher like Plantinga wouldn't publish a proof that's not valid. That's like saying Dijkstra's code compiles :)
The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise. E.g.: the possibility of a maximally great being seems to definitionally imply its necessity. Why? Because such a being B must have some properties P = { ? ? ? ... }. We may not be sure what's inside P, but we know, with absolute certainty, that existence is in there.
Kant would disagree. He thinks that existence is not a property. This is a rare case when I think he's right.
> E.g.: the possibility of a maximally great being seems to definitionally imply its necessity.
One of my favourite tongue-in-cheeek replies I read to these ontological arguments: Ah, but surely there is no greater being than one who could create the universe despite not existing!
> The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise
But that is also true of the informal rhetorical arguments that are more common in (christian) apologetics.
The gift of formal proofs is that they make explicit and unavoidable this embedding of conclusion in premise, which is fundamental to all (epistemologically rational) apologetics
Here's a nice way to make peace with Godel's theorems.
Let's say your beliefs about the integers can be summarized by some formal theory T. ("Every number has a successor", and so on, until your intuition runs out of things to say.) Now Godel jumps out of the bushes and says aha, your T doesn't include Con(T), so you aren't the math genius that you thought you were!
But let's stop for a moment and consider what it would take for T to include Con(T). First of all, compared to other sentences about integers that you believe, Con(T) is an absolutely huge sentence. It must contain an arithmetization of all of T (encoding the axioms, inference rules, etc. into integer arithmetic).
Second of all, if Con(T) is included in T while speaking about T, it might need to include an arithmetization of Con(T) itself! That uses a diagonal construction ("quine" in computer science terms), making the sentence even bigger. Now you're looking at some kind of hundred-kilobyte Diophantine equation, with no intuitive reason to believe it at all.
And third of all, it's easy to see that an inconsistent theory T would easily prove Con(T) (because it proves any sentence), so having Con(T) inside T doesn't even give you any positive evidence for trusting T. In fact, we're lucky to live in a world where Godel's theorems are true, and having Con(T) inside T is negative evidence instead of none at all!
To some degree Chaitlin's equations [1] make the issue less abstract than that though.
"We outline our construction of a single equation involving only addition, multiplication, and exponentiation of non-negative integer constants and variables with the following remarkable property. One of the variables is considered to be a parameter. Take the parameter to be 0, 1, 2, ... obtaining an infinite series of equations from the original one. Consider the question of whether each of the derived equations has finitely or infinitely many non-negative integer solutions. The original equation is constructed in such a manner that the answers to these questions about the derived equations are independent mathematical facts that cannot be compressed into any finite set of axioms."
So there are finite (though several hundred pages long) equations for which the finiteness of the solution set is independent of every finite axiomatization of arithmetic. So suddenly, even though the formula is enormous, the type of sentence is perfectly normal. Does f(x) have finitely many solutions, where f(x) is built from addition, multiplication and exponentiation.
Much more so than Gödel’s incompleteness this deeply violates my intuition about what type of statements should be decidable.
There's no single f(x) for which finiteness of the solution set is independent from all axiom systems. (We can always just add an axiom saying f(x) has finitely many solutions.) Chaitin shows something different, an f(x,y) for which finiteness of solution set in x for a given y becomes independent from more and more axiom systems as y grows (because it encodes larger and larger instances of the halting problem). That doesn't disagree with my intuition at all, in fact it seems obvious.
Well given that it was considered a surprising and highly non-trivial result when it came out less than thirty years ago, I'll say that it's obvious only in the sense that all statements that have been proven are obvious after the fact.
And yes, I worded that ambiguously. Let me rephrase, to see if I got it correct: Pick any finite axiomatization. Then there is a concrete f(x) that we can write down in about 200 pages, for which finiteness of the solution set is not decidable.
The fact that there are diphantine equations for which finiteness is undecidable is really surprising to start with to me.
Representing "Con(T)" in a formal language with the Peano Axioms isn't all that long, relatively speaking. No diagonalization is needed. It's basically:
~(Ex)Proof(x, ~0=0)
I.e., "There doesn't exist a proof of ~0=0."
Of course, representing the word "proof" using PA isn't trivial, and expanding that bulks things up a bit. But the sentence that's really long is the Godel sentence. "(G) There is no proof of G."
I wonder if anyone has written out a Gödel sentence in full as a statement about numbers in English. It would be fun to see how big it gets.
Also, the comment about size and diagonalization is interesting. The Gödel sentence from the first incompleteness theorem is made by diagonalizing, while the sentence from the second incompleteness theorem is just "Con(T)", so the sentence from the 2nd theorem is shorter and more natural if written out in full---making it even more disappointing that it's not provable. Indeed, if we put in more work we should be able to prove a more interesting theorem, but I never really thought about it before.
The most interesting outcome from Goedel's incompleteness is the study of alternative arithmetics [1]. And I don't mean ones that are progressively weaker, I mean ones that are incomparable and to which the same incompleteness theorems may not apply. For instance, Boucher's Arithmetic without the Successor Axiom.
Carl Hewitt (of Actor model fame) has this thing where he claims that contradiction alone allows you to defeat Godel Incompleteness, so he shops it around places and everyone's like, "man, wtf, this isn't how that works". I saw him shop it to D. Hofstadter and Hofstadter basically smiled and took the little piece of paper and threw it away when Carl wasn't looking.
This doesn't have anything to do with anything, just a thing that happened
I know that the above was written in jest anyway :) but just for completeness (har), a contradiction would help you defeat many things (i.e., it's not specific to incompleteness theorems, so to speak), because given it, (at least in traditional logic) you can prove anything. This is trivial and known, but to spell it out, if we have a contradiction formalized by p and not p (given), we can prove that q:
1. p and not p (given).
2. p (from 1).
3. not p (from 1).
4. p or q (from 2 (disjunction introduction)).
5. q (from 3 and 4).
So obviously this would upset quite a few things around :) that said, the interesting stuff is with Graham Priest's (et al.) paraconsistent logic systems wherein your system can tolerate a contradiction without exploding in whole. And (so the story goes) those systems may offer an actual insight into handling incompleteness (while still being usable). If anyone has looked into this more, would be interesting to hear about it!
That behaviour was desribed by the old masters as 'ex falso quodlibet': from falsity whatever (when else am i having the chance to be this pedantic). In the uni I was taught that hippie-era AI dealt with that with things called non-monotonic reasoning, abduction, truth maintenance systems.
“All difficult conjectures should be proved by reductio ad
absurdum arguments. For if the proof is long and complicated
enough you are bound to make a mistake somewhere and hence a
contradiction will inevitably appear, and so the truth of the
original conjecture is established QED.”
Hofstadter's examples 'this sentence is false' blah blah aren't inconsistent at all: it just semantic nonsense likes Gödel's made up logic and Cantor's ordinals before that? Mathematics exist without us no?
Wait, you are saying mathematics exists independent of humans but logic does not. But mathematics is build on top of logic, how can it gain independence from humans if its foundation does not have such independence? Or am I just misreading your statement?
To me this seems backwards. Don't we define some basic objects with axioms and then use logic to find out the consequences of the axioms? We make up some axioms for natural numbers, then we define operations like addition and multiplication on them, and finally we investigate the consequence of those definitions, we discover for example that some numbers have very special properties and can be used to uniquely decompose all numbers, we call them prime numbers.
I would therefore say that mathematics is a human invention and build on top of logic, it seems in no way universal. All the things we discover in mathematics are nothing but consequences of the axioms, the definitions, and the logic used to prove things. If there is something universal, at least so it seems to me, than it would have to be logic.
As a mathematician, I don't know if I agree completely with this statement. Logic in practice is essentially its own branch of mathematics with tools that are sometimes helpful in other branches, but it has its own internal motivations for research that are irrelevant to say an analyst or a number theorist. In my own opinion, it's as much a framework for the doing of mathematics as is the English language, and not too much more.
I recommend Torkel Franzén's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. It is readable without sacrificing rigor.
It is especially good at ensuring the reader doesn't come away infected with the pseudo-profound BS that plagues many discussions of the Gödel's Theorems.
That, and Nagel's book on the proof, have been recommended on HN before (very recently!). And Rebecca Goldstein's book has been dismissed as too hand-wavy.
For important, wiki-friendly topics like this one, HN is frustratingly not great for building a readily checkable/cumulative knowledge base, rather than encouraging a forgetful herd discussion that goes around in circles. It is as I say frustrating for anyone who wants long-term knowledge rather than flimsy "news".
This isn't really about Gödel, but I always wish that people had a little bit less of a natural instinct towards bastardized Gödelian thinking. So that there would be fewer infuriating people arguing things like "Infringing on my right to infringe on the rights of others infringes on my rights." Or, "You can't be against criticism, because then you'd be criticizing criticism." I've been rolling my eyes at these arguments for decades, and I wish fewer people thought they were clever.
I recently read 'Incompleteness: The Proof and Paradox of Kurt Gödel' by Rebecca Goldstein [1], I highly recommend it for those interested in learning more about his life and the proof itself.
I always was wondering: Godel proved his theorem regarding formal systems described in Principia Mathematics. In my understanding this is some higher level logic with recursive functions.
But how this can be extended to the whole universe of all possible formal systems? Who guarantee that there will be no some new system with quantum-oracle-operator, which will not be affected by incompleteness theorem, and can self-proof self-consistency?
Even well known m-recursive functions (which are essentially Turing machines) are wider class than primitive recursive functions used in the proof..
Godel's technique is a constructive proof that depends on two things to work. One, the logic needs to be at least strong enough to express the Peano axioms. Two, it needs a finite formalism of the logic to construct the proof out of.
If you have those two things, Godel's technique works. The details vary greatly based on the formal logic in use, but part of the process is encoding the formalism in Peano arithmetic.
So no, adding more things doesn't break it, because the construction takes those additional things into account.
Unless you want your logic to be infinite, of course. In that case, the method would break down. But it has to be infinite in the sense of having no finite representation, rather than the much weaker sense of having some infinite representation.
> Unless you want your logic to be infinite, of course. In that case, the method would break down.
Godel numbering is infinite, because it is just natural numbers. Nothing prevents you to build the same proof for infinite number of axioms, rules, functions, variables..
> Godel numbering is infinite, because it is just natural numbers. Nothing prevents you to build the same proof for infinite number of axioms, rules, functions, variables..
That's kind of a non-sequitor. Second-order logic, the logic required to express Peano arithmetic, consists of a finite number of axioms and inference rules. The number of statements that can be generated with those rules is irrelevant. The logic is finite.
Godel numbering requires assigning a number to each logical axiom and inference rule. The mechanism of Godel's numbering implies that every derivation has a unique number as well, but that number is derived, not assigned. The difference is important. It means that the information required to construct the system is finite. If the supply of axioms and inference rules was infinite, with no finite alternate encoding, it would mean Godel numbering would fail because the process of assigning numbers to each axiom and rule would never complete.
But that's all a bit of an aside. To get back to your original question...
Godel's proof provides a mechanism to construct a statement that refers to itself in any logic that can express Peano arithmetic. Once you can make a statement refer to itself, the game is over. You've lost.
But Godel's approach is even more clever. Not only can a statement refer to itself, it can refer to proofs in its own formal system.
So it constructs "This statement has no proof within the formal system it's expressed in."
That's far more subtle of a statement than you give it credit for. It makes no claim about other formal systems. But once you start addressing it from a different formal system (or an informal metalogic) the statement no longer refers to the logic system in which you are examining it.
So sure, you can say that Godel statement G0 constructed in formal system L0 is provable (or disprovable!) in formal system L1. But that doesn't prove anything about the completeness or consistency of L1, because G0 is a statement about L0. And if L1 happens to be strong enough to encode Peano arithmetic, you can construct a statement a Godel statement G1 which refers to logic L1.
This is always applicable. Whatever your G0 and L1 are, G0 says nothing about L1, but the existence of L1 is irrelevant to the statement G0, and very probably also allows the existence of G1. (I've spent lots of time discussing when it doesn't, and won't belabor the point further.)
> If the supply of axioms and inference rules was infinite, with no finite alternate encoding, it would mean Godel numbering would fail because the process of assigning numbers to each axiom and rule would never complete.
I strongly disagree with that. There is no evidence of that.
> And if L1 happens to be strong enough to encode Peano arithmetic, you can construct a statement a Godel statement G1 which refers to logic L1.
As I said before, Godel proved that your G1 is unprovable in specific framework of Principia Mathematics, which is first/second/higher theory/logic (consist on quantors, functions, predicate, variables, rules).
I don't see evidence that there can be no other framework even with Peano arithmetic inside which can't deliver consistent theory.
You started speculating about framework with infinite set of axiom, and I disagreed with that, but there can be other type of infinite framework, say when you allow proofs of infinite length, then Godel numbering may be impossible, and it can be example of such framework.
If you want to see a relatively brief video of a somewhat drunk Scott Aaronson talking about many interesting possible consequences of the no-cloning theorem, including Godel's Incompleteness Theorems (iirc), enjoy this one from a quantum crypto conference - https://www.youtube.com/watch?v=Z-fa669IR7I
It says "any system which includes the Peano axioms is either inconsistent or incomplete." So having a wider class doesn't help, if it contains the Peano axioms.
Proof was made within specific framework, with very specific quantors and type of inference, I still don't understand how it prevents existence of more powerful frameworks with different quantors and inference where incompleteness theorems wouldn't work.
You can construct a new Incompleteness Theorem for any more powerful formal system. To really get syntactic completeness, you would need an infinite tower of Goedel Statements as axioms, where the truth of each one is a completely independent mathematical fact not reducible to any other axiom ever.
Effectively, syntactic completeness in logic is equivalent to the Halting Problem in computing, via bijective proofs.
Let me give you example.
At first you have predicate calculus, and Godel completeness Theorem.
Now you add new tool: existence predicate, and you got first order logic, which allows you to prove Godel's incompleteness Theorem.
What is the guarantee exactly that more advanced systems can't exist? Say system with new 'quantum hack' operator.
You can't prove formula from Godel's proof? 'Quantum hack' under some conditions covers missing gap in proof path by building continuum truth table and give you tool to check if formula from Godel's proof actually provable, or it is false.
Goedel's Completeness Theorem is for semantic completeness, and still applies to first-order logic. It says, "every theorem which is semantically true for its theory (true in all models of that theory) is syntactically provable." Goedel's Incompleteness Theorem applies to syntactic completeness. Syntactic completeness would mean, "Every syntactically-valid formula is either provable or refutable." Instead, what Goedel's Incompleteness Theorem tells us is: "Some syntactically-valid formulas are neither provable nor refutable, because they're true in some models (standard models) but not in others (nonstandard models)."
Again, this applies to any given formal system. Goedel's Incompleteness Theorem is parametric over formal systems, with first-order Peano Arithmetic being one of the weakest, most standardized systems in which it applies. The real condition for the Theorem is, "Any formal system sufficient to describe Turing machines."
>Say system with new 'quantum hack' operator.
That operator is called a Turing Oracle, and it's physically impossible. Possessing a Turing Oracle is equivalent to reversing the Second Law of Thermodynamics and refuting Heisenberg's Uncertainty Principle. It's physically wrong.
> Goedel's Incompleteness Theorem is parametric over formal systems, with first-order Peano Arithmetic being one of the weakest, most standardized systems in which it applies.
It is parametric over formal systems described in Principia Mathematics. That's it. It doesn't take into account other possible types of formal systems. At least I didn't notice this when reading actual proof.
> That operator is called a Turing Oracle
I think it may be very different thing. I just gave you a quick example. That operator can be something very different. You can set measure on space of proofs, and derive concept of asymptotic proof, and say if proof is asymptotic, then it is proof. There can be many variations around possible formal systems.
> and it's physically impossible
This is very strange argument. Turing machine contains infinite amount of memory, and likely is physically impossible.
Just chipping in with my interesting reading about the implications of Godel's incompleteness theorems.
This piece about what the theorem means for developing "deep AI" and the human mind, was a fascinating eye opener for me, about the far stretching implications of the theorem.
"A common misunderstanding is to interpret Gödel's first theorem as showing that there are truths that cannot be proved."
I've heard it stated that confusing way so many times in popular media. And then often follows quantum mechanics, and geniuses going mad, and the world is just your imagination... forever.
Agreed it has been abused. On the other hand, if you adhere to a computational theory of mind and see the mind as computation over a formal system, then it is saying something about the mind and the fact that some (true) sentences cannot be proven in that system, isn't it? It is a big if though.
(though maybe in a completely irrelevant sense of truth).
Just poking fun at the way these things are presented in pop.sci. media.
Anyway, talking over my head, I'm not shure formal systems are a good way of modelling the mind itself. Formal systems are (usually) considered consistent. The mind is not. Neither are neural nets. And it's interesting how neural nets, and other statistical models/algorithms that drop the requirement of always beeing right, seems more much more capable in certain practical matters.
Wow, is that what people actually think a "computational theory of mind" is? Look, just because every program can be trivially rewritten as some kind of formal proof system, doesn't mean that any given program meaningfully has the semantics of a formal proof system, let alone the mind.
When I rant about it, I claim his theorem says "any system that reference parts of itself is either incomplete or inconsistent," and that the universe is such a system, as we're a part of it, and refer to parts of it.
So therefore, the universe is either full of magic (in a system with inconsistency, anything can happen), or mystery (there are true things that we can never prove).
My belief is that the quest to find a unified physics that describes everything is provably impossible due to Godel's theorem.
And on the rare occasions when I look for evidence of God, the fact that one of the things we can know for sure - is that we can't know everything - provides about as much comfort as I need.
My belief is that the quest to find a unified physics that describes everything is provably impossible due to Godel's theorem.
How would that happen? Physics is an empirical science, all we have to do is to look at what actually happens and write it down. Even if we fail to find good mathematical expression to describe what we see, we can always just create charts and tables describing what happens. There is nothing that prevents us from fully describing physics.
Unifying physics then just means finding one mathematical model that is able to describe all the aspects we discovered in different limits. I can not see how Gödel's incompleteness theorem would have any bearing on this. We just have to find a set of equations that reproduce our observations given the experimental setup. This does not involve any proofs, it's just the question whether a set of equations accurately describes the universe.
I can really only think of one way in which describing the universe with mathematics must fail and that is if there is no mathematical description of the universe. Otherwise we could always guess a set of equations and then verify that it works in all experiments we ever performed. You can of course never be sure that you did not simply miss one experiment that causes your theory to fail, but that is in the nature of physics. This also seems pretty unlikely, I fail to imagine anything that could escape all attempts of mathematical describing it in principle.
> My belief is that the quest to find a unified physics that describes everything is provably impossible due to Godel's theorem.
To be precise: it tells us that it's not generally possible to build a complete consistent model, but it may still be possible in specific cases, like our universe. My hunch is that such a model does exist, that we will find it, and further, that it will actually be rather elegant. We'll never be able to prove we've found it though, because we only have partial information— if we were running on a virtual machine, is the host system running Linux or BSD?
This sort of application is wildly out of bounds of the true scope of the theory.
The relationship between physics (unified or otherwise) can't be resolved with reference to Godel's theorems.
Well, you're actually making metaphysical claims more than mathematical or physical ones. One of two assumptions, depending on how literally the sentiment that the universe is a formal system is intended, is being elided here:
1. That the universe _is_ a formal system, rather than being describable in the language of some formal system. It's not evident what the universe being a formal system even means, or how it squares with basic intuition regarding e.g. the fact that physical systems have state.
2. That, dropping the physical system <=> formal system equivalence and given some real system R consisting of some fundamental entities whose behaviors can be described in full in the language of some formal system S, (borrowing a useful construct from Lucas' anti-mechanism argument, even though I don't buy that argument) no machine can be constructed in R which computes theorems of some formal system S' in which all true statements of S are provable, meaning that no state of the system R can be said to contain a description of S', and that S' is therefore not describable by any arrangement of the entities in R (assuming some reasonable predicate over states of R that is true for a state when some arrangement of a subset of the entities in that state describes S'). Intuitively, this doesn't seem to hold up: by analogy, I can describe a universal Turing machine with a computer equipped with only finite memory. You could then attempt to go down the road of claiming that, even if a description of S' is possible in R, that a mind within R would not be capable of formulating that description, but then you're heaping on an even larger tangle of assumptions, unknowns, and things you have to define if you're going to argue the case rigorously.
The point being that confidence about _any_ hypothesis about the nature of reality made on the basis of Gödel's incompleteness theorems is not epistemologically warranted.
I am halfway through reading Raymond Smullyan: A puzzle guide to Gödel, after finding out about his recent death here: https://news.ycombinator.com/item?id=13626221 . It explains Godel's incompleteness Theorems accurately to a layperson through a set of logical puzzles.
One of the professors also had a very old newspaper clipping taped up (it was brown then and that was quite a while ago), about several mathematicians committing suicide in the wake of those proofs. I've looked for corroboration of this and have never found it. A bit difficult to comprehend from a modern perspective, but more plausible with an appreciation of the 19th Century faith in rationalism / logical positivism that Godel helped overturn.
Not many people are aware that Godel spent much of his life secretly working on a modern update of an ontological argument for God's existence, and didn't reveal this until late in life -- https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_pro...