Logical Operations

31-03-2022
rules

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.

I also (occasionally) write an email newsletter! You can subscribe here if you're interested: