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.

There is usually a 'not sufficiently complex' clause in that definition. Presburger arithmetic is complete: https://en.wikipedia.org/wiki/Presburger_arithmetic

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 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.

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.

      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

  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.

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).