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ϕyGiven the total proper substitution of y for x, and provided no variable capturing arises in ϕy.