Natural deduction

The truth table and the Davis-Putnam algorithm do not explain why a formula is a tautology. The natural deduction is a way to build tautologies. For this, for each operator there are rules for creating the operator (Introduction rules) and rules for using the operator (Elimination rules).

Conjunction

Introduction

A         B
A ∧ B

Elimination

A ∧ B
A

A ∧ B
B

Example

A ∧ B
B
A ∧ B
A
B ∧ A

Disjunction

Introduction

A
A ∨ B

B
A ∨ B

Elimination

 
 
 
A ∨ B
[A]
.
.
C
[B]
.
.
C
C

Example

 
A ∨ B
A
B ∨ A
B
B ∨ A
B ∨ A

Implication

Introduction

[A]
.
.
B
A ⇒ B

Elimination

A ⇒ B         A
B

Example

A ⇒ B         A
B
 
B ⇒ C
C
A ⇒ C
(B ⇒ C) ⇒ (A ⇒ C)
(A ⇒ B) ⇒ ((B ⇒ C) ⇒ (A ⇒ C))

N.B. All the hypotheses of the proof have been introduced by the introduction rule. Hence, the conclusion is a tautology.

Equivalence

Introduction

[A]
.
.
B
       
[B]
.
.
A
A ≡ B

Elimination

 
 
 
A ≡ B
       
 
 
 
A
       
[B]
.
.
C
C
 
 
 
A ≡ B
       
 
 
 
B
       
[A]
.
.
C
C

Example

A ≡ B         B         A
A
       
A ≡ B         A         B
B
B ≡ A
       
B ≡ A         A         B
B
       
B ≡ A         B         A
A
A ≡ B
(A ≡ B) ≡ (B ≡ A)

False

Elimination

False
A

Negation

Introduction

[A]
.
.
False
¬A

Elimination

A         ¬A
False

Example

 
 
 
(A ∨ ¬B) ∧ B
A ∨ ¬B
       
 
 
 
 
A
       
(A ∨ ¬B) ∧ B
B
 
¬B
False
A
A
((A ∨ ¬B) ∧ B) ⇒ A

Exercises

E1. Find a proof of ((A ∨ B) ⇒ C) ≡ ((A ⇒ C) ∧ (B ⇒ C)).

E2. Find a proof of (A ⇒ B) ⇒ (B ⇒ A).

E3. Find a proof of A ⇒ ¬¬A.

E4*. Find a proof of A ⇒ (A ∧ A).

E5*. Find a proof of ((A ∨ B) ∧ (A ⇒ B)) ⇒ B.

E6*. Find a proof of (A ∨ B) ⇒ ((A ⇒ C) ⇒ ((B ⇒ C) ⇒ C)).

E7*. Find a proof of ((A ∧ B) ∧ C) ⇒ (A ∧ (B ∧ C)).

E8*. Find a proof of ((A ⇒ C) ∧ (B ⇒ C)) ⇒ ((A ∨ B) ⇒ C).

E9*. Find a proof of ((A ∨ B) ∧ (A ∨ ¬B)) ⇒ A.

E10*. Find a proof of ((A ∨ ¬B) ∧ B) ⇒ A.

E11*. Find a proof of ((A ⇒ B) ∧ (B ⇒ ¬A)) ⇒ ¬A.

E12*. Find a proof of ((A ⇒ ¬B) ∧ B) ⇒ ¬A.

Classical Logic

With the previous rules we do not have yet the usual logic. To have such logic, we need A ∨ ¬A to be true for any formula A. So, we change the rule:

False
A

with:

[¬A]
.
.
False
A

Example

Now it is possible to prove A ∨ ¬A:

¬A
A ∨ ¬A
       
 
¬ (A ∨ ¬A)
False
A
       
A
A ∨ ¬A
       
 
¬ (A ∨ ¬A)
False
¬A
False
A ∨ ¬A

Exercises

E13. Find a proof of ¬¬A ⇒ A.

E14. Find a proof of ((A ⇒ B) ⇒ A) ⇒ A.

E15. Find a proof of ((A ⇒ B) ∨ C) ⇒ ((A ⇒ C) ∨ B).

Monica Nesi