Three old ones, two for and two for
.
Modus ponens. From ,
deduce
.
Generalization. From deduce
as long as
does not
occur in any of the premises used to prove
.
For
and
a proof of
from
consists of
a finite sequence of lines each of which is a logical axiom or a
member of
or is obtained from earlier lines by a deduction rule.
Write
if there is a proof of
from
.
If we allowed to be an
-structure we would have a
contradiction.
Let
and
. Then
iff
.
If
then as in the first chapter we show
that for each line in
in a proof of
from
in
fact
.
We do this inductively. The only new case is if we have used
generalization. So in proof of from
we have
and we know that
.
Note that the proof of from
did not use a free
in any hypothesis, so also our proof of
from
did not use one. Therefore we can deduce
by generalization.
If is not free in
: deduce
by the seventh axiom. Otherwise
is free in
. So in our
proof of
from
cannot have used
(as generalization was used). So
so
by the first axiom and modus
ponens.
is a set of sentences, and
a sentence. Then
implies
.
Let be a consistent set of sentences. Then
has a model.
A witness for
is
for a closed term
.
Then is complete (that is for any
either
is consistent or
consistent. For
each
add a new constant
to the language to
form
and add the sentence
to
to form
.
Then is consistent.
has witnesses for
.
Now extend to a complete
and continue inductively.
Let
in language
.
Claim. consistent. Proof of claim. Suppose
. Then some
finite
has
whence some
. Contradiction.
Claim. complete. Proof of claim. For any sentence
have
for some
as
mentions only finitely many symbols. But
complete in language
so
or
. But
. Done.
Claim. has witnesses. Proof of claim. Basically the same as
for consistency.
For closed terms
say
if
, clearly an equivalence relation. Write
for equivalence
class of
.
Let
a closed term of
.
For each
with arity
and
closed terms, set
. (Clearly well defined.)
For each
with arity
and
closed terms, set
. (Clearly well defined.)
To show that is a model for
we will show that for any sentence
we have
iff
. This is an easy
induction.
Let be a theory and
a sentence. Then
implies
.
a theory,
a sentence. Then
iff
.
a theory. If every finite subset of
has a model then so does
.
Let be a theory with an infinite model. Then
has an
uncountable model.
We want a model for . But every finite
certainly
has a model since
only mentions finitely many of the
. So by
compactness the infinite model for
exists, and it is also a model
for
.
The same trick of adding constants
shows that no set of
sentences (in the language of groups, for example) can axiomatize
(i.e. have as a model) the class of finite groups.
In other words, ``finiteness is not a first order property''. Equivalently any theory that has arbitrarily large finite models must have an infinite model (called ``overspill'').
Let be a consistent theory in a countable language (that is
countable). Then
has a countable model.
John Fremlin 2010-02-17