Inference Rules

Basic rules:

mp

ϕ → ψ
ϕ
______
ψ

mt

ϕ → ψ
¬ψ
______
¬ϕ

dn

ϕ               ¬¬ϕ 
______          ______
¬¬ϕ             ϕ

r

ϕ 
______
ϕ


s

ϕ ∧ ψ               ϕ ∧ ψ
______              ______
ϕ                   ψ   

adj

ϕ                   ϕ
ψ                   ψ
______              ______
ϕ ∧ ψ               ψ ∧ ϕ   

add

ϕ                   ϕ
______              ______
ϕ ∨ ψ               ψ ∨ ϕ   

mtp

ϕ ∨ ψ               ϕ ∨ ψ
¬ψ                  ¬ϕ
______              ______
ϕ                   ψ   

cb

ϕ → ψ       
ψ → ϕ   
______              
ϕ ↔ ψ                   

bc

ϕ ↔ ψ               ϕ ↔ ψ
______              ______
ϕ → ψ               ψ → ϕ   


ui

∀αϕα
______
ϕβ

Provided that β is a name (or a variable) and ϕβ comes from ϕα by proper substitution of β for α.

eg

ϕβ
______
∃αϕα

Provided that α is a variable and ϕβ comes from ϕα by proper substitution of β for α.

ei

∃αϕα
______
ϕβ

Provided that β is a new variable and ϕβ comes from ϕα by proper substitution of β for α.



Derived rules:

nc (T40)

¬(ϕ → ψ)            ϕ ∧ ¬ψ
_________           _________
ϕ ∧ ¬ψ              ¬(ϕ → ψ)    

cdj (T45,T46)

ϕ → ψ               ¬ϕ ∨ ψ              ¬ϕ → ψ           ϕ ∨ ψ
_________           _________         _________         _________
¬ϕ ∨ ψ              ϕ → ψ               ϕ ∨ ψ            ¬ϕ → ψ

sc (T33,T49)

ϕ ∨ ψ           
ϕ → χ               ϕ → χ
ψ → χ               ¬ϕ → χ  
_________           _________
χ                   χ

dm (T63-T66)

¬(ϕ ∧ ψ)        (¬ϕ ∨ ¬ψ)           (ϕ ∧ ψ)            ¬(¬ϕ ∨ ¬ψ)
___________      ___________         ___________        ___________
 (¬ϕ ∨ ¬ψ)       ¬(ϕ ∧ ψ)           ¬(¬ϕ ∨ ¬ψ)         (ϕ ∧ ψ)


(ϕ ∨ ψ)          ¬(ϕ ∨ ψ)           ¬(¬ϕ ∧ ¬ψ)        (¬ϕ ∧ ¬ψ)
___________      ___________         ___________        ___________
¬(¬ϕ ∧ ¬ψ)       (¬ϕ ∧ ¬ψ)          (ϕ ∨ ψ)            ¬(ϕ ∨ ψ)

nb (T90)

¬(ϕ ↔ ψ)            (ϕ ↔ ¬ψ)            
_________           _________   
(ϕ ↔ ¬ψ)            ¬(ϕ ↔ ψ)            

qn (T203-T206)

¬∀xϕx           ¬∃xϕx            ∀xϕx           ∃xϕx
___________     ___________      ___________    ___________
 ∃x¬ϕx          ∀x¬ϕx            ¬∃x¬ϕx         ¬∀x¬ϕx


¬∀x¬ϕx          ¬∃x¬ϕx          ∀x¬ϕx           ∃x¬ϕx
___________     ___________     ___________     ___________
∃xϕx            ∀xϕx            ¬∃xϕx           ¬∀xϕx

av (T231-T232)

∀xϕx                    ∃xϕx
___________             ___________ 
∀yϕy                    ∃yϕy

Given the total proper substitution of y for x, and provided no variable capturing arises in ϕy.