Introduction Conjunction Implication Theorems Summary
Logic (PHIL 2080, COMP 2620, COMP 6262) Chapter: Propositional Natural Deduction — Conjunction, Implication, Theorems
Planning & Optimization
Logic Intelligent Agents
College of Engineering and Computer Science the Australian National University (ANU)
2 & 4 March 2021
Introduction
Introduction Conjunction Implication Theorems Summary
The main connective dictates the type of a formula: if main connective is ¬, formula is a negation
Pascal Bercher and Yoshihiro Maruyama 1.30
Introduction Conjunction Implication Theorems Summary
Recap on Connectives: Syntax
Recap on Connectives: Semantics (Teaser)
What do these connectives mean?
The semantics will be covered formally in a later section, so this
is just a “teaser”!
The “intended meaning” of connectives can be expressed by truth tables:
… … … …
∧, … ∨, … →, … ↔, …
conjunction disjunction implication double-implication
pq∧ pq∨ pq→
p¬
000 000 001 01 010 011 011 10 100 101 100
111 111 111
Pascal Bercher and Yoshihiro Maruyama 2.30
Pascal Bercher and Yoshihiro Maruyama 3.30
Introduction Conjunction Implication Theorems Summary
Introduction Conjunction Implication Theorems Summary
Recap on Sequents
Sequents describe valid arguments, by expressing that the conclusion follows from the premises, e.g.,
X ⊢ A means that A follows from X.
The validity might not be obvious!
E.g.,canwewrite“(p →q)→(p →r)⊢p →(q →r)”? ⊢ is a consequence relation!
Natural Deduction and Derivations
Manipulates sequents step-wise, thus generating a sequence of sequents, thus, in the end, deriving the sequent in question
Natural deduction is pure syntax manipulation and acts as proof system
A derivation is a finite sequence of formulae, which are derived from each other based on elementary formula manipulations (“1-step inference rules”)
• A derivation of A: A is the last formula
• IfAisinX,thenX ⊢A
• IfX ⊢A,thenX ∪Y ⊢AforallY
• IfX ⊢AandY,A⊢B,thenX,Y ⊢B
(reflexivity) (monotonicity) (transitivity)
Thus, X ⊢ A if there exists a “derivation” of A from X.
•
. . . from X : these are the formulae that we start from and that we manipulate to end up in A.
Pascal Bercher and Yoshihiro Maruyama 4.30
Introduction Conjunction Implication Theorems Summary
Pascal Bercher and Yoshihiro Maruyama 5.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: And-Elimination
What are the 1-step rules for dealing with conjunction?
Elimination rule:
A∧B A∧B ∧E ∧E
AB
Which reads: If we derived A ∧ B, we can derive both A and B.
Conjunction
Pascal Bercher and Yoshihiro Maruyama 6.30
Pascal Bercher and Yoshihiro Maruyama 7.30
Introduction Conjunction Implication Theorems Summary
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: And-Introduction
What are the 1-step rules for dealing with conjunction?
Introduction rule:
AB
∧I A∧B
Proof Syntax / Notation: Overview
How to write down proofs?
There are many different notations that describe the same thing We introduce two:
• Tree-like representation of the applied rules (just since it’s another standard)
• list-like representation (only use that one!)
Which reads: If we derived A and we derived B, we can derive A ∧ B.
Pascal Bercher and Yoshihiro Maruyama 8.30
Introduction Conjunction Implication Theorems Summary
Assume we want to prove p ∧ q ⊢ q ∧ p Sequenceofderivations: p∧q , q , p
,
q∧p
∧I and conclusion
Pascal Bercher and Yoshihiro Maruyama 9.30
Introduction Conjunction Implication Theorems Summary
Proof Syntax / Notation: Tree-like Representation, Example
In the tree-like format:
premise ∧E
∧E
p∧q p∧q ∧E ∧E
qp
∧I q∧p
Leaves are assumptions, root is conclusion Advantages: Makes the proof structure obvious
In exercises, etc: Do not use it, unless we ask you to!
Proof Syntax / Notation: List Representation, Example
Assume we want to prove p ∧ q ⊢ q ∧ p Sequenceofderivations: p∧q , q , p
,
q∧p
∧I and conclusion
In the list format:
α1 (1) p∧q A
≡ p∧q⊢p∧q ≡ p∧q⊢q
≡ p∧q⊢p
≡ p∧q⊢q∧p
column 2: line number column 4: how it was derived
α1 (2) q
α1 (3) p
α1 (4) q ∧ p
1∧E 1∧E 2, 3 ∧I
column 1: assumption number column 3: derivation
premise
∧E ∧E
Note: Each line represents a sequent! (Sequence of sequents.)
Pascal Bercher and Yoshihiro Maruyama 10.30
Pascal Bercher and Yoshihiro Maruyama 11.30
Introduction Conjunction Implication Theorems Summary
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules (Based on Sequents): Derivation Rules
Derivation Rules as considered so far:
A∧B A∧B A B ∧E ∧E ∧I
ABA∧B Re-written in terms of sequents:
X⊢A∧B X⊢A∧B X⊢A Y⊢B ∧E ∧E ∧I
X ⊢A X ⊢B X,Y ⊢A∧B → I.e., now we see how premises accumulate!
The 1-Step Rules (Based on Sequents):
Accumulation of Assumptions, Example
p, q ⊢ p ∧ q α1(1)p A
α2(2)q A
α1, α2 (3) p ∧ q 1, 2 ∧I
≡ p ⊢ p
≡ q ⊢ q
≡ p, q ⊢ p ∧ q
(reflexivity) (reflexivity) (∧I)
Pascal Bercher and Yoshihiro Maruyama 12.30
Introduction Conjunction Implication Theorems Summary
Pascal Bercher and Yoshihiro Maruyama 13.30
Introduction Conjunction Implication Theorems Summary
Introduction
Now we consider the “if . . . , then . . . ” connective: implication! E.g.,
• p → q: “if it is raining (p), then the ground is wet (q)” • Here, p is the antecedent and q the consequent
• (p∧q)→r:
Implication
All tigers are carnivores (p)
Timmy is a tiger (q)
Thus,Timmyisacarnivore(r)
premises conclusion
This reasoning is (also) called deduction
Pascal Bercher and Yoshihiro Maruyama 14.30
Pascal Bercher and Yoshihiro Maruyama 15.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Elimination and -Introduction
Elimination rule:
Introduction rule:
A→B A
→E B
[A] .
B
→I
A→B
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Elimination and -Introduction (Based on Sequents)
[A] .
A→BAB
→E →I
B A→B Re-written in terms of sequents:
Derivation Rules as considered so far:
X ⊢A→B X,Y ⊢B
Y ⊢A
→E
X,A⊢B X ⊢A→B
→I
The [X ] indicates that assumption X gets discharged, i.e., we do not rely on it anymore.
We say that A gets discharged, and annotate that in the proof.
Pascal Bercher and Yoshihiro Maruyama 16.30
Introduction Conjunction Implication Theorems Summary
X⊢A→B iff X,A⊢B
deduction equivalence (or deduction theorem)
Pascal Bercher and Yoshihiro Maruyama 17.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Deduction Equivalence
The 1-Step Rules: Deduction Equivalence
X⊢A→B iff X,A⊢B
deduction equivalence (or deduction theorem)
Has side effect of removing the assumption A
Why does this hold? IfX,A⊢B,thenX ⊢A→B:
IfX ⊢A→B,thenX,A⊢B:
X,A ⊢ B
→I
X⊢A→B X⊢A→B Y⊢A
X,Y ⊢B
→E
Why does this hold? IfX,A⊢B,thenX ⊢A→B:
IfX ⊢A→B,thenX,A⊢B:
X,A ⊢ B
→I
X⊢A→B X⊢A→B A⊢A
X,A ⊢ B
→E
Pascal Bercher and Yoshihiro Maruyama 18.30
Pascal Bercher and Yoshihiro Maruyama 18.30
Introduction Conjunction Implication Theorems Summary
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Introduction, Example 1
p ⊢ q → (p ∧ q) α1(1)p A
α2(2)q A
α1,α2 (n−1) p∧q
α1 (n) q → (p ∧ q) (n − 1)[α2] →I
Assumption α2 is a new one, which was not given in the original sequent, so we need to eliminate it later on.
In the last step, we discharge assumption α2 = q.
The 1-Step Rules: Implication-Introduction, Example 1
p ⊢ q → (p ∧ q)
α1(1)p A α2(2)q A
X,A ⊢ B
→I
X⊢A→B
α1, α2 (3) p ∧ q
α1 (4) q → (p ∧ q)
α1,α2 (n−1) p∧q
α1 (n) q → (p ∧ q)
1, 2 ∧I 3[α2] →I
(n − 1)[α2] →I
Assumption α2 is a new one, which was not given in the original
sequent, so we need to eliminate it later on.
In the last step, we discharge assumption α2 = q.
Pascal Bercher and Yoshihiro Maruyama 19.30
Introduction Conjunction Implication Theorems Summary
p → q ⊢ (p ∧ r ) → q α1(1)p→q A
α2(2)p∧r A α1,α2 (n−1) q
α1 (n) (p ∧ r) → q (n − 1)[α2] →I
Assumption α2 is a new one, which was not given in the original
sequent, so we need to eliminate it later on. In the last step, we discharge assumption α2.
Pascal Bercher and Yoshihiro Maruyama 19.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Introduction and -Elimination, Example 1
The 1-Step Rules: Implication-Introduction and -Elimination, Example 1
p → q ⊢ (p ∧ r ) → q
α1(1)p→q A α2(2)p∧r A
α2 (3) p α1,α2 (4) q
α1 (5) (p ∧ r) → q
Assumption α2 is a new one, which was not given in the original
sequent, so we need to eliminate it later on. In the last step, we discharge assumption α2.
2∧E 1,3 →E 4[α2] →I
X,A ⊢ B
→I
X⊢A→B
Pascal Bercher and Yoshihiro Maruyama 20.30
Pascal Bercher and Yoshihiro Maruyama 20.30
Introduction Conjunction Implication Theorems Summary
Here, we denote discharged assumptions by [. . . ](n), where we number each assumption so that they can be distinguished from each other, i.e., so that we know which rule discharged which assumption(s).
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Introduction and -Elimination, Example 1 (cont’d)
The proof of p → q ⊢ (p ∧ r) → q in a tree-like structure:
[p ∧ r ](1)
p→q
p
q
(p ∧ r ) → q
→E →I(1)
The 1-Step Rules: Implication-Introduction and -Elimination, Example 2
(p ∧ q) → r ⊢ p → (q → r)
α1 (1) (p ∧ q) → r A α2(2)p A α3(3)q A
α1,α2,α3 (n−2) r
α1,α2 (n−1) q→r (n−2)[α3]→I
α1 (n) p → (q → r) (n − 1)[α2] →I
Pascal Bercher and Yoshihiro Maruyama 21.30
Introduction Conjunction Implication Theorems Summary
Pascal Bercher and Yoshihiro Maruyama 22.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Introduction and -Elimination, Example 2
(p ∧ q) → r ⊢ p → (q → r)
α1 (1) (p ∧ q) → r A α2(2)p A α3(3)q A
α2,α3 (4) α1, α2, α3 (5) α1,α2 (6) α1 (7)
p∧q 2,3∧I
r 1,4→E q→r 5[α3]→I p→(q→r) 6[α2]→I
The 1-Step Rules:
α1 α2 α3
α2,α3 α1, α2, α3 α1,α2 α1
Implication-Introduction and -Elimination, Example 3
(1) (2) (3) (4) (5) (6) (7)
p ⊢ (q → r ) → (q → (p ∧ r )) p
q→r
q
r
p∧r
q→(p∧r)
(q →r)→(q →(p∧r))
p∧r
q → (p ∧ r )
(q →r)→(q →(p∧r))
A
A
A
2, 3 →E 1, 4 ∧I 5[α3] →I 6[α2] →I
(n − 2)[α3] →I (n − 1)[α2] →I
α1,α2,α3 (n−2) α1,α2 (n − 1)
α1 (n)
Pascal Bercher and Yoshihiro Maruyama 22.30
Pascal Bercher and Yoshihiro Maruyama 23.30
Introduction Conjunction Implication Theorems Summary
Vacous Discharge: Discharging Non-existent Assumptions
We can “discharge” assumptions that are not there; this “happens” if the conclusion does not depend on its assumption.
Introduction Conjunction Implication Theorems Summary
Excursion: ⊢ vs. →: An Often Asked Question in Previous Courses
⊢ and → seem to be of a very related nature: E.g., compare A, B ⊢ C with A ∧ B → C
So what’s the difference?
→ is simply some logical connective, i.e., part of a formula.
⊢ is used to introduce a proof system based on syntax manipulation. It makes propositions about formulae.
E.g., we know by now what p ⊢ q → p means, but “just a formula” can be both true or false!
E.g., we can write down both
• q→pand¬(q→p),orwecan“writedown”
• p →(q →p)and¬(p →(q →p))
→ But which is true? We can state that with ⊢!
p⊢q→p α1 (1) p
α1 (2) q → p
We call “such a” discharge a vacuous discharge.
A
A
1[α2] →I
A
1[] →I
α2 (2′) q
α1 (3′) q → p
Even explicitly making this assumption does not “help”, as the formula (i.e., line 3′) simply does not rely on it. (So writing “1[α2] →I” in line line 3′ does not make much sense.)
p⊢q→p α1 (1′) p
Pascal Bercher and Yoshihiro Maruyama 24.30
Introduction Conjunction Implication Theorems Summary
Pascal Bercher and Yoshihiro Maruyama 25.30
Introduction Conjunction Implication Theorems Summary
Unconditionally True Formulas
Furmulae that do not depend on anything are called theorems! Aisatheoremif“⊢A”,e.g.,⊢p →(q →p).
Another (slightly more complex) example:
α1 (1) p
α2 (2) q
α1,α2 (3)p∧q
α1 (4) q→(p∧q)
(5) p→(q→(p∧q))
Thus, we get ⊢ p → (q → (p ∧ q)), so
A
A
1, 2 ∧I 3[α2] →I 4[α1]→I
its formula is a theorem.
Theorems
Pascal Bercher and Yoshihiro Maruyama 26.30
Pascal Bercher and Yoshihiro Maruyama 27.30
Introduction Conjunction Implication Theorems Summary
Introduction Conjunction Implication Theorems Summary
From Arbitrary Sequents to Theorems
Recall that our example from the last couple of slides: • Weprovedp ⊢q →p,and
• (weclaimedthat)⊢p →(q →p)
We can generalize this to obtain arbitrarily many theorems! How? Remember the deduction equivalence!
X⊢A→B iff X,A⊢B
This means we can just “move” all assumptions as antecedents into the formula! (Just apply that equivalence recursively.)
Summary
Pascal Bercher and Yoshihiro Maruyama 28.30
Pascal Bercher and Yoshihiro Maruyama 29.30
Introduction Conjunction Implication Theorems Summary
Content of this Lecture
The most important basics of Natural deduction!
• How can proofs be written?
• What does X ⊢ A mean?
• Every logical connective comes with two 1-step rules:
Introduction and Elimination
• What’s a theorem?
→ The entire Logic Notes sections:
• Propositional natural deduction: Conjunction
• Propositional natural deduction: Implication
• Propositional natural deduction: Counting assumptions
(except Contraction, read it up!)
Pascal Bercher and Yoshihiro Maruyama 30.30