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.
[1] https://bayes.wustl.edu/etj/prob/book.pdf 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_logicFor 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.
* 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.
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.
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...
There is usually a 'not sufficiently complex' clause in that definition. Presburger arithmetic is complete: https://en.wikipedia.org/wiki/Presburger_arithmetic
Yup. Incompleteness is sort of a red herring. P≠NP (even though unproven) yields the real, practical, painful incompleteness.
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. "
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.
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).
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.
basically generalized the halting problem to arbitrary semantic properties.
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.
Overall I really enjoyed this article, short interviews with mathematicians and philosophers on a topic I've often thought about.
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?
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.
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.
Hilbert's incidence geometry, for instance, is consistent and complete. It's just rather small.
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.
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.
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.)
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.
At 25, Kurt Gödel proved there can never be a mathematical “theory of everything.” Columnist Natalie Wolchover explores the implications.

In 1931, by turning logic on itself, Kurt Gödel proved a pair of theorems that transformed the landscape of knowledge and truth. These “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 will always be true mathematical statements that don’t logically follow from those axioms.
I spent the early weeks of the Covid pandemic learning how the 25-year-old Austrian logician and mathematician did such a thing, and then writing a rundown of his proof in fewer than 2,000 words. (My wife, when I reminded her of this period: “Oh yeah, that time you almost went crazy?” A slight exaggeration.)
But even after grasping the steps of Gödel’s proof, I was unsure what to make of his theorems, which are commonly understood as ruling out the possibility of a mathematical “theory of everything.” It’s not just me. In Gödel’s Proof (a classic 1958 book that I heavily relied upon for my account), philosopher Ernest Nagel and mathematician James R. Newman wrote that the meaning of Gödel’s theorems “has not been fully fathomed.”
Maybe not, but six decades have passed since then. Where are we with these ideas today? Recently, I asked logicians, mathematicians, philosophers, and one physicist to discuss the meaning of incompleteness. They had plenty to say about the implications of Gödel’s strange intellectual achievement and how it changed the course of humanity’s unending search for truth.

PANU RAATIKAINEN, philosopher at Tampere University and author of the Stanford Encyclopedia of Philosophy entry on Gödel’s incompleteness theorems
Ever since the ancient Greeks, the axiomatic method has been widely taken as the ideal way of organizing scientific knowledge. The aim is to have a small number of “self-evident” basic propositions — axioms, principles, or laws — such that all truths of the field in question can be logically derived from them.
Gödel’s incompleteness theorems show with mathematical precision that this ideal necessarily fails for large parts of mathematics. The whole of mathematical truth concerning even just positive integers (1, 2, 3 …) is so perplexingly complex that it does not follow from any finite set of axioms.
This means that some mathematical problems are not even in principle solvable by our current mathematical methods. Progress may require creative conceptual innovation. As a result, mathematical truths do not make up a unified whole of equally indubitable truths; instead, their status as knowledge varies gradually from doubtless facts to increasingly uncertain hypotheses.
Raatikainen makes a good point that Gödel’s theorems muddy the waters between where objective truth ends and invented math begins. One historical way people have tried to overcome the limitations of Gödel’s theorems has been to propose additional axioms beyond the commonly accepted ones. Say you want to prove a statement with the traditional axioms, but you find that you can’t — that it is undecidable. If you add a new axiom to your starting set, you may then be able to prove the statement true. Adding a different axiom, however, and you may be able to prove it false. So whether it’s true or false depends on the choice you’ve made. Suddenly, “truth” is more contingent on one’s preferences or assumptions.

REBECCA GOLDSTEIN, philosopher and author of Incompleteness: The Proof and Paradox of Kurt Gödel
Intuitions have always played an important role in mathematics. After all, we can’t prove everything; we need to accept some truths (i.e., the axioms) without proof in order to get our proofs off the ground. But we’ve learned over the centuries that sometimes intuitions prove unreliable — so unreliable as to generate actual paradoxes — meaning we’re driven to assert out-and-out contradictions.
In the early 20th century, Bertrand Russell and Alfred North Whitehead were working on The Principles of Mathematics, which attempted to reduce arithmetic to logic. [The view that math is nothing but logic is known as “logicism.”] The work led Russell to the discovery of what came to be called Russell’s Paradox. It concerns the set of all sets that aren’t members of themselves. The paradox reveals itself when you ask: Is this set a member of itself? The contradiction: If it is, then it isn’t. And if it isn’t, then it is. (Georg Cantor, considered the founder of set theory, had already realized the contradiction back in the 1890s.)
The response of mathematicians — most forcefully David Hilbert, the leading mathematician of that time — was to rid mathematics of iffy intuitions by way of formally axiomatizing mathematics into a consistent and complete set of algorithmic, recursive rules, essentially reducing math to a mechanical game of symbol manipulation. This goal of formalization was christened the Hilbert Program.
What Gödel proved was that the Hilbert Program was unrealizable. His first incompleteness theorem states that in every formal system of mathematics that is rich enough to express arithmetic, there will be propositions that are both true and unprovable. So, although formal systems comprised of mechanical rules of symbol manipulation successfully eliminate all intuitions, they also fail to capture all that we know to be mathematically true — a knowledge enriched by intuitions concerning the infinite structures that we call numbers.
It’s fascinating that our intuitions about numbers might go beyond what we can prove.
Personally, my intuition is silent on the mathematical statement that, in the years after Gödel’s proof, made incompleteness real. It is called the continuum hypothesis, and it asserts that the set of all real numbers (the continuum) is the second-smallest infinite set after the set of natural numbers (1, 2, 3 …). It was found to be undecidable using the standard axioms of mathematics. Extra axioms can be engineered to establish it as true or false, but logicians are divided on which way to go.
A physicist I spoke with warns that the undecidability of the continuum hypothesis has implications for his field: that physicists might need to avoid the continuum altogether.

CLAUS KIEFER, physicist at the University of Cologne, author of a 2024 paper on the relevance of Gödelian incompleteness for fundamental physics
Kurt Gödel’s proof has far-reaching and unexpected consequences for mathematics. Given that physical laws are formulated in mathematical language, is it relevant for physics, too? I think yes.
Among the most important undecidable statements is the continuum hypothesis (CH), proved to be undecidable in the Gödelian sense by Paul Cohen in 1963. The name “continuum” comes from the postulate to identify the points on a line with the real numbers. But how many real numbers are there? There is an uncountable infinity of them, but can this uncountability be specified? The CH states that the real numbers form the next-smallest infinite set after the infinite set of the natural numbers, which are countable.
Now consider that the known fundamental interactions in physics are defined on a space-time continuum. The uncountable number of points associated with this continuum is responsible for various problems in physics. In Einstein’s theory of general relativity, for instance, our modern theory of gravity, it leads to singularities that prohibit the mathematical description of the universe’s origin and the interior of black holes. In the Standard Model of particle physics, described by a quantum field theory, direct calculations yield infinite results for energies and other physical quantities, which must be eliminated by a sophisticated and nonintuitive mathematical procedure.
The situation becomes more severe in the push for a final unified theory of all interactions. A unified theory should be characterized by a consistent and complete mathematical language. But if a unified theory were to describe space-time as a continuum, the CH may render the theory incomplete. Physicists have already shown that the CH leads to undecidable questions in quantum field theory, such as whether certain atomic systems have an “energy gap,” enabling them to settle into stable ground states. This undecidability stems from the fact that the calculation assumes the atoms inhabit a space-time continuum. One may argue that a more fundamental theory (with more complete axioms) could decide the question, but the final theory should not have undecidable statements. So it should not involve a continuum.
In my opinion, this situation of undecidability can only be avoided if the structure of space and time is discrete — that is, characterized by a countable infinity of points only. There are hints for a discreteness in some approaches to quantum gravity, for example string theory or loop quantum gravity, but the situation is far from clear.
It’s worth noting that on top of these troubles with the continuum hypothesis, high-energy physicists have many other reasons to think a continuous space-time is not fundamental to reality, but rather only a long-distance illusion that emerges from other parts.

JOUKO VÄÄNÄNEN, mathematician and logician at the universities of Helsinki and Amsterdam
Incompleteness is an unwelcome but unavoidable fact of life in mathematics, like irrational and transcendental numbers in number theory, or Heisenberg’s uncertainty principle in physics.
There is a kind of “Gödel barrier” that formal language cannot circumvent: The stronger the expressive power of a logic (meaning the more things you can say in the logic), the weaker is its effectiveness (meaning our ability to prove statements true or false in the logic), and the stronger the effectiveness, the weaker is the expressive power.
For example, one of the simplest logical systems is propositional logic, which lets you combine statements with operations such as “and,” “or,” and “not.” It is very effective, but its expressive power is weak. On the other end of the spectrum, there’s second-order logic, which lets you make statements about objects, properties, sets, and relationships. It has tremendous expressive power and very weak effectiveness. It is as if the “product” of effectiveness and expressive power were constant, just as in Heisenberg’s uncertainty principle, which says that there is a limit to the precision with which certain “complementary” pairs of physical properties, such as position and momentum, can be simultaneously known; in other words, the more accurately one property is measured, the less accurately the other property can be known. In logic, in a remarkable analogy, effectiveness and expressiveness are such “complementary” properties. This is the real content of Gödel’s incompleteness theorems.
We stumble forward in mathematics without any certainty of consistency or completeness. This is just how things are.
It is shocking that mathematics, which is the basis of exact sciences, lacks a foundation that can be proved to be consistent and complete. Hilbert can be forgiven for thinking that this cannot be the case. However, it is the case, as certainly as the square root of two is irrational. Mathematics has a puzzling lump of incompleteness which can be pushed from place to place but it will never disappear.
Surprisingly, Gödel himself was a little more optimistic. Here, Rachael Alvir explains that Gödel maintained the dream of a formal logical system that could settle the continuum hypothesis and all other questions about sets, the building blocks of modern mathematics. His incompleteness theorems tell us that any such system, so long as it consists of a finite list of axioms, will give rise to new statements that are undecidable within that system. But he wondered about the possibility of an infinite succession of ever-larger axiomatic systems that could settle every question.

RACHAEL ALVIR, logician and lecturer at the University of Waterloo
We have all been exposed to the general idea that Gödel killed Hilbert’s Program for thorough formalization of math. This is a common interpretation, so I was shocked when I first read Gödel’s original works. In his 1931 paper, in which the incompleteness theorems are first proven, Gödel explicitly states the opposite: “It must be expressly noted that Proposition XI (and the corresponding results for M and A) represent no contradiction of the formalistic standpoint of Hilbert.” In a footnote, he reiterates that the undecidable theorems of the 1931 paper are only undecidable relative to one system. The undecidable statements of any given logical framework can be mathematically proven to be true or false in a larger logical framework.
Gödel had no qualm with the claim that mathematics could prove or disprove every well-posed statement. Rather, Gödel took issue with Hilbert’s restrictive methods. Why should we believe there is a single, finite set of axioms, from which every truth will follow in a finite number of logical steps? 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.
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. It is simply one example of a statement which has not currently been decided, and on its own provides no reason to suspect it could not be decided in the future using new techniques. There are extensive, ongoing debates about this deep in the trenches of mathematics and philosophy.
The strongest point I wish to make is that the mathematical results, on their own, cannot settle the question. It is far from obvious that there are mathematical questions with no solution. For me, Gödel’s theorems do not show that mathematics is limited, but rather that mathematics is much wider and more powerful than Hilbert’s finitistic view.
Alvir further clarified that there are different ways the old dream of mathematical truth might be realized. One approach could be to tack on to the commonly accepted axioms a new one that settles the CH and doesn’t otherwise lead to any contradictions. Another approach is to discover a scheme for an infinitude of axioms that settles the CH and other questions. Or we could switch to a different logical system than the standard one, and in that alt-logic, settle the CH. (“My personal favorite [logical system] is called L-omega-1-omega,” Alvir told me, for anyone who wants to explore that further.) Or maybe the answer is “something totally new,” she said — “a truly novel stroke of creative genius. … We come up with radically new mathematical techniques to solve problems all the time. Why expect we won’t do the same for the CH?”
Of course, proving the CH true or false wouldn’t vanquish all undecidability.
I’m going to let Väänänen’s colleague (and wife) have the last word.

JULIETTE KENNEDY, philosopher of mathematics and mathematical logician at the University of Helsinki, editor of Interpreting Gödel: Critical Essays
It is easy to lose one’s sense of wonder at the fact that such a blindingly obvious set of axioms — the Peano axioms for arithmetic (the set of rules about the natural numbers 0, 1, 2, 3 … closely related to the system that Gödel used in his proof, such as the rule, “Every number has a successor”) — is essentially incomplete and undecidable, meaning that all axiomatizable consistent extensions are incomplete and undecidable. Hold on to that wonder! The incompleteness theorems teach us that when it comes to our attempt to master the conceptual order, whether it be in mathematics or, for that matter, in any other domain, we will always fail — and indeed, in this case more than any other, we should be glad to have failed, for failure was clearly the more interesting, the more profound, outcome.

