Our propositional inference rules
| Abbreviation |
Name |
If you know all of… |
…then you can infer |
| ∧∧Intro |
and-introduction |
|
(φ∧ψ)(φ∧ψ) |
| ∧∧Elim |
and-elimination (left) |
(φ∧ψ)(φ∧ψ) |
φφ |
| and-elimination (right) |
(φ∧ψ)(φ∧ψ) |
ψψ |
| ∨∨Intro |
or-introduction (left) |
φφ |
(φ∨ψ)(φ∨ψ) |
| or-introduction (right) |
ψψ |
(φ∨ψ)(φ∨ψ) |
| ∨∨Elim |
or-elimination |
| φ ⊢ θφ ⊢ θ |
| ψ ⊢ θψ ⊢ θ |
| (φ∨ψ)(φ∨ψ) |
|
θθ |
| →→Intro |
if-introduction |
φ, ψ, …, θ ⊢ ωφ, ψ, …, θ ⊢ ω |
((φ∧ψ∧…∧θ)→ω)((φ∧ψ∧…∧θ)→ω) |
| →→Elim |
if-elimination (modus ponens) |
|
ψψ |
| falseIntro |
false-introduction |
|
false |
| falseElim |
false-elimination |
false |
φφ |
| RAA |
reductio ad absurdum (v. 1) |
¬φ ⊢ false¬φ ⊢ |
φφ |
| reductio ad absurdum (v. 2) |
φ ⊢ falseφ ⊢ |
¬φ¬φ |
| ¬¬Intro |
negation-introduction |
φφ |
¬¬φ¬¬φ |
| ¬¬Elim |
negation-elimination |
¬¬φ¬¬φ |
φφ |
| CaseElim |
case-elimination (left) |
|
ψψ |
| case-elimination (right) |
|
φφ |
As usual, φφ, ψψ, θθ, ωω
are meta-variables standing for any WFF.
This is by no means the only
possible inference system for propositional logic.
This set of inference rules is based upon
Discrete Mathematics with a Computer
by Hall and O'Donnell (Springer, 2000) and
The Beseme Project.
