4Predicate logic
II Logic and Set Theory
4.3 Syntactic implication
Again, to define syntactic implication, we need axioms and deduction rules.
Definition (Axioms of predicate logic). The axioms of predicate logic consists
of the 3 usual axioms, 2 to explain how = works, and 2 to explain how
∀
works.
They are
1. p ⇒ (q ⇒ p) for any formulae p, q.
2. [p ⇒ (q ⇒ r)] ⇒ [(p ⇒ q) ⇒ (p ⇒ r)] for any formulae p, q, r.
3. (¬¬p ⇒ p) for any formula p.
4. (∀x)(x = x) for any variable x.
5.
(
∀x
)(
∀y
)
(
x
=
y
)
⇒
(
p ⇒ p
[
y/x
])
for any variable
x, y
and formula
p
,
with y not occurring bound in p.
6.
[(
∀x
)
p
]
⇒ p
[
t/x
] for any formula
p
, variable
x
, term
t
with no free variable
of t occurring bound in p.
7.
[(
∀x
)(
p ⇒ q
)]
⇒
[
p ⇒
(
∀x
)
q
] for any formulae
p, q
with variable
x
not
occurring free in p.
The deduction rules are
1. Modus ponens: From p and p ⇒ q, we can deduce q.
2.
Generalization: From
r
, we can deduce (
∀x
)
r
, provided that no premise
used in the proof so far had x as a free variable.
Again, we can define proofs, theorems etc.
Definition (Proof). A proof of
p
from
S
is a sequence of statements, in which
each statement is either an axiom, a statement in
S
, or obtained via modus
ponens or generalization.
Definition (Syntactic implication). If there exists a proof a formula
p
form a
set of formulae S, we write S ⊢ p “S proves t”.
Definition (Theorem). If
S ⊢ p
, we say
p
is a theorem of
S
. (e.g. a theorem of
group theory)
Note that these definitions are exactly the same as those we had in propo-
sitional logic. The only thing that changed is the set of axioms and deduction
rules.
Example. {x = y, x = z} ⊢ y = z.
We go for x = z giving y = z using Axiom 5.
1. (∀x)(∀y)((x = y) ⇒ (x = z ⇒ y = z)) Axiom 5
2. [(∀x)(∀y)((x = y) ⇒ (x = z ⇒ y = z))] ⇒ (∀y)(x = y ⇒ y = z) Axiom 6
3. (∀y)((x = y) ⇒ x = z ⇒ y = z) MP on 1, 2
4. [(∀y)((x = y) ⇒ x = z ⇒ y = z)] ⇒ [(x = y) ⇒ (x = z ⇒ y = z) Axiom 6
5. (x = y) ⇒ [(x = z) ⇒ (y = z)] MP on 3, 4
6. x = y Premise
7. (x = z) ⇒ (y = z) MP 6, 7
8. x = z Premise
9. y = z MP on 7, 8
Note that in the first 5 rows, we are merely doing tricks to get rid of the
∀
signs.
We can now revisit why we forbid
∅
from being a structure. If we allowed
∅
,
then (
∀x
)
⊥
holds in
∅
. However, axioms 6 states that ((
∀x
)
⊥
)
⇒ ⊥
. So we can
deduce
⊥
in the empty structure! To fix this, we will have to add some weird
clauses to our axioms, or simply forbid the empty structure!
Now we will prove the theorems we had for propositional logic.
Proposition (Deduction theorem). Let
S ⊆ L
, and
p, q ∈ L
. Then
S ∪ {p} ⊢ q
if and only if S ⊢ p ⇒ q.
Proof.
The proof is exactly the same as the one for propositional logic, except
in the ⇒ case, we have to check Gen.
Suppose we have lines
– r
– (∀x)r Gen
and we have a proof of
S ⊢ p ⇒ r
(by induction). We want to seek a proof of
p ⇒ (∀x)r from S.
We know that no premise used in the proof of
r
from
S ∪{p}
had
x
as a free
variable, as required by the conditions of the use of Gen. Hence no premise used
in the proof of p ⇒ r from S had x as a free variable.
Hence S ⊢ (∀x)(p ⇒ r).
If x is not free in p, then we get S ⊢ p ⇒ (∀x)r by Axiom 7 (and MP).
If
x
is free in
p
, then we did not use premise
p
in our proof
r
from
S ∪ {p}
(by the conditions of the use of Gen). So
S ⊢ r
, and hence
S ⊢
(
∀x
)
r
by Gen.
So S ⊢ p ⇒ (∀x)r.
Now we want to show
S ⊢ p
iff
S |
=
p
. For example, a sentence that holds in
all groups should be deducible from the axioms of group theory.
Proposition (Soundness theorem). Let
S
be a set of sentences,
p
a sentence.
Then S ⊢ p implies S |= p.
Proof.
(non-examinable) We have a proof of
p
from
S
, and want to show that
for every model of S, p holds.
This is an easy induction on the lines of the proof, since our axioms are
tautologies and our rules of deduction are sane.
The hard part is proving
S |= p ⇒ S ⊢ p.
This is, by the deduction theorem,
S ∪ {¬p} |= ⊥ ⇒ S ∪ {¬p} ⊢ ⊥.
This is equivalent to the contrapositive:
S ∪ {¬p} ⊢ ⊥ ⇒ S ∪ {¬p} |= ⊥.
Theorem (Model existence lemma). Let
S
be a consistent set of sentences.
Then S has a model.
We need several ideas to prove the lemma:
(i)
We need to find a structure. Where can we start from? The only thing we
have is the language. So we start form the language. Let
A
= set of all
closed terms, with the obvious operations.
For example, in the theory of fields, we have “1 + 1”, “0 + 1“ etc in the
structure. Then (1 + 1) +
A
(0 + 1) = (1 + 1) + (0 + 1).
(ii)
However, we have a problem. In, say, the language of fields, and
S
our
field axioms, our
A
has distinct elements “1 + 0”, “0 + 1”, “0 + 1 + 0”
etc. However,
S ⊢
1 + 0 = 0 + 1 etc. So we can’t have them as distinct
elements. The solution is to quotient out by the equivalence relation
s ∼ t
if
S ⊢
(
s
=
t
), i.e. our structure is the set of equivalence classes. It is
trivial check to check that the +,
×
operations are well-defined for the
equivalence classes.
(iii)
We have the next problem: If
S
is ”field of characteristic 2 or 3“, i.e.
S
has a field axiom plus 1 + 1 = 0
∨
1 + 1 + 1 = 0. Then
S ⊢
1 + 1 = 0. Also
S ⊢
1 + 1 + 1 = 0. So [1 + 1]
= [0], and [1 + 1 + 1]
= [0]. But then our
S
has neither characteristic 2 or 3.
This is similar to the problem we had in the propositional logic case, where
we didn’t know what to do with
p
3
if
S
only talks about
p
1
and
p
2
. So we
first extend S to a maximal consistent (or complete)
¯
S.
(iv)
Next problem: Let
S
= “fields with a square root of 2”, i.e.
S
is the
field axioms plus (
∃x
)(
xx
= 1 + 1). However, there is no closed term
t
which is equivalent to
√
2
. We say we lack witnesses to the statement
(
∃x
)(
xx
= 1 + 1). So we add a witness. We add a constant
c
to the
language, and add the axiom “
cc
= 1 + 1” to
S
. We do this for each such
existential statement.
(v)
Now what? We have added new symbols to
S
, so our new
S
is no longer
complete! Of course, we go back to (iii), and take the completion again.
Then we have new existential statements to take care of, and we do (iv)
again. Then we’re back to (iii) again! It won’t terminate!
So we keep on going, and finally take the union of all stages.
Proof.
(non-examinable) Suppose we have a consistent
S
in the language
L
=
L
(Ω
,
Π). Extend
S
to a consistent
S
1
such that
p ∈ S
1
or (
¬p
)
∈ S
for each
sentence
p ∈ L
(by applying Zorn’s lemma to get a maximal consistent
S
1
). In
particular, S
1
is complete, meaning S
1
⊢ p or S
1
⊢ ¬p for all p.
Then for each sentence of the form (
∃x
)
p
in
S
1
, add a new constant
c
to
L
and add
p
[
c/x
] to
S
1
— obtaining
T
1
in language
L
1
=
L
(Ω
∪ C
1
,
Π). It is easy
to check that T
1
is consistent.
Extend
T
1
to a complete theory
S
2
⊆ L
1
, and add witnesses to form
T
2
⊆
L
2
= L(Ω ∪C
1
∪ C
2
, Π). Continue inductively.
Let
¯
S
=
S
1
∪ S
2
∪ ···
in language
¯
L
=
L
1
∪ L
2
∪ ···
(i.e.
¯
L
=
L
(Ω
∪ C
1
∪
C
2
∪ ··· , Π)).
Claim.
¯
S
is consistent, complete, and has witnesses, i.e. if (
∃x
)
p ∈
¯
S
, then
p[t/x] ∈
¯
S For some term t.
It is consistent since if
¯
S ⊢ ⊥
, then some
S
n
⊢ ⊥
since proofs are finite. But
all S
n
are consistent. So
¯
S is consistent.
To show completeness, for sentence
p ∈
¯
L
, we have
p ∈ L
n
for some
n
, as
p
has only finitely many symbols. So
S
n+1
⊢ p
or
S
n+1
⊢ ¬p
. Hence
¯
S ⊢ p
or
¯
S ⊢ ¬p.
To show existence of witnesses, if (
∃x
)
p ∈
¯
S
, then (
∃x
)
p ∈ S
n
for some
n
.
Hence (by construction of T
n
), we have p[c/x] ∈ T
n
for some constant c.
Now define an equivalence relation
∼
on closed term of
¯
L
by
s ∼ t
if
¯
S ⊢
(
s
=
t
). It is easy to check that this is indeed an equivalence relation. Let
A
be the set of equivalence classes. Define
(i) f
A
([t
1
], ··· , [t
n
]) = [ft
1
, ··· , t
n
] for each formula f ∈ Ω, α(f ) = n.
(ii) ϕ
A
=
{
([
t
1
]
, ··· ,
[
t
n
]) :
¯
S ⊢ ϕ
(
t
1
, ··· , t
n
)
}
for each relation
ϕ ∈
Π and
α(ϕ) = n.
It is easy to check that this is well-defined.
Claim. For each sentence
p
,
¯
S ⊢ p
(i.e.
p ∈
¯
S
) if and only if
p
holds in
A
, i.e.
p
A
= 1.
We prove this by an easy induction.
– Atomic sentences:
◦ ⊥:
¯
S ⊢ ⊥, and ⊥
A
= 0. So good.
◦ s
=
t
:
¯
S ⊢ s
=
t
iff [
s
] = [
t
] (by definition) iff
s
A
=
t
A
(by definition
of s
A
) iff (s = t)
A
. So done.
◦ ϕt
1
, ··· , t
n
is the same.
– Induction step:
◦ p ⇒ q
:
¯
S ⊢
(
p ⇒ q
) iff
¯
S ⊢
(
¬p
) or
¯
S ⊢ q
(justification: if
¯
S ⊢ ¬p
and
¯
S ⊢ q
, then
¯
S ⊢ p
and
¯
S ⊢ ¬q
by completeness, hence
¯
S ⊢ ¬
(
p ⇒ q
),
contradiction). This is true iff p
A
= 0 or q
A
= 1 iff (p ⇒ q)
A
= 1.
◦
(
∃x
)
p
:
¯
S ⊢
(
∃x
)
p
iff
¯
S ⊢ p
[
t/x
] for some closed term
t
. This is true
since
¯
S
has witnesses. Now this holds iff
p
[
t/x
]
A
= 1 for some closed
term
t
(by induction). This is the same as saying (
∃x
)
p
holds in
A
,
because A is the set of (equivalence classes of) closed terms.
Here it is convenient to pretend
∃
is the primitive symbol instead of
∀
.
Then we can define (
∀x
)
p
to be
¬
(
∃x
)
¬p
, instead of the other way round.
It is clear that the two approaches are equivalent, but using
∃
as primitive
makes the proof look clearer here.
Hence A is a model of
¯
S. Hence it is also a model of S. So S has a model.
Again, if
L
is countable (i.e. Ω
,
Π are countable), then Zorn’s Lemma is not
needed.
From the Model Existence lemma, we obtain:
Corollary (Adequacy theorem). Let
S
be a theory, and
p
a sentence. Then
S |= p implies S ⊢ p.
Theorem (G¨odel’s completeness theorem (for first order logic)). Let
S
be a
theory, p a sentence. Then S ⊢ p if and only if S |= p.
Proof. (⇒) Soundness, (⇐) Adequacy.
Corollary (Compactness theorem). Let
S
be a theory such that every finite
subset of S has a model. Then so does S.
Proof.
Trivial if we replace “has a model” with “is consistent”, because proofs
are finite.
We can look at some applications of this:
Can we axiomatize the theory of finite groups (in the language of groups)?
i.e. is there a set of sentences T such that models of T are finite groups.
Corollary. The theory of finite groups cannot be axiomatized (in the language
of groups).
It is extraordinary that we can prove this, as opposed to just “believing it
should be true”.
Proof.
Suppose theory
T
has models all finite groups and nothing else. Let
T
′
be T together with
– (∃x
1
)(∃x
2
)(x
1
= x
2
) (intuitively, |G| ≥ 2)
– (∃x
1
)(∃x
2
)(∃x
3
)(x
1
= x
2
= x
3
) (intuitively, |G| ≥ 3)
– ···
Then
T
′
has no model, since each model has to be simultaneously arbitrarily
large and finite. But every finite subset of
T
′
does have a model (e.g.
Z
n
for
some n). Contradiction.
This proof looks rather simple, but it is not “easy” in any sense. We are
using the full power of completeness (via compactness), and this is not easy to
prove!
Corollary. Let
S
be a theory with arbitrarily large models. Then
S
has an
infinite model.
“Finiteness is not a first-order property”
Proof. Same as above.
Similarly, we have
Corollary (Upward L¨owenheim-Skolem theorem). Let
S
be a theory with an
infinite model. Then S has an uncountable model.
Proof. Add constants {c
i
: i ∈ I} to L for some uncountable I.
Let T = S
S
{“c
i
= c
j
” : i, j ∈ I, i = j}.
Then any finite
T
′
⊆ T
has a model, since it can only mention finitely many
of the
C
i
. So any infinite model of
S
will do. Hence by compactness,
T
has a
model
Similarly, we have a model for
S
that does not inject into
X
, for any chosen
set X. For example, we can add γ(X) constants, or P(X) constants.
Example. There exists an infinite field (
Q
). So there exists an uncountable
field (e.g. R). Also, there is a field that does not inject into P(P(R)), say,
Theorem (Downward L¨owenheim-Skolem theorem). Let
L
be a countable
language (i.e. Ω and Π are countable). Then if
S
has a model, then it has a
countable model.
Proof.
The model constructed in the proof of model existence theorem is count-
able.
Note that the proof of the model existence theorem is non-examinable, but
the proof of this is examinable! So we are supposed to magically know that the
model constructed in the proof is countable without knowing what the proof
itself is!