My understanding is that for any system of axioms strong enough to encode arithmetic, you can have at most two of these three properties:

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

No.

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.

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.

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.

Also check out https://en.wikipedia.org/wiki/Rice%27s_theorem

basically generalized the halting problem to arbitrary semantic properties.

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.

> any nontrivial axiomatic system has statements which are true but unprovable

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

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.

Proof by contradiction requires finding a single contradiction. Practical utility just requires that contradiction be infrequent enough.

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?

We really want to believe that we can understand everything, yet we know we cannot.

> the vast vast majority of statements in any axiomatic system are going to be decidable

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.

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.

Only in the sense that Economists speak entirely in statements that are unprovable.