Logic (PHIL 2080, COMP 2620, COMP 6262) Chapter: Propositional Natural Deduction — Conjunction, Implication, Theorems
Logic (PHIL 2080, COMP 2620, COMP 6262)
Chapter: Propositional Natural Deduction
— Conjunction, Implication, Theorems
Pascal Bercher
Planning & Optimization
Yoshihiro Maruyama
Logic
Intelligent Agents
College of Engineering and Computer Science
the Australian National University (ANU)
2 & 4 March 2021
Introduction Conjunction Implication Theorems Summary
Introduction
Pascal Bercher and Yoshihiro Maruyama 1.30
Introduction Conjunction Implication Theorems Summary
Recap on Connectives: Syntax
The main connective dictates the type of a formula:
if main connective is ¬, formula is a negation
… ∧, … conjunction
… ∨, … disjunction
… →, … implication
… ↔, … double-implication
Pascal Bercher and Yoshihiro Maruyama 2.30
Introduction Conjunction Implication Theorems Summary
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:
p ¬
0 1
1 0
p q ∧
0 0 0
0 1 0
1 0 0
1 1 1
p q ∨
0 0 0
0 1 1
1 0 1
1 1 1
p q →
0 0 1
0 1 1
1 0 0
1 1 1
Pascal Bercher and Yoshihiro Maruyama 3.30
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., can we write “(p → q)→ (p → r) ` p → (q → r)”?
` is a consequence relation!
• If A is in X , then X ` A (reflexivity)
• If X ` A, then X ∪ Y ` A for all Y (monotonicity)
• If X ` A and Y ,A ` B, then X ,Y ` B (transitivity)
Thus, X ` A if there exists a “derivation” of A from X .
Pascal Bercher and Yoshihiro Maruyama 4.30
Introduction Conjunction Implication Theorems Summary
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
• . . . from X : these are the formulae that we start from
and that we manipulate to end up in A.
Pascal Bercher and Yoshihiro Maruyama 5.30
Introduction Conjunction Implication Theorems Summary
Conjunction
Pascal Bercher and Yoshihiro Maruyama 6.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
∧E
A ∧ B
B
∧E
Which reads: If we derived A ∧ B, we can derive both A and B.
Pascal Bercher and Yoshihiro Maruyama 7.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: And-Introduction
What are the 1-step rules for dealing with conjunction?
Introduction rule:
A B
A ∧ B
∧I
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
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!)
Pascal Bercher and Yoshihiro Maruyama 9.30
Introduction Conjunction Implication Theorems Summary
Proof Syntax / Notation: Tree-like Representation, Example
Assume we want to prove p ∧ q ` q ∧ p
Sequence of derivations: p ∧ q︸ ︷︷ ︸
premise
, q︸︷︷︸
∧E
, p︸︷︷︸
∧E
, q ∧ p︸ ︷︷ ︸
∧I and conclusion
In the tree-like format:
p ∧ q
q
∧E
p ∧ q
p
∧E
q ∧ p
∧I
Leaves are assumptions, root is conclusion
Advantages: Makes the proof structure obvious
In exercises, etc: Do not use it, unless we ask you to!
Pascal Bercher and Yoshihiro Maruyama 10.30
Introduction Conjunction Implication Theorems Summary
Proof Syntax / Notation: List Representation, Example
Assume we want to prove p ∧ q ` q ∧ p
Sequence of derivations: p ∧ q︸ ︷︷ ︸
premise
, q︸︷︷︸
∧E
, p︸︷︷︸
∧E
, q ∧ p︸ ︷︷ ︸
∧I and conclusion
In the list format:
α1 (1) p ∧ q A
α1 (2) q 1 ∧E
α1 (3) p 1 ∧E
α1 (4) q ∧ p 2, 3 ∧I
≡ p ∧ q ` p ∧ q
≡ p ∧ q ` q
≡ p ∧ q ` p
≡ p ∧ q ` q ∧ p
column 1: assumption number column 2: line number
column 3: derivation column 4: how it was derived
Note: Each line represents a sequent! (Sequence of sequents.)
Pascal Bercher and Yoshihiro Maruyama 11.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules (Based on Sequents): Derivation Rules
Derivation Rules as considered so far:
A ∧ B
A
∧E
A ∧ B
B
∧E
A B
A ∧ B
∧I
Re-written in terms of sequents:
X ` A ∧ B
X ` A
∧E
X ` A ∧ B
X ` B
∧E
X ` A Y ` B
X ,Y ` A ∧ B
∧I
→ I.e., now we see how premises accumulate!
Pascal Bercher and Yoshihiro Maruyama 12.30
Introduction Conjunction Implication Theorems Summary
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 (reflexivity)
≡ q ` q (reflexivity)
≡ p, q ` p ∧ q (∧I)
Pascal Bercher and Yoshihiro Maruyama 13.30
Introduction Conjunction Implication Theorems Summary
Implication
Pascal Bercher and Yoshihiro Maruyama 14.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 :
I All tigers are carnivores (p)
I Timmy is a tiger (q)
}
premises
I Thus, Timmy is a carnivore (r)
}
conclusion
This reasoning is (also) called deduction
Pascal Bercher and Yoshihiro Maruyama 15.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Elimination and -Introduction
Elimination rule:
A→ B A
B
→E
Introduction rule:
[A]
…
B
A→ B
→I
The [X ] indicates that assumption X gets discharged, i.e., we do
not rely on it anymore.
Pascal Bercher and Yoshihiro Maruyama 16.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Elimination and -Introduction (Based on Sequents)
Derivation Rules as considered so far:
A→ B A
B
→E
[A]
…
B
A→ B
→I
Re-written in terms of sequents:
X ` A→ B Y ` A
X ,Y ` B
→E
X ,A ` B
X ` A→ B
→I︸ ︷︷ ︸
Has side effect of
removing the assumption A
We say that A gets discharged, and annotate that in the proof.
Pascal Bercher and Yoshihiro Maruyama 17.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Deduction Equivalence
X ` A→ B iff X ,A ` B︸ ︷︷ ︸
deduction equivalence
(or deduction theorem)
Why does this hold?
If X ,A ` B, then X ` A→ B: X ,A ` B
X ` A→ B
→I
If X ` A→ B, then X ,A ` B: X ` A→ B Y ` A
X ,Y ` B
→E
X ` A→ B A ` A
X ,A ` B
→E
Pascal Bercher and Yoshihiro Maruyama 18.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Deduction Equivalence
X ` A→ B iff X ,A ` B︸ ︷︷ ︸
deduction equivalence
(or deduction theorem)
Why does this hold?
If X ,A ` B, then X ` A→ B: X ,A ` B
X ` A→ B
→I
If X ` A→ B, then X ,A ` B: X ` A→ B A ` A
X ,A ` B
→E
Pascal Bercher and Yoshihiro Maruyama 18.30
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 (3) p ∧ q 1, 2 ∧I
α1 (4) q → (p ∧ q) 3[α2]→I
α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.
Pascal Bercher and Yoshihiro Maruyama 19.30
X ,A ` B
X ` A→ B
→I
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 (3) p ∧ q 1, 2 ∧I
α1 (4) q → (p ∧ q) 3[α2]→I
α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.
Pascal Bercher and Yoshihiro Maruyama 19.30
X ,A ` B
X ` A→ B
→I
Introduction Conjunction Implication Theorems Summary
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 2 ∧E
α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 20.30
Introduction Conjunction Implication Theorems Summary
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 2 ∧E
α1, α2 (4) q 1, 3→E
α1 (5) (p ∧ r)→ q 4[α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 20.30
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 → q
[p ∧ r ](1)
p
q
→E
(p ∧ r)→ q
→I(1)
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).
Pascal Bercher and Yoshihiro Maruyama 21.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) p ∧ q 2, 3 ∧I
α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 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) p ∧ q 2, 3 ∧I
α1, α2, α3 (5) r 1, 4→E
α1, α2 (6) q → r 5[α3]→I
α1 (7) p → (q → r) 6[α2]→I
Pascal Bercher and Yoshihiro Maruyama 22.30
Introduction Conjunction Implication Theorems Summary
The 1-Step Rules: Implication-Introduction and -Elimination, Example 3
p ` (q → r)→ (q → (p ∧ r))
α1 (1) p A
α2 (2) q → r A
α3 (3) q A
α2, α3 (4) r 2, 3→E
α1, α2, α3 (5) p ∧ r 1, 4 ∧I
α1, α2 (6) q → (p ∧ r) 5[α3]→I
α1 (7) (q → r)→ (q → (p ∧ r)) 6[α2]→I
α1, α2, α3 (n − 2) p ∧ r
α1, α2 (n − 1) q → (p ∧ r) (n − 2)[α3]→I
α1 (n) (q → r)→ (q → (p ∧ r)) (n − 1)[α2]→I
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.
p ` q → p
α1 (1) p A
α1 (2) q → p 1[]→I
p ` q → p
α1 (1
′) p A
α2 (2
′) q A
α1 (3
′) q → p 1[α2]→I
We call “such a” discharge a vacuous discharge.
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.)
Pascal Bercher and Yoshihiro Maruyama 24.30
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 → p and ¬(q → p), or we can “write down”
• p → (q → p) and ¬(p → (q → p))
→ But which is true? We can state that with `!
Pascal Bercher and Yoshihiro Maruyama 25.30
Introduction Conjunction Implication Theorems Summary
Theorems
Pascal Bercher and Yoshihiro Maruyama 26.30
Introduction Conjunction Implication Theorems Summary
Unconditionally True Formulas
Furmulae that do not depend on anything are called theorems!
A is a theorem if “` A”, e.g., ` p → (q → p).
Another (slightly more complex) example:
α1 (1) p A
α2 (2) q A
α1, α2 (3) p ∧ q 1, 2 ∧I
α1 (4) q → (p ∧ q) 3[α2]→I
(5) p → (q → (p ∧ q)) 4[α1]→I
Thus, we get ` p → (q → (p ∧ q)), so its formula is a theorem.
Pascal Bercher and Yoshihiro Maruyama 27.30
Introduction Conjunction Implication Theorems Summary
From Arbitrary Sequents to Theorems
Recall that our example from the last couple of slides:
• We proved p ` q → p, and
• (we claimed that) ` 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.)
Pascal Bercher and Yoshihiro Maruyama 28.30
Introduction Conjunction Implication Theorems Summary
Summary
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
Introduction
Conjunction
The 1-Step Rules
Proof Syntax / Notation
The 1-Step Rules (Based on Sequents)
Implication
Introduction
The 1-Step Rules
Vacous Discharge
Excursion: vs.
Theorems
Summary