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.
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.
Actually, I think your statement muddies the waters and the parent gives clearer picture for those looking for simple statement of what's going on. The background is the fellow comment: https://news.ycombinator.com/item?id=48224739. Godel's simplest (and roughly original) statement is any system of axioms strong enough to encode arithmetic is either consistent or complete. You can "Or the set of axioms is not enumerable" (as in Second Order Logic and other systems). But when one says that, one has jumped from would normally recognized as logic (finite axioms and process) to a mathematical construct with some similarities to naive logic but which "my gran pappy" would see as logic.
I mean, you could formally construct an axiom system defined to choose (via axiom of choice) and assign a truth value to each of the independent propositions of first order arithmetic logic. There, consistent and complete system but not one that's a whit closer to being in usable by anyone.
I'm not even a finitist but I think being clear what's going on with these claims is important. It's like saying "the halting problem can't be solved by finite computers but my infinite-foo hypothetical computer can solve it, gotten mention that..."
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. "
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.
> 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.
> 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.
No, this was known before the incompleteness theorem, ref Löwenheim–Skolem theorem.
The Lowenheim Skolem theorem only applies to first-order axiom systems that have an infinite model. So it would apply to the axioms for the natural numbers, yes.
The Godel theorems apply to any first-order axiom system, regardless of whether it has an infinite model or not.
I don't understand what you mean by this. Gödels two incompleteness theorems are about theories of natural numbers, so their models are infinite. I don't understand what you could mean by them applying to finite models.
I stand by my claim. The key point of Gödels incompleteness is NOT that no single theory can pin down a single model, that was known before.