(disclaimer: I'm only speaking about first-order logic in what follows)
Let me describe the difference between a theory and a model: you can't really understand Gödel's incompleteness theorems without them.
I probably don't have to start quite as far back as I do, but I hope it will better set the mood.
It all begins with an alphabet. Before you can speak about anything, you have to have selected an alphabet to use. Alphabets often contain letters, like "x", "y", "z", "a", "b", and "c". They often contain numerals
1, like "0", "1", et cetera. They often contain other symbols, such as \forall,\wedge=\Rightarrow(. We usually assume that the alphabet contain infinitely many symbols.
Then, we can get into a language. A language is essentially a specification of what combinations of symbols are meaningful. It also assigns "types" to the symbols. For example, in the language of undergraduate calculus,
R denotes the type "real numbers", = is a binary relation on real numbers, t, x, y, and z are often specified to be real number variables, f, g, and h are function symbols from reals to reals, and a, b, and c are real number constants.
Now that we have a language, we can speak about the
sentences of that language. For example, a sentence in the language of Euclidean geometry might be:
For any points P and Q: P = Q or there exists a line L such that P and Q lie on L.
Well, actually we might say it in a much more stuffy way -- if we let p and q be variable symbols of type "point", l be a variable symbol of type "line", and I be a ternary relation that operates on a point, a point, and a line, then:
\forall p: \forall q: p = q \vee \exists l: I p q l
is a sentence. Of course, we like to think of this sentence as being the one that says given any two distinct points, there exists a unique line containing those two points.
Now, a theory is just a collection of statements from a language. Generally, we specify a theory by listing some statements which we call
axioms, and then say that the theory is the collection of all statements that can be deduced from the axioms. (By the rules of logic that you select to use for your theory)
(Please note that I've said absolutely nothing about truth, thus far)
This is all very abstract -- we like things to be concrete! We would like the type of "points" to actually mean something, such as the collection of all of the things we would like to call a point in Euclidean geometry!
So, we move on to the concept of a model. A model is simply a way to give "meaning" to the components of a language. For example, a model in the language of Euclidean geometry is an actual set of points, an actual set of lines, and the appropriate relation symbols on those sets.
We say that we have a
model of a theory if the statements of the theory are actually true in the model. For example, we can actually look into our two sets of lines and points, and look at our ternary relation "incidence", and decide if the statement \forall p: \forall q: p = q \vee \exists l: I p q l is true in our model!
In general, we can talk about modelling any set of statements. For example, we might merely want to model the
axioms of a theory, rather than the whole theory itself.
There are lots of questions you might ask about these concepts:
(1) Is every statement in the language either provable or disprovable from the axioms? (this is one sense of completeness)
The content of Gödel's first incompleteness theorem is that the answer
must be "no" for most systems of interest. Any theory sufficiently capable of encoding the notion of the arithmetic of the natural numbers (and satisfying certain other conditions, such as having finitely many axioms)
must be an incomplete theory.
This is popularly, and misleadingly, characterized by saying "There must be a true statement that cannot be proven". The important thing to note is that provability is a property of the theory, but truth is a property of the
model.
When I say "P is a true statement about natural numbers, but cannot be proven from the axioms", I mean that P is true
in a particular model of the natural numbers. There must also exist some other model of the natural numbers in which P is false.
Now, this isn't true for all theories of interest. Paradoxically, we have Tarski's theorem that says the theory of the arithmetic of the
real numbers
is complete! (The resolution is that while the real numbers contains the natural numbers, there is nothing in the theory of real numbers that allows one to speak of the notion of being a natural number)
(2) If a statement is provable from the axioms, must it be true in every model of those axioms? (soundness)
Intuitively speaking, this asks "If I can prove it, must it be true?" The answer to this question is
yes!
In other words, if you have a model the axioms of a theory, it must actually be a model the entire theory.
(3) If a statement is true in every model of the axioms, must it be provable from the axioms? (another meaning of completeness)
Intuitively speaking, this asks "If it must be true, can I prove it?" The answer to this question is also
yes! That is the content of Gödel's completeness theorem.
(4) If collection of statements is consistent, must it have a model?
The answer is, again,
yes. In fact, via the compactness theorem (which essentially says that any contradiction only takes finitely much work to derive), this one let's us do some very weird, but cool things with formal logic. (e.g. nonstandard analysis)
I'm less clear on the precise meaning of Gödel's second incompleteness theorem -- I know ahrkron has given the right intuitive explanation, but I don't know it's precise meaning.
1: I did
not say numbers! A numeral is just a symbol, devoid of any meaning.
