Natural Deduction
COMP1600 / COMP6260
Australian National University
Semester 2, 2021
Criticism of Equational Proofs
The good.
Completeness tells us that if an equation is true, we can prove it.
The bad.
Sometimes need lots of ingenuity to find a proof! E.g.
x ∨ x = (x ∨ x) ∧ T = (x ∨ x) ∧ (x ∨ ¬x) = x ∨ (x ∧ ¬x) = x ∨ F = x
The ugly.
Equational reasoning is not natural, i.e. it doesn’t mirror the meaning of ∧,∨ and ¬.
1/52
Towards Propositional Formulae and Natural Deduction
. Implication, written →
In English. x → y means “if x is true, then so is y”.
Truth Table. Informally, think of x → y as a promise. the promise is that y is true if x is true
x → y evaluates to F if the promise is broken
xyx→y FT FT TF TTT
F
T
F
2/52
Interlude: Logic to English
Exercise. Use the predicates I – I’m going surfing, Y – you’re going surfing, and W – there’ll be a big wave that kills us all, to translate the following statements to English:
1. I ∧ Y → W
2. (I → W ) ∨ (Y → W )
Possible Answer.
3/52
Interlude: Logic to English
Exercise. Use the predicates I – I’m going surfing, Y – you’re going surfing, and W – there’ll be a big wave that kills us all, to translate the following statements to English:
1. I ∧ Y → W
2. (I → W ) ∨ (Y → W )
Possible Answer.
1. If both of us are going surfing, then there’ll be a big wave that kills us all.
3/52
Interlude: Logic to English
Exercise. Use the predicates I – I’m going surfing, Y – you’re going surfing, and W – there’ll be a big wave that kills us all, to translate the following statements to English:
1. I ∧ Y → W
2. (I → W ) ∨ (Y → W )
Possible Answer.
1. If both of us are going surfing, then there’ll be a big wave that kills us all.
2. If both of us are going surfing, then there’ll be a big wave that kills us all.
(Both formulae have the same truth table!)
3/52
Propositional Formulae
Definition. Given a set V of variables, propositional formulae are constructed as follows:
T (true) and F (false) and all variables x ∈ V are boolean formulae if φ and ψ are boolean formulae, then so are φ∧ψ and φ∨ψ and φ→ψ
if φ is a boolean formula, then so is ¬φ.
Precedence. ¬ binds more strongly than ∧ binds more strongly than ∨ binds more strongly than →:
¬x → y ∨ z reads as (¬x) → (y ∨ z)
Boolean Formulae vs Propositional Formulae
propositional formulae are boolean formulae with addition of → → is expressible using boolean formulae: x → y = ¬x ∨ y
but included as implication is used very frequently
4/52
Contradictions and Contingencies
Types of Propositional Formulae. A propositional formula is
valid, if it evaluates to T in all situations / under all truth value
assignments.
a contradiction if it evaluates to F in all situations, and
a contingency if there are (necessarily different) situations for which it evaluates to T and to F.
Example.
’John had toast for breakfast’ is a contingency.
’John had toast for breakfast’ ∧¬ ’John had toast for breakfast’ is a contradiction.
p→(¬q∨p)→(p∧q)∨r –canbecomplicated
5/52
Example proof using truth tables
Statement to be proved:
φ ≡ (p ∧ (q ∨ r)) → ((p ∧ q) ∨ r))
For all 8 (= 23) possibilities of p,q,r, calculate truth value of the statement
p q r q∨r p∧(q∨r) p∧q (p∧q)∨r φ TTTTTTTT TTFTTTTT TFTTTFTT TFFFFFFT FTTTFFTT FTFTFFFT FFTTFFTT FFFFFFFT
Always exponential in size!
6/52
Natural Deduction
Truth Tables. Can be exponential
Equational Proofs. Can be very unintuitive
Natural Deduction
formal system that imitates human reasoning
explains one connective at a time: intro and elim rules used to prove validity of formulae.
also used in all formal theorem provers
7/52
Informal Proof
Goal. Show that φ ≡ (p ∧ (q ∨ r)) → (q → s) ∨ p is valid.
Informal Proof.
1. First,assume that p ∧ (q ∨ r) (is true) and show that (q → s) ∨ p. 2. under this assumption, we have that p (is true).
3. still under this assumption, (q → s) ∨ p (is true).
4. Thatis,p∧(q∨r)→(q→s)∨pwithoutassumptions.
Formal Natural Deduction Proof.
1 2 3 4
p ∧ (q ∨ r) p
(q → s) ∨ p
(p ∧ (q ∨ r)) → ((q → s) ∨ p)
Assumption ∧-E, 1
∨-I, 2
→-I, 1–3
8/52
Conjunction rules
And Introduction (∧-I)
as p is true, and q is true, we have that p∧q is true. And Elimination (∧-E)
p∧q p∧q pq
as p∧q is true, we have that p is true. as p∧q is true, we have that q is true.
pq p∧q
9/52
Example
Example. Commutativity of conjunction (derived rule) p∧q
q∧p
assuming that p ∧ q (is true), we (also) have that q ∧ p (is true).
Informal Proof.
1. Assume that p ∧ q.
2. because of p∧q, we have p. 3. because of p∧q, we have q. 4. therefore, we also have q∧p.
Natural Deduction Proof.
1 p∧q 2 p
3 q
4 q∧p
∧-E, 1 ∧-E, 1 ∧-I, 2, 3
10/52
Implication rules
Implication Introduction (→-I)
[p]
.
q p→q
if q is true under the assumption p, then p → q is true without the assumption p.
[. . . ] means that the assumption p is discarded (no longer made). Implication Elimination (→-E)
p p→q q
if both p and p → q hold (are true), then so does q.
11/52
Example – transitivity of implication (derived rule)
We prove
p→q q→r p→r
Informal Proof.
1. fix the assumption p → q.
2. fix the assumption q → r.
3. additionally assume p (and show r)
4. becausepandp→q,wehaveq.
5. becauseqandq→r,wehaver.
6. hencep→r holdswithoutassumingp
Natural Deduction Proof.
1 p→q 2 q→r 3p 4 q 5 r 6 p→r
→-E, 1, 3 →-E,2,4 →-I,3–5
lines 1 and 2 are assumptions, can be used anywhere
line 3 is an assumption we make, can be used only in scope (l 3–5).
12/52
Aside: Justification of Proof Steps
Silly Proof. (we prove what we already know!)
1 p→q
2p
3 q →-E, 1, 2 4 p → q →-I, 2–3
Line Number Notation.
→-E,1,2 means that rule →-E proves line 3 from lines 1 and 2 →-I,2-3 means rule →-I proves line 4 from the fact that we could
assume line 2 and (using that assumption) prove line 3. In →-I, 2–3 is the entire scope of the assumption p.
13/52
Rules involving assumptions
1 p→q 2 q→r 3p
4 5 6
q
r q ∧ r
WRONG
→-E, 1, 3 →-E, 2, 4 ∧-I, 4, 5
statements inside the scope of an assumption depends on that assumption.
we only know that they are true if the assumption is true!
we have assumed p and “proved” q ∧ r, but q ∧ r depends on p. Indentation and vertical lines indicate scoping
Similar to programming: p is a “local variable”.
14/52
Useless assumptions
You can assume anything, but it might not be useful.
1 p∧q
2 q
3 (p ∧ q) → q
p ∧ Youareagiraffe
∧-E, 1 →-I, 1–2
1 2 3
You are a giraffe
p ∧ Youareagiraffe → Youareagiraffe
∧-E, 1 →-I,1–2
15/52
Disjunction rules
Or Introduction (∨-I)
pp p∨q q∨p
if p (holds), then so do p∨q and q∨p
Or Elimination (∨-E)
[p] [q] . .
p∨qrr r
assuming that we have a proof of p ∨ q and for the case that p holds, we have a proof of r for the case that q holds we have a proof of r then we have a proof of r just from p∨q.
16/52
∨-E template
1. know that p∨q
2. in case p is true
…
a. we know that r.
b. and in case that q is true
1 p∨q 2p
. .
ar bq
. .
cr
r ∨-E, 1, 2–a, b–c
…
c. we also know that r
d. soweknowr aslongasp∨q!
17/52
Example: commutativity of disjunction (derived rule)
Informal Proof.
1. fix the assumption p ∨ q.
p∨q q∨p
Natural Deduction Proof.
2. first assume that p is true.
3. then also have that q ∨ p.
4. now assume that q is true.
5. then also have that q ∨ p.
6. hence q ∨ p, without assuming either p or q.
1 p∨q 2p
3 q ∨ p 4q
5 q ∨ p 6 q∨p
∨-I, 2
∨-I, 4
∨-E, 1, 2–3, 4–5
18/52
Negation and Truth Rules
not introduction (¬-I) [p]
.
F ¬p
not elimination (¬-E) p ¬p
F
if assuming p gives a contradiction, p is wrong – so ¬p must hold. Proof by Contradiction (PC) Truth
[¬p] .
FT
p
to prove p, assume ¬p and derive a contradiction.
truth, i.e. T, can always be established without assumptions.
19/52
Example: double negation introduction (derived rule)
p ¬¬p
Informal Proof.
1. Fix the assumption p.
2. additionally assume that ¬p.
3. then F as p and ¬p (under assn p)
4. hence ¬p is contradictory, so ¬¬p.
It is raining
It is not the case that it is not raining
Natural Deduction Proof.
1p
2 ¬p 3 F 4 ¬¬p
¬E, 1, 2 ¬I, 2–3
20/52
Example: contradiction elimination (derived rule)
“Anything follows form a contradiction”
F q
1F
2 ¬q
3 F R,1
4 q PC, 2––3
R stands for “repeat”.
F holds and continues to hold within the scope of the assumption ¬q. assuming ¬q a “technical trick”.
21/52
Example: double negation elimination (derived rule)
¬¬p p
1 ¬¬p
2 ¬p 3 F 4 p
¬E, 1, 2 PC, 2–3
22/52
Equivalence
p ↔ q means p is true if and only if q is true We can make the definition
p ↔ q ≡ (p → q) ∧ (q → p) which would naturally give us these rules
introduction rule:
elimination rules:
p→q q→p p↔q
p↔q p↔q p→q q→p
23/52
Which rule to use next?
Guided by the “form” of your goal, and what you already have proved “form” — ie, look at the connective: ∧, ∨, →, ¬
always can consider using PC (proof by contradiction)
to prove p ∨ q, ∨-I (or introduction) may not work
pq p∨q p∨q
p may not be necessarily true, q may not be necessarily true
24/52
To prove p ∨ q, sometimes you need to do this:
1. Using PC, assume ¬(p ∨ q) (hoping to prove some contradiction) 2. When is ¬(p ∨ q) true? When both p and q are false!
3. From ¬(p ∨ q) how to prove ¬p? (next slide)
4. Having proved both ¬p and ¬q, prove some further contradiction
¬p → q p∨q
Tutorial Exercise.
25/52
Not-or elimination (derived rule)
¬(p ∨ q) ¬p
1 ¬(p ∨ q) 2p
3 4 5
p ∨ q F
∨-I, 2 ¬E, 1, 3 ¬I, 2–4
¬p
26/52
Proving a contrapositive rule
In the same way, whenever you can prove any
p q
then you can prove
¬q ¬p
1 ¬q 2p
3 4 5
q F
your proof of q from p ¬E, 1, 3
¬I, 2–4
¬p
27/52
Law of the excluded middle (derived)
p ∨¬p
“Everything must either be or not be.” – Russell
1 ¬(p ∨ ¬p)
2 ¬p ¬∨-E (previous slide), 1
3 ¬¬p ¬∨-E (previous slide), 1
4 F ¬E,2,3
5 p ∨ ¬p PC, 1–4
28/52
Summary: Major Proof Techniques
Three major styles of proof in logic and mathematics
Model based computation: truth tables for propositional logic Algebraic proof: equational reasoning
Deductive reasoning: rules of inference (e.g. Natural Deduction)
Q. Why bother? Why not write a program that does truth tables? propositional logic is decidable: can write a program
other logics are not: first order logic (next)
29/52
What can we say about the following situation?
likes
Deb
30/52
Some (English) Sentences
likes
Brian likes Alice.
Eric and Deb like one another. Nobody likes Brian.
Everybody likes Charlie.
Two people like each other.
Someone is liked by everyone.
Deb
31/52
Key Ingredients
likes
Deb
Set
Relation
U = {A,B,C,D,E}
R = {(A,C),(B,A),(B,C), (D,C),(D,E),(E,C),(E,D)}
set of ordered pairs (directional)
thought of as “individuals” (can be things)
32/52
Limits of Propositional Logic
Propositional Logic.
atomic propositions, no “inner structure”
could be ‘Brian likes Alice’ and ‘someone likes someone (else)’
How about …
Alice likes someone who is liked by everyone Everybody likes someone who doesn’t like anyone …
Propositional Logic is not enough!
What is the limit of what we can say?
What are the relationships between all these propositions?
33/52
Limits of Propositional Logic
Propositional logic talks (only) about statements, or facts e.g. ’I am going surfing’
can be true or false.
Propositional Logic cannot talk about
Objects, e.g. people, houses, cars, numbers, programs, variables Relations, e.g. red, prime, larger than
First Order Logic
Predicated depending on variables (e.g. likes(x,y))
Combined using universal (∀) and existential (∃) quantifiers
In the example: everyone (∀) and someone (∃)
more complex concepts by nesting (everybody loves someone who . . . )
34/52
Quantifiers, Informally
Universal Quantification. ∀x: “All x …
(logic) ∀x.likes(x,Charlie)
(direct translation) For all x, x likes Charlie. (natural English) Charlie is liked by everyone.
Existential Quantification. ∃x: “There is an x s.t. … (logic) ∃x.likes(x,Alice)
(direct translation) There is an x s.t. x likes Alice. (natural English) Alice is liked by someone.
35/52
More Complex Sentences.
Nobody likes Brian.
∀x (¬likes(x , Brian)) Two people like each other.
∃x ∃y(likes(x, y) ∧ likes(y, x)) Someone is liked by everyone.
∃x ∀y (likes(y , x ))
Q. What does the following translate to?
∀x ∃y (likes(y , x ))
36/52
First Order Logic: Vocabulary
Vocabulary. relation symbols
have an arity: number of “things” that are related. Examples: is elephant(x) (unary), likes(x,y) (binary)
Informal Interpretation.
is elephant: the set of all elephants
likes: the set of all pairs (x,y) s.t. x likes y
Informal Interpretation: Syntax
is elephant: a proposition depending on an argument likes: a proposition depending on two arguments
37/52
First Order Logic: Official Syntax
Vocabulary. A vocabulary for first order logic is a set R (of relation symbols) where each relation symbol has an arity (number of arguments).
Syntax of First Order Logic. Let R be a vocabulary and V a set of variables. The formulae of first-order logic (over R and V ) are constructed as follows:
1. If r ∈ R is an n-ary and x1,…,xn ∈ V, then r(x1,…,xn) is a formula.
2. Ifφandψareformulae,thensoareφ∧ψ,φ∨ψ,φ→ψ,and¬φ. 3. If φ is a formula, and x ∈ V, then ∃xφ and ∀xφ are formulae.
Dot Notation saves outermost parentheses:
∀x.very complex formula ≡ ∀x(very complex formula) ∃x.very complex formula ≡ ∃x(very complex formula)
38/52
Happy and Unhappy Dragons
Vocabulary.
unary predicates
D(x)–x isadragon,H(x)–x ishappy,F(x)–x canfly binary predicate
C(x,y)–x isachildofy Logic.
English.
1. All dragons can fly unless they are unhappy.
2. At least one dragon can fly despite being unhappy.
3. A dragon is happy if all its children can fly.
1. ∀x.D(x) → F(x) ∨ ¬H(x)
2. ∃x.D(x)∧F(x)∧¬H(x)
3. ∀x.D(x) → (∀y.C(y,x) → F(y)) → H(x)
39/52
Common Patterns
Existential Quantifier. often goes with ∧ There is a dragon that . . .
There is an x that is a dragon and … ∃x.dragon(x) ∧ . . .
Universal Quantifier. often goes with → All dragons . . .
For all x, if x is a dragon, then … ∀x.dragon(x) → . . .
40/52
Situations for First Order Logic
Recall. Formulae of propositional logic depend on variables
a situation tells us whether these variables are true or false given a situation, can evaluate a formula to true or false
Q. What do we need so that we can say that a first-order formula is true or false?
Example: likes(x,y) – what are x and y, and what is “likes”? Situations θ for first-order logic are given by:
a domain of discourse U – simply a set (of things) for every r ∈ R n-ary, an n-ary relation θ(r) on U for all variables x, an element θ(x) of U.
Notation: (U,θ)
41/52
Example: The Taxonomy of “likes”
likes
Deb
Situation. S = (U,θ) where
U = {A,B,C,D,E}
θ(likes) = {(A,C),(B,A),(B,C),(D,C),(D,E),(E,C),(E,D)}
θ(x) = θ(y) = Alice, θ(x) = Deb. (not required to be injective – many variables can point to same object)
42/52
Formal Semantics
Given. Vocabulary R, situation S = (U, θ)
Truth of formula φ in situation (U,θ) Base case. Truth of r(x1, . . . , xn)
if r(x1, . . . x) is true in the situation that is, if (θ(x1), . . . , θ(xn)) are related that is, if (θ(x1),…,θ(xn)) ∈ θ(r).
Propositional Logic Cases.
φ∧ψistrue ⇐⇒ φistrueandψistrue φ∨ψistrue ⇐⇒ φistrueorψistrue φ → ψ is true if φ is not true or ψ is true ¬φ is true ⇐⇒ φ is not true
Quantifier Cases.
∀x.φ is true if φ is true for all values of θ(x) (and everything else unchanged)
∃x.φ is true if φ is true for some value of θ(x) (and everything else unchanged)
43/52
Digression on Quantifiers
Universal Quantifier. To see that ∀x.φ is true in situation (U,θ) need to take θ and vary the value of x
show that φ is true in situation (U,θ′)
behaves like an “infinite and” over all elements of the domain
Existential Quantifier. To see that ∃x.φ is true in situation (U,θ): need to take θ and vary the value of x
need to exhibit one varied θ′ such that φ is true in situation (U,θ′) behaves line an “infinite or” over all elements of the domain
44/52
Back to the Example
Variables V = {a,b,c,…} with θ(a) = Alice, θ(b) = Brian etc. likes
Deb
Q. Does everyone like Charlie, i.e. is ∀x(likes(x,c)) true in the situation above?
vary the value of x for θ, i.e. consider θ′(x) = a,b,…,e show likes(x,c) is true for all such θ′
show likes(Alice, Charlie) and likes(Brian, Charlie) and . . . but it is false that likes(Charlie, Charlie)!
so ∀x.likes(x,c) is not true in the situation above as Charlie doesn’t like her/himself!
45/52
Special Case: Quantifiers over the Empty Set
Given.
Situation S = (U, θ) for first order logic unary relation unicorn with θ(unicorn) = ∅
Existential Quantifier
“There is a tree-climbing unicorn”: ∃x.unicorn(x) ∧ climbs trees(x) always false: ∃x.unicorn(x) ∧ climbs trees(x) is false in S irrespective of value of x, unicorn(x) is always false.
Universal Quantifier.
“All unicorns climb trees”: ∀x.unicorn(x) → climbs trees(x) always true: ∀x.unicorn(x) → climbs trees(x) is true in S. irrespective of value of x, unicorn(x) is always false.
46/52
Propositional vs First Order Logic
Propositional Logic.
Given propositional logic formula φ, can decide validity by constructing all truth tables.
First Order Logic.
To show (or check) that a first-order formula is valid, would need to construct all situations
But there are infinitely many of them, and some of them infinite!
Decidability.
Propositional logic is decidable: can write program that checks for validity.
Naive checking for validity doesn’t work for first order logic – but maybe there’s a better way?
Can formally prove that there cannot be a program that checks first-order validity!
47/52
Interlude: The Drinker’s Paradox
Drinker’s Paradox (Smullyan 1978, in “What is the name of this book?”) “In every non-empty pub there is someone so that if (s)he is drink-
ing, so is everybody else.”
In Logic (with one unary predicate D(x))
φ ≡ ∃x(D(x) → ∀yD(y))
Q. Is φ valid in all situations (U,θ) where U is not empty?
48/52
Laws for Quantifiers: Negating “there exists”
Examples.
¬(∃x.P(x)) ↔ (∀x.¬P(x))
“No elephant is unhappy. ”
¬∃x.elephant(x) ∧ ¬happy(x) ∀x.¬(elephant(x) ∧ ¬happy(x)) ∀x.¬elephant(x) ∨ happy(x)
“Everything is either happy or not an elephant”
De Morgan Laws. Consider domain U = {a0, a1, . . . }.
¬∃x.P(x) intuitively equivalent to ¬(P(a0)∨P(a1)∨…) ¬(P(a0)∨P(a1)∨…) equiv to ¬P(a0)∧¬P(a1)∧… by De Morgan ¬P(a0)∧¬P(a1)∧… intuitively equivalent to ∀x.¬P(x)
49/52
Negating ∃, Formally
Theorem. Let φ be a first-order formula, S = (U, θ) a situation. Then ¬∃x.φistrueinS ifandonlyififf∀x.¬φistrueinS.
Proof (Sketch). Suppose that ¬∃x.φ is true in S. To see that ∀x.¬φ is true in S, let θ′ agree with θ except possibly on the value of x.
We need to show that ¬φ is true in S′ = (U,θ′), i.e. φ is false in S′. Suppose for a contradiction that φ is true in S′. As θ′ agrees with θ except
possibly on the value of x, this means that ∃x.φ is true in S, contradiction. The reverse direction is analogous.
50/52
Negating “for all”
Examples
¬(∀x.P(x)) ↔ (∃x.¬P(x))
“Not all elephants are happy” ¬∀x.elphant(x) → happy(x) ∃x.¬(elephant(x) → happy(x)) ∃x.elephant(x) ∧ ¬happy(x) There exists an unhappy elephant.
Theorem. Let φ be a first-order formula, S a situation for first order logic. Then ¬∀x.φ is true in S iff ∃x.¬φ is true in S.
51/52
Mixed negated quantifiers
Here are four different expressions of the fact that there is no upper bound to the natural numbers.
We can shift from one to the other by negating the quantifiers.
¬∃m. ∀n. m≥n ∀m. ¬∀n. m≥n ∀m. ∃n. ¬m≥n ∀m. ∃n. m