Goedel incompleteness theorem -> apply this to "theories"
Goedel completeness theorem -> apply this to a specific "model", of the theory
So there can be "something true but not provable" in the theory, and "we cannot describe all true things about specific models", but ....what?
The completeness theorem says simply: if T is a first-order theory (list of axioms in first-order logic), any sentence true in every model of T is provable by logical deduction in T.
The first incompleteness theorem says: if T is a consistent recursively enumerable theory that can contains a sufficient amount of Peano arithmetic, then there exists a sentence which is neither true in all models nor false in all models. In other words, there is a sentence which is true in at least one model of T, and false in another.
The second incompleteness theorem says that if T can interpret Peano arithmetic, then we cannot prove the consistency of T within T.
So a tl;dr:
-Completeness: any SENTENCE true in ALL models is PROVABLE - applies to all first order theories
-1st Incompleteness: there EXISTS sentences which are TRUE in some models, FALSE in others. - Applies to theories that contain enough arithmetic
-2nd Incompleteness: if a sufficiently strong system is CONSISTENT, we CANNOT PROVE that CONSISTENCY within the system.
NB: of course, if you have a sufficiently WEAK system, like the axioms of group theory together with "FOR ALL x FOR ALL y (x=y)", then that theory would be COMPLETE and Godel's incompleteness theorem does not apply here.
But just to be clear, your summarization of the first incompleteness theorem is through the lens of model theory and therefore predicated on the completeness theorem and doesn't hold in its absence. The canonical example is second-order PA under full second-order semantics, which has only one model (this is also true of second-order ZFC). Hence there do not exist sentences of second-order PA which are true in some models and false in others.
To fully flesh out the syntactic results of Godel's incompleteness theorems and their semantic consequences when Godel's completeness theorem holds, there's the following syntactic -> semantic chains.
1st incompleteness: there exist sentences which cannot be proved within any theory containing enough arithmetic. Therefore by Godel's completeness theorem there are sentences in the theory which are satisfied by some models and whose negation are satisfied by other models.
2nd incompleteness: the sentence Con(T) corresponding to the informal sentence "the theory T is consistent" cannot be proved within the theory T itself assuming T contains enough arithmetic. Therefore by Godel's completeness theorem there are models of T where Con(T) is satisfied and models of T where Not(Con(T)) is satisfied.
As I said in another post while Godel's completeness theorem is an essentially model-theoretic result (and it is the foundation that all other model theory builds on), Godel's incompleteness theorems are fundamentally syntactic results that live in the realm of proof theory, rather than semantic ones that live in the realm of model theory, although they have deep implications for the latter.
(Also to be extraordinarily pedantic, as you point out elsewhere, a sentence is true if it is satisfied by all models. Hence technically it is a misnomer to say that a sentence is true in a given model. Rather a sentence is satisfied by a given model. But it's a common enough bit of informal terminology, but I just want to point it out for people who aren't familiar with model theory so that they don't get tripped up trying to square different formal definitions of "true.")
Goedel's completeness theorem tells you that for a theory in first-order logic, there's a model that corresponds exactly to that theory: anything that's true in that model can be proven in the theory, and vice versa.
Godel's incompleteness theorem tells you that there's no such model for any system that includes the usual "full" version of arithmetic. A model is a very concrete thing, so any question you ask about the model has an answer - but you don't necessarily know whether that answer is a fact about the theory (i.e. true in all models of the theory - which any statement that's provable would be) or just a fact about that particular model.
It's like if you write some C code, run it, and it prints 4. Does that mean your program always prints 4 according to the C standard? Or did your program do some undefined behaviour, and it just happened that with your particular compiler it printed 4?
Unfortunately it doesn't work if you swap our "for all models" with "there exists a model."
Take the theory of the natural numbers with the new symbol "Special" and the axiom "there exists a number n such that Special(n) holds." In every model of that theory there will be a concrete n that is Special (say 6). However, the theory will never be able to prove that a specific n is Special, precisely because it is under-specified which n it is.
> Godel's incompleteness theorem tells you that there's no such model for any system that includes the usual "full" version of arithmetic.
No in conjunction with Godel's completeness theorem, the incompleteness theorem would say rather that there is no theory that is strictly only the "full" version of arithmetic. Any theory will always be too broad and have too many models that satisfy it, only one of which is the "usual" model of arithmetic.
EDIT: Ah I see I misinterpreted your statement the first time, around, but my objections still hold with modification. Change "the theory of the natural numbers" to a far weaker theory, e.g. the theory of Presburger Arithmetic, and everything else still holds.
Hmm. So which n is special in the model that you get from the model existence theorem? Doesn't it all get somehow equivalence-classed away?
> No in conjunction with Godel's completeness theorem, the incompleteness theorem would say rather that there is no theory that is strictly only the "full" version of arithmetic. Any theory will always be too broad and have too many models that satisfy it, only one of which is the "usual" model of arithmetic.
Sure. The point is that there's always a gap between the theory and the model, an "implementation-defined" part of the model.
The model existence theorem relies on extending your original language (and therefore your theory) with a bunch of new constants. So in this case you would end up conjuring up a specific new constant symbol just for `Special`.
You then "forget" about all those constants when you retract back to your original theory and so you lose the one-to-one relationship.
So it is true that if your original theory is Henkin (i.e. there is a constant symbol witnessing every single existential statement you have) and maximally consistent, then there exists a model that coincides exactly with your theory, in particular the model that is constructed from all your constant symbols modulo equality in your theory.
But most theories are not Henkin. And moreover most theories are not maximally consistent (since that would imply completeness in the sense of Godel's incompleteness theorems). In particular the theory you get out of the model existence theorem is usually not computably enumerable, so you can't actually write down your extended theory.
So most theories do not have that nice property that they correspond exactly with the semantic properties of a model.
Also, the incompleteness theorem doesn't say anything about the nonexistence of a model. It gives the existence of at least one sentence X (for sufficiently nice theories that include enough arithmetic) such that there ARE two models where X is true in one and false in the other.
I wouldn't say that it has "nothing to do" with existence of models. It wasn't the original Goedel's formulation of the theorem, but these days, one of the most, if not the most popular statement of it is to say that "if theory T is consistent, there exists a model of it".
Let's drop "truth" for a sec.
Let's say I come up with a series of axioms about cows. They describe spots on cows, how many legs cows have, etc.
Now I come up with a sentence "all cows have spots." There are two ways of proving this sentence. One is a "semantic proof." That is I go and round up every cow and examine it and make sure they all have spots. Another way of proving this sentence is a "syntactic proof." I list out a series of axioms defining what cows are. Then I do a series of string manipulations on my axioms about cows according to an allowed ruleset to arrive at the statement "all cows have spots."
Semantic proofs are hard. They're annoying for finite groups of things and impossible to do for infinite groups of things. If possible we would like to use syntactic proofs. But syntactic proofs face two hurdles. The first is how to know we've applied our axioms correctly. For example, maybe one of my axiom is "all cows have 4 legs," and then I just conveniently define the symbol "4" to mean three. You can't really get around that problem. You kind of just have to tell people, don't mess around with the meaning of words.
The second hurdle though concerns our ruleset. That is string manipulations can be of an arbitrary form. How do I know, even if I've applied my axioms correctly, that my ruleset isn't crazy? Something like, anytime you see a sentence S, you're allowed to replace it with Not(S) if you want.
Godel's completeness theorem says for a lot of reasonable rulesets (including most of the ones we use for mathematics), semantic proofs and syntactic proofs coincide. You can decide to either go out and look at every cow or you can use your axioms about cows to move symbols on a sheet of paper around. As long as your axioms about cows capture enough information about whether cows have spots, with certain popular rulesets, you'll get the same result.
Put another way, as long as the result you're looking for is relevant to the axioms you've listed, either a semantic proof or a syntactic proof is valid.
Okay, but what about statements that aren't relevant to the axioms I've listed? Things like the weight of a cow? Or what about statements that are under-specified? For example if I just say as an axiom "some cows have spots," does that mean all cows have spots or that some don't?
Through the lens of Godel's completeness theorem this just means that our list of axioms is applicable to a lot more situations than we're giving it credit for. Our axioms don't talk about the weight of a cow? Well then they could be used for situations where cows are weightless or when they have weight. Our axioms don't specify whether all cows have spots? Well they can be used in situations where all cows have spots as well as situations where some cows don't have spots.
No biggie. That just means the only things relevant to our axioms are those properties in common across all the situations we could apply our axioms. And anything that can be semantically proved in all of these situations is also something that can be syntactically proved.
Okay so that concludes Godel's completeness theorem. Let's start going into his incompleteness theorems through the same lens.
Cows are really complicated things. They have tons and tons of different properties, so it's no surprise that our list of axioms will probably always under-specify them.
What if we strip things down to really really simple things. For example the natural numbers? Can we have a list of axioms that apply to the natural numbers and pin down every property about them?
The answer is no. Any list of axioms we come up with will always be "too broad." There are things other than the usual natural numbers (that's already a bit of a minefield to privilege one of them as being the "usual", but we'll ignore it for now) that I can present to you that also fulfill those axioms. In the same way that "some cows have spots" is mum on the issue of whether a certain cow doesn't have spots, and so can be used to describe either a herd of cows that all have spots or a herd of cows split half-and-half with spots and without spots, any system of logic that simultaneously fulfills both Godel's completeness theorem and incompleteness theorem means that it can be applied to more than one unique situation. Moreover those things that the system cannot syntactically prove are exactly those things that have different semantic proofs in different situations. For example, because I can't have a series of string manipulation steps that result in the sentence "all cows have spots" (Godel's incompleteness thereoms) there's gotta be some situations where all my axioms apply and all cows have spots and other situations where at least one cow doesn't have a spot (Godel's completeness theorem).
Hence through this lens Godel's incompleteness theorems aren't really about capital-T Truth so much as they are about our ability to completely specify infinite objects. If you and a friend decide to start listing out axioms to try to describe something like the natural numbers, no matter how many axioms you list out there is always something left unspecified.
More to the point, Godel's incompleteness theorems are theorems of proof theory, not model theory. Their proofs can be carried out with no recourse to models at all. And I think they are far less prone to being misunderstood when carried out without recourse to models and by extension without recourse to semantic truth.
You can of course choose to interpret them in model theory if you're working in a semantically complete logical system such as first-order logic with the usual semantics or second-order logic under Henkin semantics, and it is often illuminating to do so once you have those fundamentals. But I think in an informal setting those will tend only to confuse rather than clarify. And importantly the incompleteness theorems still hold in contexts where you don't really have a meaningful model theory to speak of.