This is a brief post to explain an issue in response to some youtube videos and comments about Gödel's Incomplete Theorem (henceforth "GIT").
How can it be that Gödel proved that first order logic ("FOL") was complete, yet at the same time proved that decidable consistent axiomatizations of arithmetic within first order logic were necessarily incomplete? The answer lies in the fact that there are two different (yet closely related) senses of incompleteness being used here. It is important in understanding the basics of logic to understand the two different senses (not just for GIT, but in general).
One of these senses could be considered more proof-theoretic, and the other more model-theoretic. More philosophically, one of them is more epistemological, one is more metaphysical.
The first sense is the sense in which FOL is complete. To say a logic is complete is to say that the methods of proof it supplies are adequate to prove all the logically true statements in that logic. So, FOL is complete means that whenever you take a set of axioms A, and consider a sentence S, one will be able to prove S from A if and only if S's truth logically follows from A's truth. (Best to write this out formally, but I am avoiding that here).
A can be any set of sentences at all, using any "non-logical" symbols (These being the symbols that require interpretation not fixed by the logic: the predicate, function, and constant symbols).
FOL is complete in this sense, but that doesn't mean that *every* sentence you can write in FOL using a given set of non-logical symbols is true or false. That is because many senses will be neither true or false in all circumstances: they are not logical truths. Whether they are true or false depends on the non-logical interpretation given to the symbols. For example, "(x) (P(x) -> P(x))" is a logical truth, so it is provable in FOL. "(Ex) (P(x) and not P(x))" is false, so its negation is provable. However, "(Ex) P(x)" is false with some interpretations of P, and true with others, so it is neither provable nor is its negation. FOL's theorem proving techniques do all we could possible ask of them here (well, not quite, we might like them to give three answers: provably true, provably false, or not provable because it could be true or false. Unfortunately this cannot be done: FOL is thus *undecidable* (or more precisely, *semi-decidable*. Perhaps more later).
So now consider the second sense of incomplete. What we want to do with FOL is use it to investigate various things of interest to us. So we set a specific non-logical language, not just P's Q's etc. In particular, we are interested in arithmetic: the mathematical structure of the natural numbers and the basic operations on them. Traditionally studied has been the structure you get using the non-logical symbols 0,1,+, and *. First order arithmetic is the study of arithmetic using first order logic and this non-logical vocabulary (henceforth "FOA")
Now the thing about this structure, is that from our understanding of its "intended interpretation" (the meanings we give to 0,1,+,*), we expect that every statement we can make in the language will be true or false. This is essentially a semantic point. Philosophically, it is a comittment to realism about the natural numbers. Their objective existence pins down the truth of every statement about them: in particular every statement about them we can make in the language of FOA. This results in a syntactic fact. For any P in FOA, either P or ~P will be in the set of true sentences of FOA. This is what the second sense of complete amounts to: a set of sentences is called complete if for every sentence in the language in question, either P or ~P is in the set. A syntactic criterion, but motivated by a semantic, or even metaphysical, idea.
The main thing we would like to do in order study of FOA is to give an axiomatization of of the true sentences of FOA that we can "deal with". What this means precisely is arguably something that cannot be given a definite mathematical expression. A finite set would be nice, but in reality we would be happy with some set for which we can decide membership in the technical sense of "decide" provided by computability theory.
GIT then shows that no matter what set of sentences we take for an axiomatization A (in the Youtube thread, this set of sentences is called, R, and considered to be a set of rules for generating theorems in FOA), if that set of sentences is consistent (cannot derive falsehood using the rules of FOL), and decidable, then Th(R), the set of sentences that can be proved from it, is incomplete in the second sense above.
How can this be, when FOL is complete? It is because the axioms A do not suffice to totally describe the intended interpretation we have in mind, the natural number structure. No matter what set of axioms we choose, there will be some (really weird (imo)) structure that satisfies it (i.e., in which they are true) and which can be distinguished from the natural numbers. (In particular, all of these structures will have in them a lot of extra numbers larger than every integer, arranged as an infinite and even dense set of copies of the integers).
The crucial point: since FOL is complete (in the first sense), every sentence S that is true in every one of the structures that satisfy the axioms A, will in fact be provable from A. Unfortunately, though, since whatever set A we choose be satisfied by some of these weird structures, there will have to be sentences S that are true in the natural numbers, but not true in these weird structures. They are like the "(x) P(x)" above, true in some cases, not in others, so FOL cannot prove them.
What is the nature of these sentences? Well, as is popularly known, Gödel found one by using tricks derived from Liars's Paradox, but using provability instead of truth: finding a sentence that can be obliquely interpreted as asserting "I am not provable from the axioms A". But mathematically speaking, this is not a sentence of any real interest, so some have argued that although any axiomatization will not have a complete theory, Peano Arithmetic ("PA", a particularly power axiomatization) is good enough. There has been a search, to date of debatable success, for "natural" statements S that are not provable from PA. The so-called Goodstein's Theorem is one of best-known examples.
One can also explain GIT in less "metaphysical" terms, keeping more just to a proof-theoretic framework, but I believe the above is in some sense more natural and of more philosophical interest, as well as being more psychologically compelling.
Philosophically (and psychologically) an interesting issue here (imo) is our feeling that we do have an adequate understanding of the natural numbers to insist that the true theory of the natural numbers should be complete. Personally, I believe that this is nearly a rock solid intuition that has to be accomodated. GIT is then of great interest because it shows we are in at least semantic contact, if not epistemological contact, with some abstract structure that cannot be completely characterized in computation terms. If necessary I will do a second post that elaborates on this idea (in particular, laying out the strong intuition that the true theory of arithmetic is indeed complete).
After comments, this post (quick draft) will be edited for clarity where required.
