Logic in Computer Science
An Introductory Course for Master Students
Wang Ji
jiwang@nudt.edu.cn
Lecture 5
Predicate Calculus
Logic in Computer Science { p.1/23
Formal Language
Logic in Computer Science { p.2/23
The need for a richer language
In P, it is not possible to express assertions
about elements of a structure.
First Order Logic is a considerably richer logic
than propositional logic, but yet enjoys many
nice mathematical properties.
Logic in Computer Science { p.3/23
Primitive Symbols of F
Improper symbols : (, ), , _, 8
Variables
Individual variables : x;y;z;
Function variables : f
n
;g
n
;h
n
;
Propositional variables : p;q;r;
Predicate variables : P
n
;Q
n
;R
n
;
Constants
Individual constants
Function constants
Propositional constants
Predicate constants
Logic in Computer Science { p.4/23
Terms
The terms of F are de ned inductively by the
following formation rules:
1. Each individual variable or constant is a term.
2. If t
1
; ;t
n
are terms and f
n
is an n-ary function
variable or constant, then f
n
t
1
; ;t
n
is a term.
Q: Formulate the de nition of the set of terms.
Q: Principle of Induction the Construction of a term.
Logic in Computer Science { p.5/23
W s
The w s of F are de ned inductively by the
following formation rules:
1. If t
1
; ;t
n
are terms and P
n
is an n-ary
predicate variable or constant, then
P
n
(t
1
; ;t
n
) is a w . Also each propositional
variable or constant is w . (W s of these forms
are called atomic w s)
2. If A is a w , so is ( A)
3. If A and B are w s, so is (A_B)
4. If A is a w and x is an individual variable, then
(8xA) is a w . (w A is the scope of 8x)
Q: Formulate the de nition of the set of w s.
Q: Principle of Induction the Construction of a w .
Logic in Computer Science { p.6/23
Abbreviations
9xA stands for 8x A
(8x 2 S)A stands for 8x(S(x) A)
(9x 2 S)A stands for 9x(S(x) ^A)
Logic in Computer Science { p.7/23
Free and Bound
1. The well formed(wf) parts of B are the
consecutive subformulas of B(including B itself)
which are w s.
2. An occurrence of a variable x in a w B is
bound i it is in a wf part of B of the form
8xC; otherwise, it is free.
3. The bound / free varibles of a w are those
which have bound / free occurrences in a w (at
di erent occurrences).
4. A w without free individual variables is said to
be a closed w .
5. A sentence is a w without free variables of any
type.
Logic in Computer Science { p.8/23
Substitution
Let be S
x
1
; ;x
n
t
1
; ;t
n
.
1. (A) = S
x
1
; ;x
n
t
1
; ;t
n
A if A is atomic. (the result of
simultaneously substituting t
i
for x
i
for
1 i n at all)
2. ( B) = (B)
3. (B_C) = (B) _ (C)
4. (8xB) =
8
<
:
8x (B) if y 62 fx
1
; ;x
n
g
8xS
x
1
; ;x
i 1
;x
i+1
; ;x
n
t
1
; ;t
i 1
;t
i+1
; ;t
n
B if x = x
i
Logic in Computer Science { p.9/23
Substitution
Let be S
p
1
; ;p
n
A
1
; ;A
n
.
1. (A) =
8
<
:
A if A 62 fp
1
; ;p
n
g
A
i
if A = p
i
(1 i n)
if A is
atomic.
2. ( B) = (B)
3. (B_C) = (B) _ (C)
4. (8xB) = 8x (B)
Logic in Computer Science { p.10/23
t is free for x in A
t is free for x in A i no free occurrence of x in
A is in a wf part of A of the form 8yB, where y
is free variable of t.
C is free for p in A i no occurrence of p in A is
in a wf part of A of the form 8yB, where y is
free variable of C.
Logic in Computer Science { p.11/23
Unique Readability
De ne a function K on the symbols such that for a
symbol s, K(s) = 1 n, where n is the number of
terms which must follow s to obtain a term.
K(s) = 1 for individual variables or constants
K(s) = 1 n for n-ary function variables or constants
Extend K to the set of strings by
K(s
1
s
n
) = K(s
1
) + +K(s
n
)
Logic in Computer Science { p.12/23
Unique Readability for Terms
1. For any term t, K(t) = 1
2. Any terminal segment of a term is a
concatenation of one or more terms.
3. No proper initial segment of a term is itself a
term.
4. The set of terms is freely generated from the set
of individual variables and constants by the F
f
operations.
Logic in Computer Science { p.13/23
Unique Readability for W s
K(() = 1 K()) = 1
K(8) = 1 K( ) = 0 K(_) = 1
K(P) = 1 n for n-ary predicate variables or
constants.
1. For any w A, K(A) = 1
2. For any proper initial segment A
0
of a w A,
K(A
0
) < 1.
3. No proper initial segment of a w is itself a w .
4. The set of w s is freely generated from the set
of atomic w s by the the operations , _ and 8.
Logic in Computer Science { p.14/23
First Order Theory
The elementary theory of additive abelian group
G1 8x(x = x)
G2 8x8y8z(x = y (x = z y = z))
G3 8x8y8z(x = y x+z = y +z)
G4 8x8y8z(x+ (y +z) = (x+y) +z)
G5 8x(x+ 0 = x)
G6 8x9y(x+y = 0)
G7 8x8y(x+y = y +x)
Logic in Computer Science { p.15/23
Proof Theory
Logic in Computer Science { p.16/23
Axiom Schemata for F
Axiom Schema 1 A_A A
Axiom Schema 2 A (B_A)
Axiom Schema 3 A B (C _A (B _C))
Axiom Schema 4 8xA S
x
t
A where t is a term
free for the individual variable x in A
Axiom Schema 5 8x(A_B) (A_8xB)
provided that x is not free in A
Logic in Computer Science { p.17/23
Rules of Inference
Modus Ponens (MP)
A; A B
B
Generalization (Gen)
A
8xA
Logic in Computer Science { p.18/23
Proof
A proof in F of a w A is a nite sequence
A
1
;A
2
; ;A
m
of w s such that
A
m
is A and
for each j(1 j m) at least one the following
conditions is satis ed:
1. A
j
is an axiom;
2. A
j
is inferred by MP from w s A
i
and A
k
,
where i<j and k<j;
3. A
j
is inferred by Gen from A
i
where i<j.
Logic in Computer Science { p.19/23
‘
‘A i A has a proof in F.
If ‘
P
A, then ‘
F
A.
Logic in Computer Science { p.20/23
Tautologous
De nition The w A is a substitution instance of
a tautology, or is tautologous i these is a
tautology B(of P) such that
A = S
p
1
p
n
C1 C
n
B
Rule P
1. If A is tautologous then ‘A.
2. If ‘ A
1
; ‘ A
n
, and if A
1
^ ^A
n
B
is tautologous, then ‘B.
Logic in Computer Science { p.21/23
Let (A) be the result of erasing all quanti ers in A
and replacing each occurrence of an atomic w in A
by the propositional variable p.
1. If A is atomic, (A) = p
2. ( A) = (A)
3. (A_B) = (A) _ (B)
4. (8xA) = (A)
Logic in Computer Science { p.22/23
Consistency of E
Lemma If ‘A, then j=
P
(A).
Consistency Theorem F is absolutely consistent
and consistent with respect to negation.
Logic in Computer Science { p.23/23