Natural deduction is a collection of rules (inference rules) which allows us to infer new formulas from given formulas
Property
Natural deduction proofs for predicate logic are both sound and complete. That means anything you can prove with natural deduction can technically be proven with transformational proofs as well, and vice versa.
Forward proof: write down premises, and then add formulas that we can deduce from lines already in the proof until we reach the conclusion.
Inference Rules
Definition
An inference rule is a primitive valid argument form. Each inference rule enables the elimination or the introduction of a logical connective.
For example, and_i means and introduction, and and_e means and elimination.
Non-Exhaustive List of Rules
Introduction
Elimination
or_e is also known as the disjunctive syllogism
imp_e is also known as modus poens, and modus tollens for contrapositive
We can conclude anything we want for not_e, whatever suits our needs.
Case Analysis
Law of Excluded Middle (LEM)
The formulas above the line are premises of the rule, and below is the conclusion. The order of the formulas does not matter.
Premise
Strategy
and_e
cases, or_e
prove , imp_e
raa with
?
use lem (law of excluded middle) with cases
Example
Prove:
proof
Example
Prove:
proof
Example
Prove:
proof
Example
Prove:
proof
Example
Prove:
proof
Example
Prove:
proof
Example
Prove:
proof
Subproofs
Info
Some natural deduction rules are subordinate proofs (subproofs).
Conditional proofs (imp_i)
Proof by contradiction (raa, reductio ad absurdum)
Case analysis (cases)
Conditional Proof
Law
The implication introduction (deduction theorem):
Example
Prove:
proof
Example
Prove:
proof
Example
Prove:
proof
Proof by Contradiction
Law
The not introduction (proof by contradiction, reductio ad absurdum):
Example
Prove:
proof
Example
Example
If the train arrives late and there are no taxis at the station, then John is late for the meeting.
John is not late for his meeting.
The train did arrive late.
Therefore, there are taxis at the station.
Letter
Declarative Sentence
p
the train is late
q
there are taxis at the station
r
John is late for his meeting
Argument: Ifandnegation, then .
Not . .
Therefore, .