Predicate Logic (1)
The need for a richer language
Predicate logic as a formal language
– terms — variables, functions
– formulas — predicates, quantifiers
– free and bound variables
– substitution
Proof theory of predicate logic
– Natural deduction rules
Slide 1 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
The Need for a Richer Language
Propositional Logic:
Study of declarative sentences, statements about the world which can be
given a truth value
Dealt very well with sentence components like: not, and, or, if then
Limitations: cannot deal with modifiers like there exists, all, among, only.
Example: “Every student is younger than some instructor.”
We could identify the entire phrase with the propositional symbol p.
However, the phrase has a finer logical structure. It is a statement about the
following properties:
– being a student
– being an instructor
– being younger than somebody else
Slide 2 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Predicates, Variables and Quantifiers
Properties are expressed by predicates. S, I, Y are predicates.
S andy : Andy is a student.
I paul : Paul is an instructor.
Y andy paul : Andy is younger than Paul.
Variables are placeholders for concrete values.
S x : x is a student.
I x : x is an instructor.
Y x y : x is younger than y.
Quantifiers make possible encoding the phrase:
“Every student is younger than some instructor.”
Two quantifiers: — forall, and — exists.
Encoding of the above sentence:
x S x y I y Y x y
Slide 3 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
More Examples
“No books are gaseous. Dictionaries are books. Therefore, no dictionary is
gaseous.”
We denote: B x : x is a book x B x G x x D x B x
G x : x is gaseous
D x : x is a dictionary x D x G x
“Every child is younger than his mother”
We denote: C x : x is a child x y C x M x y Y x y
M x y : x is y’s mother
Denote m x : mother of x x C x Y x m x
Using the function m to encode the “mother of” relationship
is more appropriate, since every person has a unique mother.
Slide 4 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
More Examples (2)
“Andy and Paul have the same maternal grandmother”
x y u v M x y M y a M u v M v p x u
We have introduced a new, special predicate: equality.
Alternative representation:
m m a m m p
Consider the relationship B x y : x is the brother of y. This relationship
must be encoded as a predicate, since a person may have more than one
brother.
Slide 5 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Predicate Logic as a Formal Language
Two sorts of “things” in a predicate formula:
Objects such as a (Andy) and p (Paul). Function symbols also refer to
objects. These are modeled by terms.
Expressions that can be given truth values. These are modeled by formulas.
A predicate vocabulary consists of 3 sets:
Predicate symbols P ; Each predicate and function symbol comes with a fixed
Function symbols F ; arity (i.e. number of arguments)
Constants C.
Elements of the formal language of predicate logic:
Terms
Formulas
Free and bound variables
Substitution
Slide 6 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Terms
Definition: Terms are defined as follows:
Any variable is a term;
Any constant in C is a term;
If t1 , ,tn are terms and f F has arity n, then f t1 tn is a term;
Nothing else is a term.
Backus-Naur definition: t :: x c f t t where x represents variables, c
represents constants in C , and f represents function in F with arity n.
Remarks:
The first building blocks of terms are constants and variables.
More complex terms are built from function symbols using previously buit
terms.
The notion of terms is independent on the sets C and F .
Slide 7 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Formulas
Definition: We define the set of formulas over F P inductively, using the
already defined set of terms over F .
If P is a predicate with n 1 arguments, and t1 , ,tn are terms over F ,
then P t1 tn is a formula.
If Φ is a formula, then so is Φ.
If Φ and Ψ are formulas, then so are Φ Ψ, Φ Ψ, Φ Ψ.
If Φ is a formula and x is a variable, then x Φ and x Φ are formulas.
Nothing else is a formula.
BNF definition:
Φ :: P t1 tn Φ Φ Φ Φ Φ
Φ Φ x Φ x Φ
where P is a predicate of arity n, ti are terms, i 1
n , x is a variable.
Convention: We retain the usual binding priorities of the connectives , , , .
We add that x and x bind like .
Slide 8 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Example
Consider translating the sentence:
“Every son of my father is my brother”
Two alternatives:
“Father of” relationship encoded as a predicate.
S x y : x is the son of y.
F x y : x is the father of y.
B x y : x is the brother of y.
m: constant, denoting “myself”.
Translation: x y F x m S y x B y m
“Father of” relationship encoded as a function.
f x : father of x.
Translation: x S x f m B x m
Slide 9 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Free and Bound Variables
Definition: Let Φ be a formula in predicate logic. An occurrence of x
in Φ is free in Φ if it is a leaf node in the parse tree of Φ such that there
is no path upwards from that node x to a node x or x. Otherwise, that
occurrence x is called bound. For x Φ, we say that Φ — minus any of
its sub-formulas x Ψ, or x Ψ — is the scope of x, respectively x.
Formula: x
x P x Q x S x y
Scope of x
S
x is bound.
P Q x y
y is free.
x x free
bound
Slide 10 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Examples of Free and Bound Variables
Formula: x P x Q x
P x Q y
Parse tree:
x
Q
P Q P y
x x x
Slide 11 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Substitution
Variables are placeholders, so we must have means of replacing them with more
concrete information.
Definition: Given a variable x, a term t, and a formula Φ, we define Φ t x to be
the formula obtained by replacing each free occurrence of variable x in Φ with t.
x P x Q x
P x Q y
f x y x is
x P x Q x
P f x y Q y
x
Q
P Q P y
x x f
x y
Slide 12 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Substitution (2)
Definition: Given a term t, a variable x, and a formula Φ, we say that t
is free for x in Φ if no free x leaf in Φ occurs in the scope of y or y,
for every variable y occurring in t.
Remark: If t is not free for x in Φ, then the substitution Φ t x has
unwanted effects.
Example:
S x y P x Q y
y x is S y y P y Q y
Avoid this by renaming y into z.
S x z P x Q z
y x is S y z P y Q z
Slide 13 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Proof Theory of Predicate Logic
Natural deduction rules for propositional logic are still valid
Natural deduction rules for predicate logic:
– proof rules from propositional logic;
– proof rules for equality;
– proof rules for universal quantification;
– proof rules for existential quantification.
Quantifier equivalences
Slide 14 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Proof Rules for Equality
t1 t2 Φ t1 x
i e
t t Φ t2 x
Convention: When we write a substitution in the form Φ t x , we implicitly
assume that t is free for x in Φ.
Proof example:
x x 1 0 1 0
x 1 1 1 x 1 1 x 1 x
1 x 1 1 x premise
2 x 1 1 x 1 0 premise
3 1 x 1 1 x 0 e 1,2
Slide 15 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Proof Rules for Universal Quantification
x0
..
.
xΦ Φ x0 x
xe xi
Φ t x xΦ
Proof examples:
x P x Q x x P x x Q x P t x P x Q x
Q t
1 x P x Q x premise 1 P t premise
2 x P x premise 2 x P x Q x
premise
3 x0 P x0 Q x 0 xe1 3 p t Q t xe2
4 P x0 xe2 4 Q t e 3,1
5 Q x0 e 3,4
6 x Q x x i 3-5
Slide 16 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Proof Rules for Existential Quantification
x0 Φ x 0 x
xΦ ..
.
Φ t x χ
xi Side condition: x0
doesn’t occur in χ xe
xΦ χ
Proof examples: x P x Q x
x P x x Q x
xΦ xΦ x P x Q x
1 premise
2 P x premise
1 xΦ premise
3 x0 P x0 assumption
2 Φ x x xe1
4 P x0 Q x0 xe1
3 xΦ xi2
5 Q x0 e 4,3
6 x Q x xi5
7 x Q x x e 2,3–6
Slide 17 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
Another Example
x P x x y P x Q y y Q y
1 x P x premise
2 x y P x Q y premise
3 y0
4 x0 P x0 assumption
5 y P x0 Q y xe2
6 P x 0 Q y0 ye2
7 Q y0 6,4
8 Q y0 x e 1,4-7
9 y Q y y i 3–8
Slide 18 CS3234 — Logic and Formal Systems — Lecture 03 — 26/08/04
