# Logical Operations

31-03-2022
rules

## Inference Rules

Basic rules:

mp

``````ϕ → ψ
ϕ
______
ψ``````

mt

``````ϕ → ψ
¬ψ
______
¬ϕ``````

dn

``````ϕ               ¬¬ϕ
______          ______
¬¬ϕ             ϕ``````

r

``````ϕ
______
ϕ``````

s

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

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

``````ϕ                   ϕ
______              ______
ϕ ∨ ψ               ψ ∨ ϕ   ``````

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: