Logic in Computer Science
An Introductory Course for Master Students
Wang Ji
jiwang@nudt.edu.cn
Lecture 11
FOL with Equality
Logic in Computer Science { p.1/15
Syntax
Logic in Computer Science { p.2/15
F
=
F
=
= F + \ = " + 2 Axiom Schemata
Axiom Schema 6 x = x.
Axiom Schema 7 x = y (S
z
x
A S
z
y
A) where
A is an atomic w .
A rst order theory is a rst-order theory with
equality if it has a binary predicate = such that the
w s above are theorem of the theory.
Logic in Computer Science { p.3/15
Properties of \="
1. ‘ x = y y = x
2. ‘ x = y (y = z x = z)
3. ‘ x = y (S
z
x
A S
z
y
A) where x and y are free
for z in A.
4. ‘ x = y (S
z
x
t = S
z
y
t)
5. ‘ x
1
= y
1
^ ^ x
n
= y
n
f(x
1
; ;x
n
) =
f(y
1
; ;y
n
) for any n-ary function symbol f.
6. ‘ x
1
= y
1
^ ^ x
n
= y
n
(P(x
1
; ;x
n
)
P(y
1
; ;y
n
)) for any n-ary predicate symbol P.
Logic in Computer Science { p.4/15
First Order Theory with Equality
Let T be a rst-order theory with a binary predicate
constant = such that
1. ‘
T
x = x
2. ‘
T
x
1
= y
1
^ ^ x
n
= y
n
f(x
1
; ;x
n
) =
f(y
1
; ;y
n
) for any n-ary function symbol f.
3. ‘
T
x
1
= y
1
^ ^ x
n
= y
n
(P(x
1
; ;x
n
)
P(y
1
; ;y
n
)) for any n-ary predicate symbol P.
Then T is a rst order theory with equality.
Logic in Computer Science { p.5/15
9! and 9!!
9!xA stands for
9xA ^8x8y(A ^ S
x
y
A x = y)
9!!xA stands for
8x8y(A ^ S
x
y
A x = y)
where y is the rst individual variable distinct from x
and all variables which occur in A.
Logic in Computer Science { p.6/15
Sequent Rules
;A
1
; ;A
k
)
)
where, A
1
; ;A
k
are of the following forms
t = t
s
1
= t
1
^ ^ s
n
= t
n
f(s
1
; ;s
n
) =
f(t
1
; ;t
n
)
s
1
= t
1
^ ^ s
n
= t
n
^ P(s
1
; ;s
n
)
P(t
1
; ;t
n
)
Logic in Computer Science { p.7/15
Semantics
Logic in Computer Science { p.8/15
Equality-Interpretation
An interpretation [model] < D;I
0
> for a rst order
language with an equality predicate = is an
equality-interpretation [model] i I
0
(=) is the
identity relation on D.
Logic in Computer Science { p.9/15
Soundness Theorem
If M is an equality-model for a set of sentences
and ‘
F
=
A, then j=
M
A.
Logic in Computer Science { p.10/15
Elementarily Equivalent
Interpretations M and N are elementarily equivalent
i for every sentence A of F,
j=
M
A i j=
N
A
Logic in Computer Science { p.11/15
Equality-Model
Let M =< D;I
0
> be any model for Axioms 6 and
7. Then there is an equality-model N =< D
0
;I
0
0
>
such that
1. #D
0
#D, and
2. N is elementarily equivalent to M.
Logic in Computer Science { p.12/15
Completeness
1. Let be a set of sentences consistent in F
=
.
Then has a frugal equality-model.
2. Let be a set of sentences, and A be a w , of
F
=
. Then ‘
F
=
A i A is valid in all the frugal
equality-models satisfying .
Logic in Computer Science { p.13/15
Compactness
Let L
0
(F
=
). The following parts are equivalent.
1. is consistent.
2. Every nite subset of is consistent.
3. is has an equality-model.
4. Every nite subset of has an equality-model.
5. is has a frugal equality-model.
6. Every nite subset of has a frugal
equality-model.
Logic in Computer Science { p.14/15
Size of Models
Let L
0
(F
=
).
1. If has arbitrarily large nite equality-models,
then it has an in nite equality-model.
2. Lowenheim-Skolem-Tarski Theorem
If has an in nite equality-model, and is any
cardinal number such that #(L(F
=
)), then
has an equality-model of cardinality .
Logic in Computer Science { p.15/15