COMP2022|2922
Models of Computation
Lesson 2b: Deduction in Propositional Logic
Presented by
Sasha Rubin
School of Computer Science
Deduction is a syntactic mechanism for deriving validities as well as logical consequences from assumptions
1/27
Deduction: motivation
– The most famous deductive system is surely found in Euclid’s Elements for deducing facts in elementary geometry and number theory.
– Euclid made some assumptions E1, · · · , Ek about points and lines …
– . . . and produced formal proofs that established logical consequences F such as
1. “the angles in a triangle sum to 180 degrees” 2. “there are infinitely many prime numbers”.
2/27
Deduction: Formal proofs
A deductive system gives you rules for constructing formal proofs.
Formal proofs:
1. A highly disciplined way of reasoning (good for computers)
2. A sequence of formulas where each step is a deduction based on earlier steps
3. Based entirely on rewriting formulas – no semantics.
3/27
Deduction: Formal proofs
– A formal proof usually starts with some assumptions. – Each step creates another formula which is justified by
applying an inference rule to formulas from previous steps. – If we manage to prove a formula F from assumptions
E1,··· ,Ek, then we will write
{E1,··· ,Ek}⊢F
which is read E1,··· ,Ek proves F.1
1The name of the symbol ⊢ is called “turnstile”.
4/27
|= is a semantic notion ⊢ is a syntactic notion
5/27
Natural deduction
We use a deductive system called Natural Deduction (ND).2
1. Every connective has two types of inference rules:
– Introduction rules introduce the connective – Elimination rules remove the connective
2. There is also a rule to introduce assumptions.
3. Some of the connective rules cancel assumptions.
4. In this system, → and ⊥ are not abbreviations.
5. If we collect all the assumptions {E1,··· ,Ek} that have not been cancelled at the end of the derivation, and if F is the last formula in the proof, then we write
{E1,··· ,Ek}⊢F
2Developed by Gerhard Gentzen (20th century German logician), and Stanisław Jaśkowski (20th century Polish logician).
6/27
Natural deduction
Here is one of the rules: (∧ E) Let’s analyse it:
S ⊢(A ∧ B) S⊢A
1. The name of the rule is (∧ E) which is read “Conjunction Elimination”.
2. S denotes a set of formulas, and A, B denote formulas.
3. We use this rule as follows: if we have proven (A ∧ B) using the formulas in S, then we can apply this rule to get a proof of A that uses the formulas in S.
4. This rule formalises the following type of reasoning: if we have a proof of (A∧B), then we have a proof of A.
7/27
Natural deduction
Let’s look at another rule: (∧I) Let’s analyse it:
S1 ⊢ A S2 ⊢ B S1 ∪ S2 ⊢(A ∧ B)
1. The name of the rule is (∧ I) which is read “Conjunction Introduction”.
2. S1 and S2 denote sets of formulas, and A, B denote formulas.
3. We use this rule as follows: if we have proven A using the formulas in S1, and we have proven B using the formulas in S2, then we can apply this rule to get a proof of (A ∧ B) that uses the formulas in S1 ∪ S2.
4. This rule formalises following type of reasoning: if we have a proof of A and we have a proof of B, then we have a proof of (A∧B).
8/27
Natural deduction: formal proofs
Here is how we will write a formal proof in ND.
1. Write the initial assumptions (sometimes called premises).
2. Devise a sequence of formulas, in which the last one is the desired conclusion.
3. Each step in the sequence must be:
– line numbered so that we can refer to it later in the proof, – annotated with the line numbers of the assumptions which
that step depends on,
– justified by the name of inference rule,
– annotated with the line numbers referenced by the justification.
Line
Assumptions
Formula
Justification
References
9/27
Natural deduction: formal proofs
Each line of the proof means the following:
If we know the assumptions hold, then we conclude the formula holds, because it can be justified by applying rule to the referenced lines above it.
Line
Assumptions
Formula
Justification
References
.
.
.
.
.
8
1,2,4
¬C
(∧ E)
4
.
.
.
.
.
10/27
Natural deduction: Rules involving ∧
(∧ E)
S ⊢(A ∧ B) S⊢A
(∧ E)
S ⊢(A ∧ B) S⊢B
(∧I)
S1 ⊢ A S2 ⊢ B S1 ∪ S2 ⊢(A ∧ B)
– The ∧E rules formalise the following reasoning: if we have a proof of (A∧B), then we have a proof of A and we have a proof of B.
– The ∧I rule formalises the following reasoning: if we have a proof of A and we have a proof of B, then we have a proof of (A∧B).
11/27
Natural deduction: Proof involving ∧ {(F ∧G)}⊢(G∧F)
Line 1
Assumptions 1
Formula
(F ∧ G)
Justification Asmp. I
References
2
1
F
∧E
1
3
1
G
∧E
1
4
1
(G∧F)
∧I
2,3
12/27
Natural deduction: Introducing an assumption
(Asmp. I)
{F}⊢F
– This rule allows one to introduce a formula F as an assumption, without reference to earlier lines.
– It’s only assumption is itself.
13/27
Natural deduction: rules involving →
(→ E) (→ I)
S1 ⊢A S2 ⊢(A→B) S1 ∪ S2 ⊢ B
S ∪ {A} ⊢ B S ⊢(A → B)
– The (→ E) rule formalises Modus Ponens.
– The (→ I) rule formalises that if we have a proof of B from A, then we have a proof of “if A then B”.
14/27
Natural deduction: proofs involving → The following consequence is called Hypothetical Syllogism (HS):
{(A → B),(B → C)}⊢(A → C)
Line
Assumptions
Formula
Justification
References
1
1
(A→B)
Asmp. I
2
2
(B→C)
Asmp. I
3
3
A
Asmp. I
4
1,3
B
→E
1,3
5
1,2,3
C
→E
2,4
6
1,2
(A → C)
→I
3,5
15/27
Natural deduction: rules involving ∨
(∨ I)
S⊢A
S ⊢(A ∨ B)
(∨ I)
S⊢A
S ⊢(B ∨ A)
(∨E) S1⊢(A∨B) S2∪{A}⊢C S3∪{B}⊢C S1 ∪ S2 ∪ S3 ⊢ C
– The ∨I rule formalises the following reasoning: if we have a proof of A, then we have a proof of (A ∨ B), and similarly we have a proof of (B ∨ A), no matter what B is.
– The ∨E rule formalises “reasoning by cases”: if we have a proof of (A∨B), a proof of C from A, and a proof of C from B, then we have a proof of C.
16/27
Natural deduction: proof involving ∨ {(A∨B),(A→C),(B→C)}⊢C
Line
Assumptions
Formula
Justification
References
1
1
(A∨B)
Asmp. I
2
2
(A→C)
Asmp. I
3
3
(B→C)
Asmp. I
4
4
A
Asmp. I
5
2,4
C
→E
2,4
6
6
B
Asmp. I
7
3,6
C
→E
3,6
8
1,2,3
C
∨E
1,4,5,6,7
Inline8,weuse(∨E)withS1 ={(A∨B)},S2 ={(A→C)}, S3 = {(B → C)}.
17/27
Natural deduction: proofs
The following consequence is called Constructive Dilemma (CD): {((A→B)∧(C →D)),(A∨C)}⊢(B∨D)
Line
Assumptions
Formula
Justification
References
1
1
(A→B) ∧ (C → D)
Asmp. I
2
2
(A∨C)
Asmp. I
3
1
(A→B)
∧E
1
4
1
(C → D)
∧E
1
5
5
A
Asmp. I
6
1,5
B
→E
3,5
7
1,5
(B ∨ D)
∨I
6
8
8
C
Asmp. I
9
1,8
D
→E
4,8
10
1,8
(B ∨ D)
∨I
9
11
1,2
(B ∨ D)
∨E
2,5,7,8,10
18/27
Natural deduction: rules involving ¬
(¬ E) (¬ I)
S1 ⊢ A S2 ⊢ ¬A S1 ∪ S2 ⊢ ⊥
S ∪ {A} ⊢ ⊥ S ⊢ ¬A
– The (¬ E) rule formalises that ⊥ follows from any contradiction.
– The (¬ I) rule formalises that we have a proof of ⊥ from A, then we have a proof of ¬A.
19/27
Natural deduction: proofs
{F}⊢¬¬F
Line
Assumptions
Formula
Justification
References
1
1
F
Asmp. I
2
2
¬F
Asmp. I
3
1,2
⊥
¬E
1,2
4
1
¬¬F
¬I
2,3
To show
we can continue the proof above with one more line:
∅⊢F →¬¬F
5
F → ¬¬F
→I
1,4
20/27
Natural deduction: proofs
The following consequence is called Modus Tollens: {(F →G),¬G}⊢¬F
Line
Assumptions
Formula
Justification
References
1
1
(F → G)
Asmp. I
2
2
¬G
Asmp. I
3
3
F
Asmp. I
4
1,3
G
→E
1,3
5
1,2,3
⊥
¬E
2,4
6
1,2
¬F
¬I
3,5
21/27
Natural deduction: another rule
(⊥)
S⊢⊥ S⊢A
– The (⊥) rule formalises that from a false assumption, anything can be derived.
22/27
Natural deduction: proofs
{(F ∨G),¬G}⊢F
Line
Assumptions
Formula
Justification
References
1
1
(F ∨ G)
Asmp. I
2
2
¬G
Asmp. I
3
3
G
Asmp. I
4
2,3
⊥
¬E
2,3
5
2,3
F
⊥
4
6
6
F
Asmp. I
7
1,2
F
∨E
1,3,5,6,6
Weapply(∨E)usingS1 ={(F∨G)},S2 =∅,S3 ={¬G}
23/27
Natural deduction: last rule
(RA)
S ∪ {¬A} ⊢ ⊥ S⊢A
– The (RA) rule is called Reductio ad absurdum or Reduction to the absurd. It formalises the method of proof by contradiction: if the assumption that A is false (i.e., that ¬A is true) leads to a contradiction, then A must be true.
24/27
Natural deduction: proofs
{¬¬F}⊢F
Line
Assumptions
Formula
Justification
References
1
1
¬¬F
Asmp. I
2
2
¬F
Asmp. I
3
1,2
⊥
¬E
1,2
4
1
F
RA
2,3
We apply (RA) using S = {¬¬F }.
25/27
Natural Deduction: wrap-up
We should definitely ask two questions about Natural Deduction:
1. Can it prove only logical consequences? Such a system is
called sound.
2. Can it prove all logical consequences? Such a system is called
complete.
Roughly speaking:
1. A deductive system that is not sound might give us wrong results.
– E.g., it might have a proof of (B→A) from (A→B).
2. A deductive system that is not complete might not give us all the right results.
– E.g., it might not have a proof of ¬¬A from A.
Theorem
Natural deduction for propositional logic is sound and complete.
26/27
For you think about
How does the following idea apply to Natural Deduction for propositional logic?
In Computer Science we start with the simplest possible systems, and sets of rules that we haven’t necessarily confirmed by experiment, but which we just suppose are true, and then ask what sort of complex systems we can and cannot build. . . it is a mathematical set of tools, or body of ideas, for understanding just about any system—brain, universe, living organism, or, yes, computer.
Scott Aaronson — theoretical computer scientist
27/27