Logic (PHIL 2080, COMP 2620, COMP 6262) Chapter: First-Order Logic — Introduction and Natural Deduction
Logic (PHIL 2080, COMP 2620, COMP 6262)
Chapter: First-Order Logic
— Introduction and Natural Deduction
Pascal Bercher
Planning & Optimization
Yoshihiro Maruyama
Logic
Intelligent Agents
College of Engineering and Computer Science
the Australian National University (ANU)
23 & 25 March 2021
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Introduction
Pascal Bercher and Yoshihiro Maruyama 1.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Motivation
How to model that in propositional logic?
All logicians are rational aLr
Some philosophers are not rational ¬ sPr
premises
Thus, not all philosophers are logicians ¬aPL
}
conclusion
So, can we prove aLr ,¬sPr ` ¬aPL?
No! It’s even three completely different propositions!
We need a more expressive logic!
(We could have also used p, q, and r above, the names above were
chosen to have more “speaking” names.)
Pascal Bercher and Yoshihiro Maruyama 2.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
How to extend Propositional Logic?
Logic is about making statements:
(natural language) sentence︷ ︸︸ ︷
Socrates︸ ︷︷ ︸
constant
is a goat︸ ︷︷ ︸
predicate
In first-order logic, we:
can represent individual objects (people, goats, footballs, etc.)
and express properties and relationship between objects.
In our example,
the “object” Socrates can be represented by a constant,
the “property” is a Goat can be represented by a predicate.
⇒ For example, isGoat(Socrates)
⇒ In propositional logic, we had to use SocratesIsGoat , which is
missing some information, since it does not “relate” to another
proposition involving Socrates, like SocratesKicksGoat . (Also cf.
previous example with philosophers and logicians! Same issue!)
Pascal Bercher and Yoshihiro Maruyama 3.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Predicate Logic
Pascal Bercher and Yoshihiro Maruyama 4.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Terminology And Conventions: Terminology
Term: Anything that represents an object, i.e.,
a constant (representing a fixed object, like the person Socrates)
a variable (representing a non-specified object)
a function (representing a fixed object given a sequence of terms)
Intuition:
Constants are meant to represent concrete objects, as in
“isGoat(Socrates)”.
Variables are used for “more general” relationships as in:
“All logicians are rational”. If we had a statement like
“isRational(Logician)” (when talking about all logicians),
then Logician is not a concrete individual, but a variable!
How to know that “Socrates” refers to a concrete object, but
“Logician” does not? (⇒ see next notes!)
Predicates: Express properties or relations of/between terms:
Takes as input (or “argument”) a sequence of terms.
• The sequence length depends on the predicate, e.g., isGoat is
unary, kicks is binary, etc. (some might even be nullary!)
• This length is called arity and can be given as a subscript, e.g.,
isGoat1, kicks2, but we don’t since it’s clear from context.
Maps to a truth value, e.g., isGoat(Socrates) might be false, but
isGoat(aGoat) true.
⇒ The “formal semantics” (e.g., for which terms is a predicate true?)
will be given later.
Pascal Bercher and Yoshihiro Maruyama 5.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Terminology And Conventions: Terminology
Term: Anything that represents an object, i.e.,
a constant (representing a fixed object, like the person Socrates)
a variable (representing a non-specified object)
a function (representing a fixed object given a sequence of terms)
Note:
Constants and variables cannot be distinguished “syntactically”,
they look the same! This had to be specified additionally.
E.g., in isGoat(Socrates), we cannot “know” whether Socrates is
a constant referring to a “concrete” object (namely Socrates!) or a
variable (representing just some “arbitrary” object of which we did
not yet specify to which concrete object it refers to).
Predicates: Express properties or relations of/between terms:
Takes as input (or “argument”) a sequence of terms.
• The sequence length depends on the predicate, e.g., isGoat is
unary, kicks is binary, etc. (some might even be nullary!)
• This length is called arity and can be given as a subscript, e.g.,
isGoat1, kicks2, but we don’t since it’s clear from context.
Maps to a truth value, e.g., isGoat(Socrates) might be false, but
isGoat(aGoat) true.
⇒ The “formal semantics” (e.g., for which terms is a predicate true?)
will be given later.
Pascal Bercher and Yoshihiro Maruyama 5.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Terminology And Conventions: Terminology
Term: Anything that represents an object, i.e.,
a constant (representing a fixed object, like the person Socrates)
a variable (representing a non-specified object)
a function (representing a fixed object given a sequence of terms)
Predicates: Express properties or relations of/between terms:
Takes as input (or “argument”) a sequence of terms.
• The sequence length depends on the predicate, e.g., isGoat is
unary, kicks is binary, etc. (some might even be nullary!)
• This length is called arity and can be given as a subscript, e.g.,
isGoat1, kicks2, but we don’t since it’s clear from context.
Maps to a truth value, e.g., isGoat(Socrates) might be false, but
isGoat(aGoat) true.
⇒ The “formal semantics” (e.g., for which terms is a predicate true?)
will be given later.
Pascal Bercher and Yoshihiro Maruyama 5.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Terminology And Conventions: Conventions
We continue to use our sequent notation!
• X ` A
• X ,Y ` A
• X ,A ` B
• etc. Only now they represent first-order predicate logic formulae.
As before we write only single letters!
• X, Y, Z for sets of formulae, and
• A, B, C for single formulae.
Pascal Bercher and Yoshihiro Maruyama 6.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Terminology And Conventions: Conventions (cont’d)
Capital letters are predicate symbols:
F ,G,H, . . . ,P,Q,R, L, . . .
Lower-case letters represent terms:
• a, b, c are (usually) used for constants.
• f , g, h are used for functions.
• v and x , y are used for variables.
• t is used for terms (i.e., any of the above).
For the sake of simplicity, we do not use parentheses, e.g.,
F(a), G(b), and R(a, b) become Fa, Gb, and Rab, respectively.
Now it’s clear that the arity is clear from the context! E.g.,
• Fa represents a predicate F with arity 1 (with term a), and
• Rab represents a predicate R with arity 2 (with terms a and b).
Pascal Bercher and Yoshihiro Maruyama 7.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
First-Order Formulae: Introduction
How do formulae work?
¬(Fa→ Rab)
But a and b are constants, like the one representing Socrates! So
this is not “as general” as we want it to be!
An introductory example:
All vulcans are logicians.
Let’s reformulate that step by step:
• Take any vulcan, call it x , then x is a logician. (x is a variable!)
• Take any vulcan, call it x , then Lx .
• For every object x , such that x is a Vulcan, Lx holds.
• For every object x , such that Vx holds, Lx holds.
Now we need special syntax for that “every object”!
Pascal Bercher and Yoshihiro Maruyama 8.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
First-Order Formulae: Possible Quantifiers
We want to “quantify” the objects we talk about.
For every object x , such that Vx holds, Lx holds.
More formally: ALL(x : Vx)︸ ︷︷ ︸
quantifier!
Lx
Even more formally: ∀︸︷︷︸
quantity indicator
( x︸︷︷︸
variable
: Vx︸︷︷︸
sort indicator
)Lx
What other quantifiers could possibly exist?
SOME(x : Vx)Ex (“some vulcans are emotional”)
FEW (x : Vx)Ex (“a few vulcans are emotional”)
MOST (x : Lx)¬Vx (“most logicians are not vulcans”)
ONE(x : Lx)(Ex ∧ Vx) (“One logician is an emotional vulcan”)
Pascal Bercher and Yoshihiro Maruyama 9.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
First-Order Formulae: Possible Quantifiers
We want to “quantify” the objects we talk about.
For every object x , such that Vx holds, Lx holds.
More formally: ALL(x : Vx)︸ ︷︷ ︸
quantifier!
Lx
Even more formally: ∀︸︷︷︸
quantity indicator
( x︸︷︷︸
variable
: Vx︸︷︷︸
sort indicator
)Lx
What quantifiers do exist? (In our predicate logic!)
Just two!
ALL(x : A)B, i.e., ∀(x : A)B
SOME(x : A)B, i.e., ∃(x : A)B
“SOME” means “at least one”, so “∃” is also called “exists”
“ALL”, i.e., ∀, is called the “universal” quantifier
Pascal Bercher and Yoshihiro Maruyama 9.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
First-Order Formulae: Example (from before)
Propositional logic (not working):
All logicians are rational aLr
Some philosophers are not rational ¬sPr
Thus, not all philosophers are logicians ¬aPL
Predicate logic (works!):
All logicians are rational ∀(x : Lx)Rx
Some philosophers are not rational ∃(x : Px)¬Rx
Thus, not all philosophers are logicians ¬∀(x : Px)Lx
But how to prove “∀(x : Lx)Rx ,∃(x : Px)¬Rx ` ¬∀(x : Px)Lx”?
Natural Deduction Semantic Tableaux
Pascal Bercher and Yoshihiro Maruyama 10.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Some Small Examples
All goats are hairy. ∀(x : Gx)Hx
Some footballers are hairy. ∃(x : Fx)Hx
No goats are footballers. ¬∃(x : Gx)Fx ≡ ∀(x : Gx)¬Fx
(You can see here that negations before formulae invert the
outer-most quantifier an get moved before the inner formula
(which might again be a quantified formula). You can prove this
“rule”, but you can’t use it!)
Pascal Bercher and Yoshihiro Maruyama 11.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: More Complicated Examples
Every hairy footballer kicks a goat.
• ∀(x : Hx ∧ Fx)∃(y : Gy)Kxy
• ∃(x : Gx)∀(y : Hy ∧ Fy)Kyx
• In the first model, each footballer can kick his/her own goat!
In the second, all footballers kick the same goat!∗
∗ I argue that this model is wrong! This is not what the sentence is
saying; the model is “more specific”.
Only hairy footballers kick goats.
• ∀(x : Fx ∧ ∃(y : Gy)Kxy)Hx
• ∀(x : ∃(y : Gy)Kxy)(Hx ∧ Fx)
• The first model means: “All footballers that kick a goat are hairy.”
The second: “Anything that kicks a goat is a hairy footballer.”
But which one is right? (Hard to tell, language is vague!)
Pascal Bercher and Yoshihiro Maruyama 12.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Note on Interpreting Natural Language
Modeling a proposition with logic often reveals how vague
language is!
“Only hairy footballers kick goats.” What is meant here?
• Among all footballers, only the hairy ones kick goats.
• Among all human beings, only hairy footballers kick goats.
“Only lazy students don’t study.” What is meant here?
• Among all students, only the lazy ones don’t study.
• Among all human beings (aliens, spirits, . . . ), only lazy students
don’t study.
We normally rely on context to figure that out. In an exam, we
(examiners) have to make sure to provide all the information
necessary!
Pascal Bercher and Yoshihiro Maruyama 13.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Translating a Natural Language Text into Predicate Logics
Anyone who sees a hairy footballer sees someone who kicks a
non-footballer.
Sounds horribly complicated, but let’s do it step by step!
1 ∀(x : x sees a hairy footballer)
(x sees someone who kicks a non-footballer)
2 ∀(x : ∃(y : Hy ∧ Fy)Sxy)
( ∃(y : y kicks a non-footballer)Sxy )
3 ∀(x : ∃(y : Hy ∧ Fy)Sxy)
( ∃(y : ∃z(z : ¬Fz)Kyz )Sxy )
Pascal Bercher and Yoshihiro Maruyama 14.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
From Restricted Quantifiers to Unrestricted Quantifiers: Main Idea
So far, we were only considering restricted quantifiers:
∃(x : Px)¬Rx (Some philosophers are not rational)
∀(x : Lx)Rx (All logicians are rational)
But now – to make life easier! – we don’t make restrictions anymore!
We cheat to get around having a sort restriction:
∃(x : x is a thing)Gx is the same as ∃(x : Fx → Fx)Gx
Example:
Something is hairy:
• ∃(x : Fx → Fx)Hx
• So we could also just
write ∃x Hx
Some goats are hairy:
• ∃(x : Gx)Hx
• So we can just write
∃x Gx ∧ Hx
Pascal Bercher and Yoshihiro Maruyama 15.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
From Restricted Quantifiers to Unrestricted Quantifiers: Eliminating Sort Indicator
Did we lose something when switching to unrestricted quantifiers?
No! (So, we can just use unrestricted logic instead!)
Existential quantified formulae become conjunctions:
E.g., ∃(x : Gx)Hx (some goats are hairy) becomes ∃x Gx ∧ Hx
Universally quantified formulae become implications:
E.g., ∀(x : Gx)Hx (all goats are hairy) becomes ∀x Gx → Hx
Thus, from now on, we will use non-restricted formulae instead.
(But Yoshi will re-visit restricted quantifiers again.)
Pascal Bercher and Yoshihiro Maruyama 16.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Natural Deduction
Pascal Bercher and Yoshihiro Maruyama 17.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Introduction
Instead of re-doing all our previous rules, we will just provide
additional ones!
I.e., we will still “somehow” perform natural deduction for
propositional logic, but extend these formulas to first-order
predicate formulae using the adequate rules.
We only need rules for introducing and eliminating ∀ and ∃.
Pascal Bercher and Yoshihiro Maruyama 18.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Substitutions
Let A be a formula, x a variable, and t a term.
Axt stands for the result of substituting each t in A by x .
So the term t in A gets substituted by the variable.
E.g., if A is Fa→ Ga, then Axa is Fx → Gx .
(Might look odd, since a constant gets replaced by a variable!
But we’ll only use this “strange” rule in a meaningful way!)
Let A, B be formulae, x a variable not occurring in A or B, and t a
term. Then, the following substitutions are (again/also) formulae:
∀(x : Axt )Bxt (“all As are Bs”), and
∃(x : Axt )Bxt (“At least one A is a B”).
Why the side condition? To avoid non-intended “name collisions”! E.g,
Is A = ∀(y : Py)(Qyx) the same as Axy = ∀(x : Px)(Qxx)?
No, but Azy = ∀(z : Pz)(Qzx) is!
Pascal Bercher and Yoshihiro Maruyama 19.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Universal Quantifiers
Pascal Bercher and Yoshihiro Maruyama 20.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Universal Elimination: The 1-step Rule
Let’s assume we want to say that the age of all human people is
smaller than 130: ∀x age(x) < 130
If we had one constant for each individual (person), we could
conclude: age(a) < 130 ∧ age(b) < 130 ∧ age(c) < 130 ∧ . . .
(Though that’s clearly not practical! And maybe not even possible
if we reason about infinitely many objects like numbers.)
So we could also conclude age(x) < 130 for any x !
So, how will the All-Elimination rule look like?
∀x Fx
Fa
∀E more general:
∀x A
Atx
∀E
Universal Elimination: (in sequent notation)
X ` ∀x A
X ` Atx
∀E
Pascal Bercher and Yoshihiro Maruyama 21.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Universal Introduction: Introduction
For the introduction of the universal quantifier, we would like to
have, conceptually, a rule like the following:
Fa Fb Fc . . .
∀x Fx
∀I
But that’s again infeasible, and potentially even impossible!
How about: Fa
∀x Fx
∀I ?
That rule is wrong! Just because Aristotle is (was) a footballer,
doesn’t mean that everybody is!
But it might work for “typical objects”... (a variable)
Pascal Bercher and Yoshihiro Maruyama 22.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Universal Introduction: Typical Objects
What’s a typical object?
Remember the “undergraduate school” when you have to proof
some property of all triangles.
• Step 1: Let ABC=
B
A
C
a
b
c
α
α
β
β
be a triangle.
• Step 2: “some fancy proof”
• Step 3: Thus, ABC has property P. Thus P holds for all triangles!
Why is that correct? Since we did not make any assumptions for
ABC other than it being a triangle! E.g., we did not demand that it
has a 90-degree angle or any other special case! We gave it a
name (ABC), but that was also arbitrary!
Pascal Bercher and Yoshihiro Maruyama 23.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Universal Introduction: The 1-step Rule
So, we need an “object without any assumption” to generalize its
property (formula) to the general case.
But how to express this “no assumptions”?
Fv
∀x Fx
∀I more general:
A
∀x Axv
∀I with side condition:
provided the variable v does not occur in any assumption that A
depends upon.
Universal Introduction: (in sequent notation)
X ` A
X ` ∀x Axv
∀I only if v does not occur in X !
Pascal Bercher and Yoshihiro Maruyama 24.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Universal Introduction: More on our Assumption and Side-Conditions
So we have: X ` A
X ` ∀x Axv
∀I only if v does not occur in X !
So, can we use Fa
∀x Fx
∀I to prove Fa ` ∀x Fx?
Let’s try! Does not work: Rule fails for two reasons!
Faristotle ` ∀x Fx
α1 (1) Faristotle A
α1 (n) ∀x Fx
Pascal Bercher and Yoshihiro Maruyama 25.40
X ` A
X ` ∀x Axv
∀I
Only if v does
not occur in X!
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Universal Introduction: More on our Assumption and Side-Conditions
So we have: X ` A
X ` ∀x Axv
∀I only if v does not occur in X !
So, can we use Fa
∀x Fx
∀I to prove Fa ` ∀x Fx?
Thus, no!
• The side condition states that a (which is “the thing” being
substituted) does not occur in X , but X is Fa here, so the side
condition is violated.
• Also, in our rule above a represents a constant (like aristotle in the
failed proof attempt), but the rule only works for variables! So it’s
not applicable here anyway. Recall: Just because Aristotle plays
football, not everybody does!
Pascal Bercher and Yoshihiro Maruyama 25.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
More on Syntax: Meaning of a, b, c, . . . in Proofs
Important:
Note that the Logic Notes (and sometimes Yoshi as well!) refer to
constants as “names”.
More importantly, note that we only use a, b, c, etc. as constants
in the explanations for rules here in the lecture. For convenience,
in all exercises, including those given in the lecture, these letters
do not represent constants!
Instead, in formal proofs, these letters (again: a, b, c, . . . ) will
represent our “typical objects” – like the triangle ABC from before!
These “typical objects” are (free, i.e., unbound) variables.
In fact, you will never deal with constants in proofs!
Pascal Bercher and Yoshihiro Maruyama 26.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Example Proofs: Example 1
∀x Fx ,∀x Gx ` ∀x (Fx ∧ Gx)
α1 (1) ∀x Fx A
α2 (2) ∀x Gx A
α1 (3) Fa 1 ∀E
α2 (4) Ga 2 ∀E
α1, α2 (5) Fa ∧ Ga 3,4 ∧I
α1, α2 (6) ∀x (Fx ∧ Gx) 5 ∀I
α1, α2 (n-1) Fa ∧ Ga
α1, α2 (n) ∀x (Fx ∧ Gx) (n-1) ∀I
Pascal Bercher and Yoshihiro Maruyama 27.40
X ` A
X ` ∀x Axv
∀I
Only if v does
not occur in X!
X ` ∀x A
X ` Atx
∀E
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Example Proofs: Example 1
∀x Fx ,∀x Gx ` ∀x (Fx ∧ Gx)
α1 (1) ∀x Fx A
α2 (2) ∀x Gx A
α1 (3) Fa 1 ∀E
α2 (4) Ga 2 ∀E
α1, α2 (5) Fa ∧ Ga 3,4 ∧I
α1, α2 (6) ∀x (Fx ∧ Gx) 5 ∀I
Did we adhere all side conditions?
Yes!
• X ` A corresponds to line 5, which is α1, α2 ` Fa ∧ Ga,
• variable v corresponds to a, and
• although a (of course!) occurs in Fa ∧ Ga, it is not in
X = {α1, α2} = {∀x Fx ,∀x Gx}, so all good!
Pascal Bercher and Yoshihiro Maruyama 27.40
X ` A
X ` ∀x Axv
∀I
Only if v does
not occur in X!
X ` ∀x A
X ` Atx
∀E
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Example Proofs: Example 2
∀x (Fx → ∀y Fy) ` ∀x (¬Fx → ∀y ¬Fy)
α1 (1) ∀x (Fx → ∀y Fy) A
α2 (2) ¬Fa A
α3 (3) Fb A
α1 (4) Fb → ∀y Fy 1 ∀E
α1, α3 (5) ∀y Fy 3,4→E
α1, α3 (6) Fa 5 ∀E
α1, α2 (7) ¬Fb 2,6[α3] RAA
α1, α2 (8) ∀y ¬Fy 7 ∀I
α1 (9) ¬Fa→ ∀y ¬Fy 8[α2]→I
α1 (10) ∀x (¬Fx → ∀y ¬Fy) 9 ∀I
α1, α2 (n-3) ¬Fb
α1, α2 (n-2) ∀y ¬Fy (n-3) ∀I
α1 (n-1) ¬Fa→ ∀y ¬Fy (n-2)[α2]→I
α1 (n) ∀x (¬Fx → ∀y ¬Fy) (n-1) ∀I
Pascal Bercher and Yoshihiro Maruyama 28.40
Why did we substitute y by b rather than by a?
X ` A corresponds to ¬Fb,
The variable v in the rule (which is b in our case!)
may not occur in X , which works for us since
X = {α1, α2} = {∀x (Fx → ∀y Fy),¬Fa}
So choosing v = a would not have been possible,
since a occurs in α2 = ¬Fa!
X ` A
X ` ∀x Axv
∀I
Only if v does
not occur in X!
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Example Proofs: Example 2
∀x (Fx → ∀y Fy) ` ∀x (¬Fx → ∀y ¬Fy)
α1 (1) ∀x (Fx → ∀y Fy) A
α2 (2) ¬Fa A
α3 (3) Fb A
α1 (4) Fb → ∀y Fy 1 ∀E
α1, α3 (5) ∀y Fy 3,4→E
α1, α3 (6) Fa 5 ∀E
α1, α2 (7) ¬Fb 2,6[α3] RAA
α1, α2 (8) ∀y ¬Fy 7 ∀I
α1 (9) ¬Fa→ ∀y ¬Fy 8[α2]→I
α1 (10) ∀x (¬Fx → ∀y ¬Fy) 9 ∀I
α1, α2 (n-3) ¬Fb ?,?[α3] RAA
α1, α2 (n-2) ∀y ¬Fy (n-3) ∀I
α1 (n-1) ¬Fa→ ∀y ¬Fy (n-2)[α2]→I
α1 (n) ∀x (¬Fx → ∀y ¬Fy) (n-1) ∀I
Pascal Bercher and Yoshihiro Maruyama 28.40
X ` A
X ` ∀x Axv
∀I
Only if v does
not occur in X!
X ,B ` A Y ,B ` ¬A
X ,Y ` ¬B
RAA
X ` ∀x A
X ` Atx
∀E
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Existential Quantifiers
Pascal Bercher and Yoshihiro Maruyama 29.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Existential Introduction: Introduction
Recall that you can “imagine” the universal quantifier ∀ like:
age(a) < 120 ∧ age(b) < 120 ∧ age(c) < 120 ∧ . . .
The existential quantifier ∃ can similarly interpreted as:
age(a) > 100 ∨ age(b) > 100 ∨ age(c) > 100 ∨ . . .
Thus, conceptually, we would expect something like the following
rule:
Fa ∨ Fb ∨ Fc ∨ . . .
∃x Fx
∃I
Pascal Bercher and Yoshihiro Maruyama 30.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Existential Introduction: The 1-step Rule
Existential Introduction Rule:
Fa
∃x Fx
∃I more general:
Atx
∃x A
∃I
in sequent
notation:
X ` Atx
X ` ∃x A
∃I
What’s written there?
• The formula above is Atx , so we know that it does not have an x in
it! (Because if A does have some x , it got replaced by t !)
• The formula below is just A, so that might still have an x inside –
an x for which we know that some term t exists for which Atx can
be derived.
Note that this rule assumes a non-empty “universe” (the objects
that we reason about, more later when we formally deal with the
semantics), i.e., that there exists at least one “object” that the
terms represent. (Not relevant for the exam.)
Pascal Bercher and Yoshihiro Maruyama 31.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Existential Elimination: Introduction
We want to eliminate the existential quantifier. So can we just use
the following rule?
∃x Fx
Fa
∃E ? Recall:
∀x Fx
Fa
∀E !
So, no! Because we don’t know which object has that property!
(You can try to “prove” some invalid sequent when having this
(wrong) rule available!)
Pascal Bercher and Yoshihiro Maruyama 32.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Existential Elimination: Introduction, cont’d
The idea behind the rule is the following:
∃x Fx
[Fy ]
…
B
B
∃E for a “typical” y .
The idea is similar to disjunction elimination: In A ∨ B, we don’t
know whether A or B is true, so we assume both and show that
either way the derivation can be done.
Here, we show it for “some instance” that does not pose further
restrictions (and then discharge it since we know that such an
“instance” exists due to the assumption ∃x Fx).
Pascal Bercher and Yoshihiro Maruyama 33.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Existential Elimination: The 1-step Rule
Existential Elimination Rule:
X ` ∃x Axt Y ,A ` B
X ,Y ` B
∃E Provided t does not occur
in B or any formula in Y .
Note what’s written here: The assumption formula A in sequent 2
can be regarded an “instantiation” of the derivation in sequent 1
by substituting x by a term.
We need the side condition so that our choice of the “instance” of
x is still “general”.
Otherwise we might be able to derive simply because we chose a
specific special case!
Again, you can try to prove an invalid sequent, which you might
be able to if you violate that side condition!
Pascal Bercher and Yoshihiro Maruyama 34.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Example 1
` ∀x ∃y (Fx → Fy)
α1 (1) Fa A
(2) Fa→ Fa 1[α1]→I
(3) ∃y (Fa→ Fy) 2 ∃I
(4) ∀x ∃y (Fx → Fy) 3 ∀I
(n-1) ∃y (Fa→ Fy)
(n) ∀x ∃y (Fx → Fy) (n-1) ∀I
Pascal Bercher and Yoshihiro Maruyama 35.40
X ` A
X ` ∀x Axv
∀I
Only if v does
not occur in X!
X ` Atx
X ` ∃x A
∃I
Wait a minute! Didn’t we say that Atx replaces all occurrences of x
in A by t? So going from line (2) Fa→ Fa to line (3) ∃y (Fa→ Fy)
is wrong, right?
No! A is defined in line (3), so A is Fa→ Fy . So we did substitute all
ts (here: y ) by x (here: a)!
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Example 1
` ∀x ∃y (Fx → Fy)
α1 (1) Fa A
(2) Fa→ Fa 1[α1]→I
(3) ∃y (Fa→ Fy) 2 ∃I
(4) ∀x ∃y (Fx → Fy) 3 ∀I
(n-1) ∃y (Fa→ Fy)
(n) ∀x ∃y (Fx → Fy) (n-1) ∀I
Pascal Bercher and Yoshihiro Maruyama 35.40
X ` A
X ` ∀x Axv
∀I
Only if v does
not occur in X!
X ` Atx
X ` ∃x A
∃I
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Example 2
∃x (Fx ∧ Gx) ` ∃x Fx ∧ ∃x Gx
α1 (1) ∃x (Fx ∧ Gx) A
α2 (2) Fa ∧ Ga A
α2 (3) Fa 2 ∧E
α2 (4) ∃x Fx 3 ∃I
α2 (5) Ga 2 ∧E
α2 (6) ∃x Gx 5 ∃I
α2 (7) ∃x Fx ∧ ∃x Gx 4,6 ∧I
α1 (8) ∃x Fx ∧ ∃x Gx 1,7[α2] ∃E
α2 (n-1) ∃x Fx ∧ ∃x Gx
α1 (n) ∃x Fx ∧ ∃x Gx 1,(n-1)[α2] ∃E
Pascal Bercher and Yoshihiro Maruyama 36.40
X ` ∃x Axt Y ,A ` B
X ,Y ` B
∃E
Provided t does not occur in
B or any formula in Y .
X ` Atx
X ` ∃x A
∃I
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Example 3: On Logicians and Philosophers
Remember from the beginning:
All logicians are rational ∀(x : Lx)Rx
Some philosophers are not rational ∃(x : Px)¬Rx
Thus, not all philosophers are logicians ¬∀(x : Px)Lx
Now, in our unsorted predicate logic, this is:
All logicians are rational ∀x Lx → Rx
Some philosophers are not rational ∃x Px ∧ ¬Rx
Thus, not all philosophers are logicians ¬∀x Px → Lx
Pascal Bercher and Yoshihiro Maruyama 37.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Examples: Example 3: On Logicians and Philosophers (cont’d)
∀x Lx → Rx ,∃x Px ∧ ¬Rx ` ¬∀x Px → Lx
α1 (1) ∀x Lx → Rx A
α2 (2) ∃x Px ∧ ¬Rx A
α3 (3) Pa ∧ ¬Ra A
α4 (4) ∀x Px → Lx A
α4 (5) Pa→ La 4 ∀E
α3 (6) Pa 3 ∧E
α3, α4 (7) La 5,6→E
α1 (8) La→ Ra 1 ∀E
α1, α3, α4 (9) Ra 7,8→E
α3 (10) ¬Ra 3 ∧E
α1, α3 (11) ∀x Px → Lx 9,10[α4] RAA
α1, α2 (12) ∀x Px → Lx 2,11[α3] ∃E
α1, α3 (n-1) ¬∀x(Px → Lx) ?,?[α4] RAA
α1, α2 (n) ¬∀x(Px → Lx) 2,(n-1)[α3] ∃E
Pascal Bercher and Yoshihiro Maruyama 38.40
X ` ∃x Axt Y ,A ` B
X ,Y ` B
∃E
Provided t does not occur in
B or any formula in Y .
X ,B ` A Y ,B ` ¬A
X ,Y ` ¬B
RAA
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Summary
Pascal Bercher and Yoshihiro Maruyama 39.40
Introduction Predicate Logic Natural Deduction Universal Quantifiers Existential Quantifiers Summary
Content of this Lecture
We introduced predicate logic:
• with restricted quantifiers (we re-visit that later)
• and with unrestricted quantifiers
Predicate logic extends propositional logic in the sense that it’s
able to reason about objects, properties, and their relation to
each other.
Natural deduction for predicate logics, with additional rules for:
• Existential introduction and elimination
• Universal introduction and elimination
• For the rest we keep using the rules from propositional logics!
→ The entire Logic Notes sections:
• 4: Expressing Generality
I except “Properties of relations”
I and except “Functions”
I (You should read them anyway, in particular “Functions”!)
Pascal Bercher and Yoshihiro Maruyama 40.40
Introduction
Predicate Logic
Terminology And Conventions
First-Order Formulae
Examples
From Restricted Quantifiers to Unrestricted Quantifiers
Natural Deduction
Universal Quantifiers
Universal Elimination
Universal Introduction
More on Syntax
Example Proofs
Existential Quantifiers
Existential Introduction
Existential Elimination
Examples
Summary