5 ms·

What Do Gödel's Incompleteness Theorems Mean?

163 points by baruchel 4mo ago

hybrid_study 4mo ago
It may mean our brains are not currently equipped to understand the universe.
marojejian 4mo ago
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.
- lioeters 4mo ago
  That part you quoted was interesting to me too. I remember once re-reading the incompleteness theorems - where it talks about a "finite set of axioms", it seemed there may be a loophole if we can imagine a theoretically infinite set of axioms, as a way to approach completeness. Overall I really enjoyed this article, short interviews with mathematicians and philosophers on a topic I've often thought about.
  - AndrewOMartin 4mo ago
    Some people, when confronted with a Gödel's Incompleteness Theorems, think "I know, I’ll use a theoretically infinite set of axioms." Now they have aleph-nought problems.
    - lioeters 4mo ago
      "..How about infinity plus one! Or infinite infinities!" -- Every child who learns about infinity for the first time, but also serious mathematicians in philosophical struggle with the truth. And Cantor, may the angels soothe his troubled soul.
  - kakaz 4mo ago
    [dead]
- joe_the_user 4mo ago
  I think the combination of Godel's completeness theorem and Godel's incompleteness theorem stakes out a position in between "truth absolutism" (everything certainly knowable etc) and "truth nihilism" (nothing is truly knowable with any certainty). Which I think is great. Thing, however, is that a lot of philosophers and mathematicians fall into one of these views of truth and so you see people constantly fighting, chaffing at the bit against, this middle ground, claiming it "satisfies nobody" etc. Well, it satisfies me quite a bit.
- whattheheckheck 4mo ago
  I wonder if thats why agile is best. We can never fully "prove" the program as theory building
brookst 4mo ago
I don’t think we’ll ever entirely know what they mean.
watershawl 4mo ago
It hints at something fundamental to how the universe works, in that there is always an adjacent possible.
MrDrDr 4mo ago
> “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 https://en.wikipedia.org/wiki/Presburger_arithmetic
- __MatrixMan__ 4mo ago
  Right, you need to be able to construct numbers for Gödel's proof to apply. Hilbert's incidence geometry, for instance, is consistent and complete. It's just rather small.
svantana 4mo ago
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.
- lacewing 4mo ago
  Right, if you're a software engineer, the realization that the two theorems are nearly-equivalent really takes the air out of a lot of the existential philosophizing around Gödel's incompleteness. 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.
  - mspn 4mo ago
    [dead]
  - cobbal 4mo ago
    I think that's selling the theorems a little short. A math system with arithmetic is equal to, or more powerful than, a computer. For an example, even classical logic comes with the law of excluded middle that can say (internally) if a program halts or not. Incompleteness applies to all the stronger systems as well.
    - voxl 4mo ago
      There is no logic that is more expressive than a Turing machine. In fact, just about every logic you know can only expressive necessarily terminating programs. There is a bit of an issue on what exactly someone means by expressive, but if we're talking programs that compute outputs from inputs (without caring about the invariants imposed on said programs) then this holds.
- 4mo ago
seanhunter 4mo ago
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/pure-mathematics-formalisation-msc/ https://www.imperial.ac.uk/study/courses/postgraduate-taught...
- scott_meyer 4mo ago
  Proof by contradiction requires finding a single contradiction. Practical utility just requires that contradiction be infrequent enough.
- random3 4mo ago
  This is more like the popular lay take that are more or less confused about the meaning and implications of the theorems. The fact is that the implications are real yet more nuanced than this - something the article touched on. 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.
- jolt42 4mo ago
  We really want to believe that we can understand everything, yet we know we cannot.
- dehsge 4mo ago
  At the same time if you imagine a machine that can associate different maths. Would said machine encounter undecidable statements more frequently? 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?
eimrine 4mo ago
Is it releteble to Logic? I have heard that Economy is a subset of Logic, so is this theorem relatable to Economy?
- AndrewOMartin 4mo ago
  Only in the sense that Economists speak entirely in statements that are unprovable.
bo1024 4mo ago
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.
- danbruc 4mo ago
  That is interesting, I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so. But if it that is not the case and there always exist models where the theorem is true and false, that makes it sound to me, like the incompleteness theorem is not really about proving things. With that it sounds more like the inability of a sufficiently complex set of axioms to only admit isomorphic models, i.e. have all possible models agree on all expressible theorems. Makes the entire thing sound almost trivial, of course you can not prove what does not follow from the axioms.
  - pdonis 4mo ago
    > I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so. 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.
alan-crowe 4mo ago
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.
- bananaflag 4mo ago
  > 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. Yup. Incompleteness is sort of a red herring. P≠NP (even though unproven) yields the real, practical, painful incompleteness.
  - 4mo ago
retrocryptid 4mo ago
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_logic
hughw 4mo ago
From E.T. Jaynes' Probability Theory [1] : 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 https://bayes.wustl.edu/etj/prob/book.pdf
remywang 4mo ago
The best way to understand the theorems is to try to understand the proofs, and the short book “Gödel’s proof” by Nagel and Newman is excellent for that. Just like Douglas Hofstadter wrote in the foreword, I found the book an absolute page turner and finished in one afternoon.
kazinator 4mo ago
Gödel's Incompleteness means that formal systems that are sufficiently expressive can be used to write down new kinds of statements that can neither be derived nor contradicted from their existing axioms. Those statements can be adapted as new axioms. Unfortunately, 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).
- pdpi 4mo ago
  > formal systems that are sufficiently expressive One of the more interesting bits about this is understanding what "sufficiently expressive" means. The Naturals are incomplete, the Reals aren't.
immanuwell 4mo ago
[dead]

163 points by baruchel 4mo ago

It may mean our brains are not currently equipped to understand the universe.

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.

lioeters 4mo ago
That part you quoted was interesting to me too. I remember once re-reading the incompleteness theorems - where it talks about a "finite set of axioms", it seemed there may be a loophole if we can imagine a theoretically infinite set of axioms, as a way to approach completeness. Overall I really enjoyed this article, short interviews with mathematicians and philosophers on a topic I've often thought about.
- AndrewOMartin 4mo ago
  Some people, when confronted with a Gödel's Incompleteness Theorems, think "I know, I’ll use a theoretically infinite set of axioms." Now they have aleph-nought problems.
  - lioeters 4mo ago
    "..How about infinity plus one! Or infinite infinities!" -- Every child who learns about infinity for the first time, but also serious mathematicians in philosophical struggle with the truth. And Cantor, may the angels soothe his troubled soul.
- kakaz 4mo ago
  [dead]
joe_the_user 4mo ago
I think the combination of Godel's completeness theorem and Godel's incompleteness theorem stakes out a position in between "truth absolutism" (everything certainly knowable etc) and "truth nihilism" (nothing is truly knowable with any certainty). Which I think is great. Thing, however, is that a lot of philosophers and mathematicians fall into one of these views of truth and so you see people constantly fighting, chaffing at the bit against, this middle ground, claiming it "satisfies nobody" etc. Well, it satisfies me quite a bit.
whattheheckheck 4mo ago
I wonder if thats why agile is best. We can never fully "prove" the program as theory building

brookst 4mo ago

I don’t think we’ll ever entirely know what they mean.

watershawl 4mo ago

It hints at something fundamental to how the universe works, in that there is always an adjacent possible.

MrDrDr 4mo ago

> “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 https://en.wikipedia.org/wiki/Presburger_arithmetic

__MatrixMan__ 4mo ago
Right, you need to be able to construct numbers for Gödel's proof to apply. Hilbert's incidence geometry, for instance, is consistent and complete. It's just rather small.

svantana 4mo ago

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.

lacewing 4mo ago
Right, if you're a software engineer, the realization that the two theorems are nearly-equivalent really takes the air out of a lot of the existential philosophizing around Gödel's incompleteness. 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.
- mspn 4mo ago
  [dead]
- cobbal 4mo ago
  I think that's selling the theorems a little short. A math system with arithmetic is equal to, or more powerful than, a computer. For an example, even classical logic comes with the law of excluded middle that can say (internally) if a program halts or not. Incompleteness applies to all the stronger systems as well.
  - voxl 4mo ago
    There is no logic that is more expressive than a Turing machine. In fact, just about every logic you know can only expressive necessarily terminating programs. There is a bit of an issue on what exactly someone means by expressive, but if we're talking programs that compute outputs from inputs (without caring about the invariants imposed on said programs) then this holds.
4mo ago

seanhunter 4mo ago

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/pure-mathematics-formalisation-msc/ https://www.imperial.ac.uk/study/courses/postgraduate-taught...

scott_meyer 4mo ago
Proof by contradiction requires finding a single contradiction. Practical utility just requires that contradiction be infrequent enough.
random3 4mo ago
This is more like the popular lay take that are more or less confused about the meaning and implications of the theorems. The fact is that the implications are real yet more nuanced than this - something the article touched on. 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.
jolt42 4mo ago
We really want to believe that we can understand everything, yet we know we cannot.
dehsge 4mo ago
At the same time if you imagine a machine that can associate different maths. Would said machine encounter undecidable statements more frequently? 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?

eimrine 4mo ago

Is it releteble to Logic? I have heard that Economy is a subset of Logic, so is this theorem relatable to Economy?

AndrewOMartin 4mo ago
Only in the sense that Economists speak entirely in statements that are unprovable.

bo1024 4mo ago

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.

danbruc 4mo ago
That is interesting, I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so. But if it that is not the case and there always exist models where the theorem is true and false, that makes it sound to me, like the incompleteness theorem is not really about proving things. With that it sounds more like the inability of a sufficiently complex set of axioms to only admit isomorphic models, i.e. have all possible models agree on all expressible theorems. Makes the entire thing sound almost trivial, of course you can not prove what does not follow from the axioms.
- pdonis 4mo ago
  > I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so. 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.

alan-crowe 4mo ago

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.

bananaflag 4mo ago
> 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. Yup. Incompleteness is sort of a red herring. P≠NP (even though unproven) yields the real, practical, painful incompleteness.
- 4mo ago

retrocryptid 4mo ago

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_logic

hughw 4mo ago

From E.T. Jaynes' Probability Theory [1] : 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 https://bayes.wustl.edu/etj/prob/book.pdf

remywang 4mo ago

The best way to understand the theorems is to try to understand the proofs, and the short book “Gödel’s proof” by Nagel and Newman is excellent for that. Just like Douglas Hofstadter wrote in the foreword, I found the book an absolute page turner and finished in one afternoon.

kazinator 4mo ago

Gödel's Incompleteness means that formal systems that are sufficiently expressive can be used to write down new kinds of statements that can neither be derived nor contradicted from their existing axioms. Those statements can be adapted as new axioms. Unfortunately, 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).

pdpi 4mo ago
> formal systems that are sufficiently expressive One of the more interesting bits about this is understanding what "sufficiently expressive" means. The Naturals are incomplete, the Reals aren't.

immanuwell 4mo ago

[dead]