Logic (PHIL 2080, COMP 2620, COMP 6262) Chapter: First-Order Logic — Semantic Tableaux
Logic (PHIL 2080, COMP 2620, COMP 6262)
Chapter: First-Order Logic
— Semantic Tableaux
Pascal Bercher
Planning & Optimization
Yoshihiro Maruyama
Logic
Intelligent Agents
College of Engineering and Computer Science
the Australian National University (ANU)
30 March & 1 April 2021
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Introduction
Pascal Bercher and Yoshihiro Maruyama 1.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Recap: Predicate Logics
We now (since week 5) know Predicate Logics as a means to
express properties of and relationships between objects.
For example:
• If everyone plays football, and everyone is a goat, everyone is a
football-playing goat
• ∀x Fx ,∀x Gx ` ∀x (Fx ∧ Gx)
We know how to prove sequents involving Predicate Logics using
natural deduction.
• We “only” needed additional elimination and introduction rules for
the exists (∃) and universal (∀) quantifiers.
• Apart from that we’ve re-used the rules known from Propositional
Logics
Pascal Bercher and Yoshihiro Maruyama 2.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Recap: Semantic Tableaux
Today, we will cover Semantic Tableaux for Predicate Logics.
But first a recap on Semantic Tableaux for Propositional Logics!
If we want to prove X ` A (with X = {A1, . . . ,An}), then, we:
• label each assumption A1, . . . ,An as being true (T),
• label A as being false (F),
• simplify each formula (according to the connectives corresponding
to truth tables) thus eventually obtaining:
1 the tree is complete and each branch induces a contradiction
2 there is some complete branch (none of its formulae can be
simplified further) and that is open (no contradiction).
In case 1 the sequent is valid.
In case 2 the sequent is invalid, and we can construct an
interpretation that makes all formulae in X true, but A false
(thus proving invalidity).
Pascal Bercher and Yoshihiro Maruyama 3.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Recap: Example for a Valid Sequent
p → q, r → s ` (p ∨ r)→ (q ∨ s)
(1) T: p → q X
(2) T: r → s X
(3) F: (p ∨ r)→ (q ∨ s) X
(4) T: p ∨ r X from (3)
(5) F: q ∨ s X from (3)
(6) F: q from (5)
(7) F: s from (5)
(8) F: p from (1) (9) T: q from (1)
(10) F: r from (2) (11) T: s from (2)
(12) T: p from (4) (13) T: r from (4)
Pascal Bercher and Yoshihiro Maruyama 4.36
T: A→ B
F: A | T: B
F: A→ B
T: A , F: B
T: A ∨ B
T: A | T: B
F: A ∨ B
F: A , F: B
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Recap: Example for an Invalid Sequent
p ∨ q ` p ∧ q
(1) T: p ∨ q X
(2) F: p ∧ q X
(3) T: p from (1) (4) T: q from (1)
(5) F: p from (2) (6) F: q open! from (2)
We’ve found an open branch, as we are allowed to stop the proof!
The sequent is invalid.
The interpretation p = > (T) and q = ⊥ (F) proves that the
assumption p ∨ q can be true while the formula p ∧ q is false,
thus disproving the sequent.
But we could also expand the right branch (line (4)) to obtain the
second interpretation p = ⊥ (F) and q = > (T). (Not required.)
Pascal Bercher and Yoshihiro Maruyama 5.36
T: A ∨ B
T: A | T: B
F: A ∧ B
F: A | F: B
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Introduction to Semantic Tableaux Rules
Pascal Bercher and Yoshihiro Maruyama 6.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Note on Notation of the Rules
Recap: In Natural Deduction for Predicate Logics, we only
required these additional rules, but we were able to keep using
those for Propositional Logics.
Also for Semantic Tableaux we are keeping all the rules from
Propositional Logics!
We again just add additional rules for the existential (∃) and
universal (∀) quantifiers.
Pascal Bercher and Yoshihiro Maruyama 7.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Simplifying a true ∃ Quantifier (Intuition)
T: ∃x Fx
T: Fa
provided a is new to the branch
Why does a need to be new?
Think of the triangle ABC! If a would exist already in the branch it
would not be general (e.g., we could “accidentally” assume that
our triangle is rectangular).
Pascal Bercher and Yoshihiro Maruyama 8.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Simplifying a false ∀ Quantifier (Intuition)
F: ∀x Fx
F: Fa
provided a is new to the branch
This corresponds to the true existential quantifier!
Recall ¬∀x Fx ≡ ∃x ¬Fx
Pascal Bercher and Yoshihiro Maruyama 9.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Simplifying a true ∀ Quantifier (Intuition)
T: ∀x Fx
T: Fa, T: Fb, . . .
for all a, b, . . . in the branch (present and future!)
This rule will never be finished! If a new constant/term gets
introduced we need to apply the rule again!
“Need” means in order to show that a branch is open. If we
already obtained a contradiction, we are clearly done. (There is
never a need to continue below a contradiction within the same
branch/path.)
Pascal Bercher and Yoshihiro Maruyama 10.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Simplifying a false ∃ Quantifier (Intuition)
F: ∃x Fx
F: Fa, F: Fb, . . .
for all a, b, . . . in the branch (present and future!)
Again, this rule will never be finished! If a new constant/term gets
introduced we need to apply the rule again!
Recall from last week that ¬∃x Fx ≡ ∀x ¬Fx
Pascal Bercher and Yoshihiro Maruyama 11.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Note on Notation of the Rules
Note that the rules presented so far were only general “in spirit”,
but they were illustrated in terms of examples, since they all used
a single predicate with arity 1, Fx .
We will first do several examples and show their “correct”
(general) form later.
Pascal Bercher and Yoshihiro Maruyama 12.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Examples
Pascal Bercher and Yoshihiro Maruyama 13.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example 1
∀x(Fx ∨ Gx) `? ∀x Fx ∨ ∀x Gx
(1) T: ∀x(Fx ∨ Gx) Xa,b
(2) F: ∀x Fx ∨ ∀x Gx X
(3) F: ∀x Fx X from (2)
(4) F: ∀x Gx X from (2)
(5) F: Fa from (3)
(6) F: Gb from (4)
(7) T: Fa ∨ Ga X from (1)
(8) T: Fb ∨ Gb X from (1)
(9) T: Fa from (7) (10) T: Ga from (7)
(11) T: Fb open! from (8) (12) T: Gb from (8)
Pascal Bercher and Yoshihiro Maruyama 14.36
T: ∀x Fx
T: Fa, T: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
F: ∀x Fx
F: Fa
if a is new to
the branch
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example 1 (cont’d)
So? Is ∀x(Fx ∨ Gx) ` ∀x Fx ∨ ∀x Gx valid?
Let’s see… Not all branches are contradictory.
Thus, there is an open branch:
(5) F: Fa from (3)
(6) F: Gb from (4)
(10) T: Ga from (7)
(11) T: Fb from (8)
So we can extract an interpretation for the formular in Predicate
Logics. (Note that the formal definition of interpretations will be
introduced later by by Yoshi.) The interpretation answers for
which objects F and G is true:
• F is true for exactly b
• G is true for exactly a
• Thus, showing that there is an interpretation that makes the
assumption true, but the formula false!
→ So the sequent is invalid!
Pascal Bercher and Yoshihiro Maruyama 15.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example 2
∃x Fx ,∃x Gx `? ∃x (Fx ∧ Gx)
(1) T: ∃x Fx X
(2) T: ∃x Gx X
(3) F: ∃x (Fx ∧ Gx) Xa,b
(4) T: Fa from (1)
(5) T: Gb from (2)
(6) F: Fa ∧ Ga X from (3)
(7) F: Fb ∧ Gb X from (3)
(8) F: Fa from (6) (9) F: Ga from (6)
(10) F: Fb open! from (7) (11) F: Gb from (7)
Pascal Bercher and Yoshihiro Maruyama 16.36
T: ∃x Fx
T: Fa
if a is new to
the branch
F: ∃x Fx
F: Fa, F: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example 2 (cont’d)
So? Is ∃x Fx , ∃x Gx `? ∃x (Fx ∧ Gx) valid?
Let’s see… Not all branches are contradictory.
Thus, there is an open branch:
(4) T: Fa from (1)
(5) T: Gb from (2)
(9) F: Ga from (6)
(10) F: Fb from (7)
So we can extract an interpretation for the formular in Predicate
Logics. (Note that the formal definition of interpretations will be
introduced later by by Yoshi.) The interpretation answers for
which objects F and G is true:
• F is true for exactly a
• G is true for exactly b
• Thus, showing that there is an interpretation that makes the
assumption true, but the formula false!
→ So the sequent is invalid!
Pascal Bercher and Yoshihiro Maruyama 17.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example by de’Morgan
Intended to show how Predicate Logics goes beyond Propositional
Logics:
All horses are animals.
Therefore, any horse’s head is an animal head!
We formalize this in terms of Predicate Logics.
Instead of:
“any horse’s head is an animal head”
We formalize that as: “each part of a horse is part of an animal”
∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy))
Thus we get:
∀x Hx → Ax ` ∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy))
Pascal Bercher and Yoshihiro Maruyama 18.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example 3
∀x Hx → Ax ` ∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy))
(1) T: ∀x Hx → Ax
Xb
(2) F: ∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy)) X
(3) F: ∃y(Hy ∧ Pay)→ ∃y(Ay ∧ Pay) X from (2)
(4) T: ∃y(Hy ∧ Pay) X from (3)
(5) F: ∃y(Ay ∧ Pay)
Xb
from (3)
(6) T: Hb ∧ Pab X from (4)
(7) T: Hb from (6)
(8) T: Pab from (6)
(9) T: Hb → Ab from (1)
(10) F: Hb from (9) (11) T: Ab from (9)
(12) F: Ab ∧ Pab
X
from (5)
(13) F: Ab from (12) (14) F: Pab from (12)
Pascal Bercher and Yoshihiro Maruyama 19.36
T: ∀x Fx
T: Fa, T: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
F: ∀x Fx
F: Fa
if a is new to
the branch
F: ∃x Fx
F: Fa, F: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
T: ∃x Fx
T: Fa
if a is new to
the branch
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example 3
∀x Hx → Ax ` ∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy))
(1) T: ∀x Hx → Ax Xb
(2) F: ∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy)) X
(3) F: ∃y(Hy ∧ Pay)→ ∃y(Ay ∧ Pay) X from (2)
(4) T: ∃y(Hy ∧ Pay) X from (3)
(5) F: ∃y(Ay ∧ Pay) Xb from (3)
(6) T: Hb ∧ Pab X from (4)
(7) T: Hb from (6)
(8) T: Pab from (6)
(9) T: Hb → Ab from (1)
(10) F: Hb from (9) (11) T: Ab from (9)
(12) F: Ab ∧ Pab X from (5)
(13) F: Ab from (12) (14) F: Pab from (12)
Pascal Bercher and Yoshihiro Maruyama 19.36
All branches are contradictory. Sequent is valid!
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Example 3 (Again with a different Order)
∀x Hx → Ax ` ∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy))
(1) T: ∀x Hx → Ax Xb
(2) F: ∀x(∃y(Hy ∧ Pxy)→ ∃y(Ay ∧ Pxy)) X
(3) F: ∃y(Hy ∧ Pay)→ ∃y(Ay ∧ Pay) X from (2)
(4) T: ∃y(Hy ∧ Pay) X from (3)
(5) F: ∃y(Ay ∧ Pay) Xb from (3)
(6) T: Hb ∧ Pab X from (4)
(7) T: Hb from (6)
(8) T: Pab from (6)
(9) F: Ab ∧ Pab X from (5)
(10) F: Ab from (9)
(12) T: Hb → Ab X from (1)
(11) F: Pab from (9)
(13) F: Hb from (12) (14) T: Ab from (12)
Pascal Bercher and Yoshihiro Maruyama 20.36
All branches are contradictory. Sequent is valid!
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Rules
Pascal Bercher and Yoshihiro Maruyama 21.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Note for Rule on false Existential and true Universal
Recall the rules for false existentials and true universals:
They state that you only “use” constants which are already there.
Sometimes, however, there one no such constants! Then, you
are also allowed to create a new one.
Pascal Bercher and Yoshihiro Maruyama 22.36
F: ∃x Fx
F: Fa, F: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
T: ∀x Fx
T: Fa, T: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Rules For Existential Quantifiers
Pascal Bercher and Yoshihiro Maruyama 23.36
F: ∃x Fx
F: Fa, F: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
X , F: ∃x A
X , F: ∃x A, F: Aax
for a in X or A
≡
T: ∃x Fx
T: Fa
if a is new to
the branch
X , T: ∃x A
X , T: Aax
for a not in X or A
≡
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Rules For Universal Quantifiers
Pascal Bercher and Yoshihiro Maruyama 24.36
T: ∀x Fx
T: Fa, T: Fb, . . .
for all a, b, . . .
in the branch –
present and future!
X , T: ∀x A
X , T: ∀x A, T: Aax
for a in X or A
≡
F: ∀x Fx
F: Fa
if a is new to
the branch
X , F: ∀x A
X , F: Aax
for a not in X or A
≡
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Rule for Invalid Sequents
Pascal Bercher and Yoshihiro Maruyama 25.36
Introduction Introduction to Semantic Tableaux Rules Examples Rules Rule for Invalid Sequents Properties Summary
Motivating Example
Assume we are deep within some branch:
(n) T: ∀x ∃y Rxy Xa,b,c from (k