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.