COMP30026 Models of Computation – Predicate Logic: Syntax
COMP30026 Models of Computation
Predicate Logic: Syntax
Bach Le / Anna Kalenkova
Lecture Week 3 Part 2 (Zoom)
Semester 2, 2021
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 1 / 25
This Lecture is Being Recorded
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 2 / 25
Where We Are Heading
“Logic is the calculus of computation.”
Zohar Manna
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 3 / 25
From Propositional to Predicate Logic
Propositional logic is useful for many purposes, but there is much in
our everyday vocabulary (and in the mathematician’s arguments)
that it cannot express.
Propositional logic as we know it was developed early in the second
half of the 19th century.
By 1879 Gottlob Frege had designed his
“Begriffschrift”, which was really the
language of first-order predicate logic,
although it looked very different, with
statements being written as tree structures.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 4 / 25
Why Predicate Logic?
Unlike propositional logic, predicate logic allows us to
finitely express statements that deal with infinite collections of
objects (integers, for example);
express relations, capturing transitive verbs and relative
pronouns.
To enable this, predicate logic uses variables that are assumed to
range over collections of individuals, such as integers, graphs, people,
or whatever, as well as quantifiers.
Propositional letters become generalised to predicates, that is,
functions that map tuples of individuals to f or t.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 5 / 25
Expressiveness of Predicate Logic: Samples
No emus fly: ∀x (Emu(x)⇒¬Flies(x))
There are black swans: ∃x (Black(x) ∧ Swan(x))
or: ∃y (Black(y ) ∧ Swan(y ))
If all push the cart, the donkey will be happy: ∀x (P(x))⇒ H
If somebody pushes, the donkey will be happy: ∃x (P(x))⇒ H
or (strangely): ∀x (P(x)⇒ H)
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 6 / 25
Expressing Relations
Tom found Rover and returned him to Anne:
Found(tom, rover) ∧ Gave(tom, rover , anne)
Tom found a dog and gave it to Anne:
∃x (Dog(x) ∧ Found(tom, x) ∧ Gave(tom, x , anne))
Jill inhabits the house that Jack built:
∃x (House(x) ∧ Inhabits(jill , x) ∧ BuilderOf (jack, x))
Mothers’ mothers are grandmothers:
∀x , y , z ((Mother(x , y ) ∧Mother(y , z))⇒ Grandmother (x , z))
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 7 / 25
Existential and Universal Quantification
Tom found an amount of money and gave it to Red Cross:
(Found(tom, $1) ∧ Gave(tom, $1, redcross)) ∨
(Found(tom, $2) ∧ Gave(tom, $2, redcross)) ∨
…
Existential quantification, ∃, is generalised ∨.
Universal quantification, ∀, is generalised ∧.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 8 / 25
Sidebar: Other Variable Binders
∑100
i=1 i
2 is another example of variable binding.
Similarly with the lambda term λx . x2 + 1, or in Haskell notation
\x -> x^2 + 1
A lambda term allows us to create a function without giving it a
name. This is surprisingly useful.
Mathematicians sometimes talk about “the function x2 + 1”, but
really that notation is ambiguous, because it does not allow us to
distinguish, say, λx . x2 + 1 and λxy . x2 + 1.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 9 / 25
Mechanical Inference with Predicate Logic
Consider this argument:
Every shark eats a tadpole.
All large white fish are sharks.
Colin is a large white fish living in deep water.
Any tadpole eaten by a deep water fish is miserable.
Therefore some tadpole is miserable.
Later we shall see how to automate reasoning about such arguments.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 10 / 25
Our Vocabulary
The alphabet of a first-order language:
variables (x , y , z , u, v , w ,. . . )
function symbols (f , g , h, . . . , +, ·, . . . )
constants (a, b, c, . . . , 0, 1, tom, . . . )
predicate symbols (P, Q, R , A, B , . . . , <, =)
connectives
quantifiers
parentheses
(sometimes: f, t)
Each function symbol comes with an arity: a number that says how
many arguments the function takes. Each predicate symbol similarly
comes with an arity.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 11 / 25
Terminology
A term is a variable or a constant or a construction
f (t1, . . . , tn)
where n > 0, f is a function symbol of arity n, and each ti is a term.
(Or we may think of a constant as a function of arity 0.)
An atomic formula (or atom) is a construction P(t1, . . . , tn) where
n ≥ 0 and P is a predicate symbol of arity n, and each ti is a term.
Term ←→ Individual, object
Atom ←→ Assertion (false or true)
A literal is an atomic formula or its negation.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 12 / 25
Case Matters
Note carefully the convention we adopt:
A predicate starts with an upper case letter; nothing else does.
So father(ron) is a term; it denotes some object.
(Most likely we intend this to mean: “the father of Ron”)
On the other hand, Father (ron) is a formula; it denotes a truth value.
(Most likely we intend this to mean: “Ron is a father”)
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 13 / 25
First-Order Predicate Logic: Syntax
Well-formed formulas (wffs) are generated by the grammar
wff → atom
| ¬ wff
| wff ∧ wff
| wff ∨ wff
| wff ⇒ wff
| wff ⇔ wff
| wff ⊕ wff
| ∀var (wff )
| ∃var (wff )
| ( wff )
Assume precedence rules like for propositional logic.
Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 14 / 25
Bound and Free Variables
A variable which is in the scope of a quantifier (binding that variable)
is bound. If it is not bound then it is free.
A variable may occur both free and bound in a formula—witness y in
∀z (P(x , y , z) ∧ ∀y (P(f (x), z , y )))
A formula with no free variable occurrences is closed.
It is possible for scopes to have “holes”:
∀x∃y (x < y ∧ ∃x (y < x)) The last occurrence of x is bound by the closest quantifier, so the scope of ∀x is not all of ∃y (. . .). Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 15 / 25 Bound Variable Renaming and Capture The bound variable of a quantified formula is just a placeholder—its exact name is inessential. ∃x∀y (x < y ) means the same as ∃x∀z (x < z). If a variable occurs bound in a certain expression then the meaning of that expression does not change when all bound occurrences of that variable are replaced by another one. However, to avoid variable capture, we cannot change the variable bound by ∀y to a variable in an enclosing scope: ∃x∀y (x ≤ y ) is very different to ∃x∀x (x ≤ x). Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 16 / 25 From English to Predicate Logic Introduce symbols for predicates. Sentence: “He is a man.” Predicate: is a man Symbol: M( ) “x is a man”, M(x), cannot be assigned a truth value. Kim is a man, M(kim), can be assigned a truth value. Sentence: “Alice is taller than Kim” T (alice, kim) Quantifier examples: “Every human is mortal” ∀x (Human(x)⇒Mortal(x)) “Some cat is mortal” ∃x (Cat(x) ∧Mortal(x)) Note: Very common to use ⇒ with ∀ and ∧ with ∃. Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 17 / 25 Example Translations Let L(x , y ) stand for “x loves y”. Let I (x , y ) stand for “x is y”. L(bob, eva) Bob loves Eva ∀x L(x , eva) Everyone loves Eva (incl. Eva) ∀x (¬I (x , eva)⇒ L(x , eva)) Eva is loved by everyone else ∃x (¬I (x , bob) ∧ L(x , bob)) Someone other than Bob loves Bob ∀x (∃y L(x , y )) Everybody loves somebody ∃y (∀x L(x , y )) Someone is loved by everybody ∃x (∀y L(x , y )) Someone loves everybody Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 18 / 25 Quiz: Translate This Translate the following statement to predicate logic: Every Melburnian barracks for a footy team. Use these predicates: M(x) x is a Melburnian T (x) x is a footy team B(x , y ) x barracks for y Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 19 / 25 Quiz: Translate This Translate the following statement to predicate logic: Every Melburnian barracks for a footy team. Use these predicates: M(x) x is a Melburnian T (x) x is a footy team B(x , y ) x barracks for y ∀x (M(x)⇒∃y (T (y ) ∧ B(x , y ))) or, equivalently: ∀x ∃y (M(x)⇒ (T (y ) ∧ B(x , y ))) Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 19 / 25 Word Order Consider word order with care: “There is something which is not P”: ∃y ¬P(y ) “There is not something which is P” (“nothing is P”): ¬∃y P(y ) “All S are not P” vs “not all S are P:” ∀x (S(x)⇒¬P(x)) vs ¬∀x (S(x)⇒ P(x)) Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 20 / 25 Quantifier Order The order of different quantifiers is important. ∀x∃y is not the same as ∃y∀x . The former says each x has a y that satisfies P(x , y ); the latter says there’s an individual y that satisfies P(x , y ) for every x . But ∀x∀y is the same as ∀y∀x and ∃x∃y is the same as ∃y∃x . Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 21 / 25 Quantified Formulas as a Two-Person Game The truth or falsehood of a quantified formula can be expressed as a question of winning strategies for a two-person game. Say I make a claim (the quantified statement) and you try to disprove it. You get to supply values for the universally quantified variables. If I claim ∀x∃y P(x , y ), then you can challenge me by choosing an x and asking me to find the y that satisfies P(x , y ), but I get to know the x you chose. If I claim ∃y∀x P(x , y ), then you can challenge me by asking me to provide the y , and then you just have to find an x that does not satisfy P(x , y ), knowing the y that I chose. If I claim ∃x∃y P(x , y ), then I have to find both x and y , so it doesn’t matter what order they appear. If I claim ∀y∀x P(x , y ), then you get to pick both x and y , so again their order does not matter. Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 22 / 25 Implicit Quantifiers Often quantifiers are implicit in English. Look for nouns (especially plural) without determiners (words to indicate which members of a group are intended). “Humans are mortal” means “all humans are mortal”: ∀x (Man(x)⇒Mortal(x)) “A woman is stronger than a man” would usually mean: ∀x∀y ((Woman(x) ∧Man(y ))⇒ Stronger (x , y )) “If a girl owns a poodle, she spoils it”: ∀x∀y ((Girl(x) ∧ Poodle(y ) ∧ Owns(x , y ))⇒ Spoils(x , y )) Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 23 / 25 Reading Materials Remember, if you feel like reading more about these topics, check out the resources that are linked under “Subject Overview” (also accessible from “Modules” → “Reading Resources”). O’Donnell, Hall and Page discuss predicate logic in Chapter 7, including translations from English. In Section 7.3 they make use of a style of inference also known as “natural deduction” (not covered by us, and not examinable). A rather different introduction to predicate logic is in Makinson’s Chapter 9. The book by Jenkyns also looks good. Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 24 / 25 Next Week Tune In for More Predicate Logic We next cover the semantics of first-order predicate logic in more detail. Plus, we get ready to extend the resolution principle to predicate logic. Models of Computation (Sem 2, 2021) Predicate Logic: Syntax c© University of Melbourne 25 / 25