HN

Comments (49)

• Menu

  alan-crowe
  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.
• remywang
  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.
• Menu

  bo1024
  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.
• Menu

  svantana
  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.
• Menu

  marojejian
  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.
• hughw
  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
• Menu

  seanhunter
  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...
• Menu

  MrDrDr
  > “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
• Menu

  eimrine
  Is it releteble to Logic? I have heard that Economy is a subset of Logic, so is this theorem relatable to Economy?
• watershawl
  It hints at something fundamental to how the universe works, in that there is always an adjacent possible.
• retrocryptid
  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
• brookst
  I don’t think we’ll ever entirely know what they mean.
• hybrid_study
  It may mean our brains are not currently equipped to understand the universe.