alt Hacker NewsWhat Do Gödel's Incompleteness Theorems Mean?
Comments
It's much easier than it seems.
* There are axioms, there are models, and there are theorems.
* A model is a particular structure with objects and relationships. The "standard model of arithmetic" is just the natural numbers 0, 1, 2, ... with normal rules of addition and subtraction and so on. A different model could be the real numbers, or one that includes infinitesimally small numbers, or so on.
* A set of axioms are rules about how a model can work. For example, we can have an axiom for any set of objects called "numbers" with an operation called "addition" that the operation must be commutative (x+y = y+x). The standard model above is one model that satisfies this axiom.
* A theorem is a fact that can be true or false about a given model. For example, "the model has infinitely many objects." If we can prove a theorem from a set of axioms, then that theorem is true for every model that satisfies the axioms. However, there can also be theorems that are true for one model that satisfies the axioms but false for a different model.
Godel's completeness theorem says that if a theorem is true for every model that satisfies a set of axioms, then one can prove that theorem from the axioms.
Godel's first incompleteness theorem says that in any axiomatic system (sufficiently complex) there are theorems that are neither always true nor always false. In other words, there is a theorem that is true for some model of the axioms but false for some other model of the axioms.
Of all the incompleteness-style theorems, I find the Halting problem to be the most approachable and also the most interesting. Maybe it's because I'm a software dev that dabbles in math rather than the other way around. But that makes me wonder if all of Gödel's theorems can be stated if 'software form', so to speak.
Interesting points in here.
e.g. that Godel didn't think this scrapped Hilbert's project totally:
>Gödel believed that it was possible to redefine what we mean by a formal mathematical framework, or allow for alternative frameworks. He often discussed an infinite sequence of acceptable logical systems, each more powerful than the last. Every well-formulated mathematical question might be answerable within one of them.
As far as I can see people always radically exaggerate the effect of the incompleteness theorems. It seems interesting that any nontrivial axiomatic system has statements which are true but unprovable but to say that derails Hilbert’s project seems just obviously untrue when you can for example join math postgrad programs now which are focused on formalisation. [1] So formalisation is very much still going on, probably more so now than ever given advances in theorem provers.
Yes there are undecidable statements (eg the continuum hypothesis) but that doesn’t change the fact that the vast vast majority of statements in any axiomatic system are going to be decidable, and most undecidable statements are going to have “niche” significance like that.
[1] eg https://www.imperial.ac.uk/study/courses/postgraduate-taught...
> “incompleteness theorems” established that no formal system of mathematics — no finite set of rules, or axioms, from which everything is supposed to follow — can ever be complete.'
There is usually a 'not sufficiently complex' clause in that definition. Presburger arithmetic is complete: https://en.wikipedia.org/wiki/Presburger_arithmetic
Natalie mentions the Newman & Nagel's text "Gödel's Proof," a
(//the//?) 1958 classic on the subject. [[1]] Having left IBM in
December 1990, I spent a month with the text, dipping into mild
insanity, taking to strange wines to relieve myself of the fear
that my previous years long study of Whitehead & Russell's
"Principia Mathematica" [[2]] was not useless.
I really appreciate the inclusion of Alvir's statement on
whether or not Gödel thought he proved all logical systems
undecidable and incomplete. About 80% into the article is her
quote:
>> Often people will speak as if the CH is the smoking gun that
>> shows sometimes mathematical questions have no answer. But
>> in my opinion, this situation provides very little evidence
>> that there are “absolutely undecidable” mathematical
>> problems, relative to any given permissible framework.
Though I would have added a reference to Infinitary Logic [[3]]
after dropping the reference to L-omega-1-omega. I suspect most
readers would find discussion of higher-order and modern logic a
bit confusing without a pause for further study. But a guide
post pointing in the appropriate direction would be good.
That this is the only critique I have of the article speaks to
Wolchover's skill in communicating complex ideas for a lay
audience. I really liked this article, so thank you @baruchel
for posting the reference to it.
:: References
1. https://search.worldcat.org/title/1543160023
2. https://search.worldcat.org/title/933122838
3. https://en.wikipedia.org/wiki/Infinitary_logicIs it releteble to Logic? I have heard that Economy is a subset of Logic, so is this theorem relatable to Economy?
It hints at something fundamental to how the universe works, in that there is always an adjacent possible.
I don’t think we’ll ever entirely know what they mean.
It may mean our brains are not currently equipped to understand the universe.
As a child, I noticed that the proofs of mathematical theorems were esoteric knowledge, known only to a few adults. I struggled to follow even the simplest proofs, and hoped that one day I might learn to create a proof or two of my own. This was not only a high aspiration, but a dangerous one. I saw no reason why certain knowledge of a true fact would be accessible to humans via proof. Any-one who embarked on the quest to find a proof risked embarking on a doomed quest to find a non-existent proof.
For me Gödel's completeness theorem is the miracle. Every valid statement has a proof. Amazing!
Aim a little higher, every true statement, and there might not be a proof. It is no surprise to me that this is true. It is a big surprise to me that Gödel was able to prove it; ordinary proofs are hard to find, and proofs of the limits of provability presumably even more deeply hidden.
Non-standard models of arithmetic are weird. Theorems that are true of the standard model of arithmetic and false in some non-standard model must surely be convoluted and obscure. The first order version of the Peano axioms nail down the integers, not perfectly, but very well. Restricting one-self to theorems that are true in all models of them, even the weird, non-standard ones, feels like a very minor restriction. Gödel's completeness theorem raises the possibility of writing a computer program to find a proof of every theorem that isn't convoluted and obscure. Gödel completeness theorem is the really big deal.
Except it isn't. That computer program turns out to be one of those wretched tree search ones that soon bogs down. The real problem turns out to be the combinatorial explosion inherent in unstructured search through the Herbrand universe. One needs Unification and one needs a still missing ingredient to give search a sense of direction. The interesting questions are about the "sense of direction" that lets us find some of the deeply hidden proofs that do exist. Will LLM's help? The answer will be interesting, either way.