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.
Having said all that, I'd taken mathematical logic in college to learn about incompletenss, but the most interesting things I got out of it were completeness and compactness. Non-standard models really can be quite interesting.
* 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.
Gödel's argument basically says that any system of mathematics powerful enough to implement basic arithmetic is a computer. This shouldn't be surprising to software engineers because the equivalency between Boolean logic and arithmetic is easy to show. And if you have a computer, you can build algorithms whose outcome can't be programmatically decided by other algorithms.
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.
Overall I really enjoyed this article, short interviews with mathematicians and philosophers on a topic I've often thought about.
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...
To understand the above Gödel result, the essential point is
the principle of elementary logic that a contradiction
Ā A implies all propositions, true and false.
(Given any two propositions A and B, we have A ⇒ (A+B),
therefore Ā A ⇒ Ā (A+B) = Ā A + Ā B ⇒ B.)
Then let A = {A1, A2, ..., An,} be the system of axioms
underlying a mathematical theory and T any proposition,
or theorem, deducible from them:
A ⇒ T.
Now, whatever T may assert, the fact that T can be deduced
from the axioms cannot prove that there is no contradiction
in them, since, if there were a contradiction, T could
certainly be deduced from them!
This is the essence of the Gödel theorem, as it pertains to
our problems. As noted by Fisher(1956), it shows us the
intuitive reason why Gödel's result is true. We do not
suppose that any logician would accept Fisher's simple
argument as a proof of the full Gödel theorem; yet for most
of us it is more convincing than Gödel's long and
complicated proof.
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 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_logicUnfortunately, Gödel's proof method per se only shows an example that is not so meaningful, involving self-reference. He builds a number-theoretical formal system which can talk about its own formulas, by encoding them as integers (something we do with computers now as a daily matter: all computer program text and other data is arithmetically encoded into binary, which has an interpretation as a number). In the context of Gödel's work, we call this arithmetic encoding "Gödel numbering".
Whether a proposition is true is reformulated as a number-theoretical property: instead of asking, is this proposition or equation true, we ask, is the arithmetic encoding of this proposition an integer which belongs to the set of theorem-integers; is it a theorem-number?
Within this framework, Gödel shows that a proposition can be made which says "G is not a theorem-number", such that this very propostion's own Gödel number is G! In other words, a kind of Quining is going on, whereby the proposition embeds a coded reference to itself. Essentially, Gödel introduces the idea that we can make a statement which says "I am unprovable", in formal, rigorous way. If that statement can be derived from the axioms, then a contradiction results: it was derived, yet it asserts the falsehood that it is not derivable, and so a falsehood was derived from the system's axioms. If it is true, then it points to incompleteness: there is a truth that can be expressed in the syntax of the system, yet cannot be derived.
Thus if we have any system expressive enough to encode the "G is unprovable" statement where that statement itself is G, that system is either inconsistent (allows a falsehood to be derived) or incomplete (allows true statements to be written which cannot be derived).
[dead]
When it first appeared, sure. But it wasn't with Godel and Turing that this happened.
Yup. Incompleteness is sort of a red herring. P≠NP (even though unproven) yields the real, practical, painful incompleteness.
If P=NP, but the best asymptotic solution is n^7, and it has so much overhead that the best practical solution is n^9, then it doesn't really matter that it isn't exponential. It's still unsolvable for easily accessible problem sizes.
Shameless plug: I put together a Jupyter notebook walking through the use of Herbrand Universes for a semi-decision procedure for first order logic: https://github.com/aetilley/harrison-rust/blob/main/Herbrand...
Fix axioms, we get a Godel sentence G1. Add G1 to axioms, we get G2. So on and so forth. In the limit of this process, we have our Universe.
[deleted]
So it indicates me to think about the boundaries while I design and build a system. These boundaries will protect us from those unsolvable constraints.
If we don't include the compiler and runtime, sure we can.
Godel's theorem is about formal axiomatic mathematical systems with certain properties like the ability to do basic arithmetic.
Godel's completeness theorem can not be understood without bringing in first order logic, because it is a statement of the expressitivity of the language(relative to its semantics). Other more expressive languages, like second order logic (with its usual semantics) is not complete. Trying to explain Godel's completeness theorem without bringing in the language is a path to confusion.
And your explanation of the first incompleteness theorem is also at best confusing. I must preface this with the comment that your definition of a 'theorem' matches what is usually called a sentence or a statement, and a theorem is usually reserved for a sentence which is proven by a axiomatic system. If the axiomatic system is sound, all theorems will be true in all models. The question of completeness is whether or not all truths(aka sentences true in all models) can be proven(aka they are theorems). With this more common usage of the words, Gödel's incompleteness theorems show that every consistent theory containing the natural numbers has true statements on natural numbers that are not theorems of the theory (that is they cannot be proved inside the theory).
Your description of the first incompleteness theorem is also true for complete logics, even for propositional logic (with your definition of 'theorem' as actually meaning statement). It has statements which is true in some models and false in others. This does not make it incomplete.
I mean, you can formally construct an axiom system defined to include (via axiom of choice) and assign a truth value to each of the independent propositions of first order arithmetic logic. There, you have consistent and complete system but not one that's a whit closer to being in usable by anyone.
I'm not even a finitist but I think being clear what's going on with these claims is important. It's like saying "the halting problem can't be solved by finite computers but my infinite-foo hypothetical computer can solve it, gotten mention that..."
As the GP points out, that's not what Godel's incompleteness theorem actually shows. Although it's a common misconception (one which unfortunately is propagated by many sources that should know better).
The key point of the incompleteness theorem is that it shows that (at least in first order logic, which is the logic in which the theorem holds) no set of axioms can ever pin down a single model. For example, no set of first-order axioms can ever pin down "the standard natural numbers" as the only model satisfying the axioms. There will always be other models that also satisfy them. So if you want to pin down a single model, you always have to go beyond just a set of first-order axioms.
Using the natural numbers as an example, consider a model that consists of two "chains" of numbers:
(0, 1, 2, 3, ....)
(..., -3a, -2a, -1a, 0a, 1a, 2a, 3a, ...)
The first chain is, of course, the standard natural numbers, but the second chain also satisfies the standard first-order axioms that we normally take to define natural numbers. So this model, as a whole, satisfies those axioms. And there is no way, within first-order logic, to say "I only want my model to include the first chain". That's what Godel's incompleteness theorem (or more precisely, his first incompleteness theorem combined with his completeness theorem) tells us.
But I don’t think incompleteness is best described as saying "no first-order axioms can pin down a single model" That’s more about non-categoricity/compactness/Lowenheim–Skolem.
Well, it's an obvious implication of the two theorems (completeness and incompleteness) combined: if a FO sentence is not provable from a system of FO axioms, it can't be true in all models of those axioms. And if an FO sentence is not provable, its negation can't be either (since proving its negation true would prove the sentence itself false). So the negation also can't be true in all models. That means there must be at least one model in which the FO sentence is false, and at least one in which its negation is false (so the sentence itself is true). Which means there must be at least two models of that set of FO axioms--i.e., the axioms can't pin down a single model. And the incompleteness theorem proves that there is such a sentence in every system of FO axioms.
I agree that the Lowenheim-Skolem theorem has similar consequences, since it says there must be models with different infinite cardinalities.
1. Complete (for any well formed statement, the axioms can be used to prove either it or its negation)
2. Consistent (can't arrive at contradictory statements ~ arriving at a both a statement and its negation )
3. The set of axioms is enumerable ~ you can write a program that lists them in a defined order (since the workaround for completeness can be just adding an axiom for the cases that are unproven in your original set)
If my understanding is correct, I believe your explanation is missing the third required property.
It's also important to point out that if we cant prove a statement or its negation (one of which must be true) then we know there are true statements that are unprovable. This is a much stronger of a finding than "Godel's first incompleteness theorem says that in any axiomatic system (sufficiently complex) there are theorems that are neither always true nor always false. "
Is that true, could it not be neither, i.e. independent of the axioms? Or is this assuming completeness which rules out independent statements?
[dead]
basically generalized the halting problem to arbitrary semantic properties.
Also though, just as for the Halting Problem, we are always allowed a three-way split. Rice proves that "Has property" vs "Does not have property" can't be done, but "Has property" vs "Does not have property" vs "Shrug - I dunno, seems hard" is possible, and indeed easy if you're OK with lots of machines landing in the "Shrug" pile. You can expend as much work as you like to shrink that pile, Rice just proved it would need infinite work to empty it completely.
Statement: Every sound (i.e. not just consistent, but sound) recursive theory of arithmetic is incomplete.
Proof: Assume it is complete. List all its theorems by a program. Then one can decide the halting problem as follows: for any instance, look whether "the program halts" or "the program does not halt" shows up in the list of theorems (since the theory is complete, one of them must show up; and since the theory is sound, the theorem is true).
There is current research into finding the smallest such Turing Machine. Here is one with 748 states: https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...
In the software form, it can be restated as: "there is no finite program that outputs the sequence with this property".
[dead]
Hilbert’s program was to reduce math to a finite set of axioms and was indeed derailed by incompleteness theorems(Gödel) and undecidability (Church, Turing).
Formalizing math with automated theorem provers has little to do with the goal of Hilbert program. Also they aren’t related to the foundational research that it entailed.
Also, as the article mentions, the implications as well as Gödel was largely misunderstood.
Although this is a common way of stating what Godel's incompleteness theorem tells us, it's actually not correct. As was posted upthread, when you combine Godel's first incompleteness theorem with Godel's completeness theorem (all this in first-order logic), you find that, for any sentence that is not provable in a system of first-order logic (such as the Godel sentence for that system), there must be a semantic model of that first-order logic in which the sentence is false. (I gave an example of such a model for the first-order axioms of arithmetic upthread.)
[dead]
Like people saying Godel theorems "prove" LLMs could never invent new mathematics because being a software system Godel applies to their operation, but not to humans which are not axiomatic systems, and thus humans can go beyond them and beyond the limits of Godel, humans can "know" a result to be true even if Godel says you can't prove it.
Would the rules of said machine have statements they themselves cannot prove by parameters set in their ‘programmed(by humans, machines, or other machines)’ assumptions?
This is just flatly untrue, in the strictest possible sense, and even in the generous definition of "statements that mathematicians care about", that is going to be very heavily biased towards questions that are decidable, because the questions that are likely to be decidable are the ones that they can even reason about to begin with.
If you're a computer programmer, the CS shadow of Godel comes up _all the time_ in practice, and undecidable situations are quite common and don't really need to be carefully constructed.
This is just the drunk-in-the-streetlight situation. Things seem to be decidable everywhere we look because we look where things are likely to be decidable.
To actually get independence, we need very rigid statements that don't allow any simple way to fudge a solution or counterexample. If anything, statements that mathematicians (and programmers) care about are biased toward undecidability, simply because they're extremely biased toward nontriviality. We put in the hard work of building towers of rigid definitions to that effect.
Hilbert's incidence geometry, for instance, is consistent and complete. It's just rather small.
One of the more interesting bits about this is understanding what "sufficiently expressive" means. The Naturals are incomplete, the Reals aren't.
As I understand it, the proof of the Lowenheim-Skolem theorem requires the axiom of choice, but the proof of the two Godel theorems does not. That would make a difference for people who are doubtful about the axiom of choice.
No, this was known before the incompleteness theorem, ref Löwenheim–Skolem theorem.
The Godel theorems apply to any first-order axiom system, regardless of whether it has an infinite model or not.
I stand by my claim. The key point of Gödels incompleteness is NOT that no single theory can pin down a single model, that was known before.
You might think LS would trivially demonstrate as much---"Just take P = our underlying model is countable!"---but this is not formalizable within the system itself.
[deleted]