A.4. Derivation rules
Basic system
Rules for developing gaps
|
|
for resources
|
for goals
|
atomic
sentence
|
|
IP
|
negation
¬ φ
|
CR
(if φ not atomic
& goal is ⊥)
|
RAA
|
conjunction
φ ∧ ψ
|
Ext
|
Cnj
|
disjunction
φ ∨ ψ
|
PC
|
PE
|
conditional
φ → ψ
|
RC
(if goal is ⊥)
|
CP
|
universal
∀x θx
|
UI
|
UG
|
existential
∃x θx
|
PCh
|
NcP
|
In addition, if the conditions for applying a rule are met except for differences between co-aliases, then the rule can be applied and is notated by adding "="; QED= and Nc= are examples of this.
|
|
Rules for closing gaps
|
when to close
|
rule
|
co-aliases
|
resources
|
goal
|
|
|
φ
|
φ
|
QED
|
|
φ and ¬ φ
|
⊥
|
Nc
|
|
|
⊤
|
ENV
|
|
⊥
|
|
EFQ
|
τ—υ
|
|
τ = υ
|
EC
|
τ—υ
|
¬ τ = υ
|
⊥
|
DC
|
τ1—υ1, …, τn—υn
|
Pτ1…τn
|
Pυ1…υn
|
QED=
|
τ1—υ1, …, τn—υn
|
Pτ1…τn
¬ Pυ1…υn
|
⊥
|
Nc=
|
Detachment rules (optional)
|
required resources
|
rule
|
main
|
auxiliary
|
|
φ → ψ
|
φ
|
MPP
|
¬± ψ
|
MTT
|
φ ∨ ψ
|
¬± φ or ¬± ψ
|
MTP
|
¬ (φ ∧ ψ)
|
φ or ψ
|
MPT
|
|
Additional rules (not guaranteed to be progressive)
Attachment rules
|
added resource
|
rule
|
φ ∧ ψ
|
Adj
|
φ → ψ
|
Wk
|
φ ∨ ψ
|
Wk
|
¬ (φ ∧ ψ)
|
Wk
|
τ = υ
|
CE
|
θυ1…υn
|
Cng
|
∃x θx
|
EG
|
|
|
Rule for lemmas
|
prerequisite
|
rule
|
the goal is ⊥
|
LFR
|
|
Diagrams
Rules from chapter 2
Extraction (Ext)
| │⋯ | |
| │φ ∧ ψ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││⋯ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │φ ∧ ψ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
n Ext | ││φ | |
n Ext | ││ψ | |
| ││ | |
| ││⋯ | |
| │⋯ | |
|
Conjunction (Cnj)
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ ∧ ψ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││φ | n |
| ││ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││ψ | n |
| │├─ | |
n Cnj | ││φ ∧ ψ | |
| │⋯ | |
|
Quod Erat Demonstrandum (QED)
| │⋯ | |
| │φ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │φ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n QED | ││φ | |
| │⋯ | |
|
Ex Nihilo Verum (ENV)
|
→
|
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n ENV | ││⊤ | |
| │⋯ | |
|
Ex Falso Quodlibet (EFQ)
| │⋯ | |
| │⊥ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │⊥ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n EFQ | ││φ | |
| │⋯ | |
|
Adjunction (Adj)
| │⋯ | |
| │φ [available] | |
| │⋯ | |
| │ψ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │φ | (n) |
| │⋯ | |
| │ψ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Adj | ││φ ∧ ψ | X |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
Lemma for Reductio (LFR)
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││φ | n |
| ││ | |
| │││φ | |
| ││├─ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││⊥ | n |
| │├─ | |
n LFR | ││⊥ | |
| │⋯ | |
|
Rules from chapter 3
Indirect Proof (IP)
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ [atomic] | |
| │⋯ | |
|
→
|
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││¬ φ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││⊥ | n |
| │├─ | |
n IP | ││φ | |
| │⋯ | |
|
Completing the Reductio (CR)
| │⋯ | |
| │¬ φ [φ is not atomic] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │¬ φ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││φ | n |
| │├─ | |
n CR | ││⊥ | |
| │⋯ | |
|
Reductio ad Absurdum (RAA)
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││¬ φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││φ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││⊥ | n |
| │├─ | |
n RAA | ││¬ φ | |
| │⋯ | |
|
Non-contradiction (Nc)
| │⋯ | |
| │¬ φ [available] | |
| │⋯ | |
| │φ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │¬ φ | (n) |
| │⋯ | |
| │φ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n Nc | ││⊥ | |
| │⋯ | |
|
Rules from chapter 4
Proof by Cases (PC)
| │⋯ | |
| │φ ∨ ψ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││χ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │φ ∨ ψ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││φ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││χ | n |
| ││ | |
| │││ψ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││χ | n |
| │├─ | |
n PC | ││χ | |
| │⋯ | |
|
Proof of Exhaustion (PE)
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ ∨ ψ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││¬± φ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││ψ | n |
| │├─ | |
n PE | ││φ ∨ ψ | |
| │⋯ | |
|
OR
|
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││¬± ψ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││φ | n |
| │├─ | |
n PE | ││φ ∨ ψ | |
| │⋯ | |
|
Modus Tollendo Ponens (MTP)
| │¬± φ [available] | |
| │⋯ | |
| │φ ∨ ψ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││χ | |
| │⋯ | |
|
→ |
| │¬± φ | (n) |
| │⋯ | |
| │φ ∨ ψ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
n MTP | ││ψ | |
| ││ | |
| │├─ | |
| ││χ | |
| │⋯ | |
|
| │¬± ψ [available] | |
| │⋯ | |
| │φ ∨ ψ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││χ | |
| │⋯ | |
|
→ |
| │¬± ψ | (n) |
| │⋯ | |
| │φ ∨ ψ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
n MTP | ││φ | |
| ││ | |
| │├─ | |
| ││χ | |
| │⋯ | |
|
Modus Ponendo Tollens (MPT)
| │φ [available] | |
| │⋯ | |
| │¬ (φ ∧ ψ) | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │φ | (n) |
| │⋯ | |
| │¬ (φ ∧ ψ) | n |
| │⋯ | |
| │ | |
| ││⋯ | |
n MPT | ││¬± ψ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
| │ψ [available] | |
| │⋯ | |
| │¬ (φ ∧ ψ) | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │ψ | (n) |
| │⋯ | |
| │¬ (φ ∧ ψ) | n |
| │⋯ | |
| │ | |
| ││⋯ | |
n MPT | ││¬± φ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
Weakening (Wk)
| │⋯ | |
| │φ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │⋯ | |
| │φ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Wk | ││φ ∨ ψ | X |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
| │⋯ | |
| │ψ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │⋯ | |
| │ψ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Wk | ││φ ∨ ψ | X |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
Weakening (Wk)
| │⋯ | |
| │¬± φ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │¬± φ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Wk | ││¬ (φ ∧ ψ) | X |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
| │⋯ | |
| │¬± ψ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │¬± ψ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Wk | ││¬ (φ ∧ ψ) | X |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
Rules from chapter 5
Rejecting a Conditional (RC)
| │⋯ | |
| │φ → ψ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │φ → ψ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││φ | n |
| ││ | |
| │││ψ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││⊥ | n |
| │├─ | |
n RC | ││⊥ | |
| │⋯ | |
|
Conditional Proof (CP)
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ → ψ | |
| │⋯ | |
|
→ |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │││φ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││ψ | n |
| │├─ | |
n CP | ││φ → ψ | |
| │⋯ | |
|
Modus Ponendo Ponens (MPP)
| │φ [available] | |
| │⋯ | |
| │φ → ψ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │φ | (n) |
| │⋯ | |
| │φ → ψ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ψ | |
| ││ | |
| │├─ | |
n MPP | ││θ | |
| │⋯ | |
|
Modus Tollendo Tollens (MTT)
| │¬± ψ [available] | |
| │⋯ | |
| │φ → ψ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │¬± ψ | (n) |
| │⋯ | |
| │φ → ψ | n |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││¬± φ | |
| ││ | |
| │├─ | |
n MTT | ││θ | |
| │⋯ | |
|
Weakening (Wk)
| │ψ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │ψ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Wk | ││φ → ψ | X |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
Weakening (Wk)
| │¬± φ [available] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
→ |
| │¬± φ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Wk | ││φ → ψ | X |
| ││ | |
| │├─ | |
| ││θ | |
| │⋯ | |
|
Rules from chapter 6
Equated Co-aliases (EC)
| │⋯ | |
| │[τ and υ are co-aliases] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │├─ | |
| ││τ = υ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │[τ and υ are co-aliases] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n EC | ││τ = υ | |
| │⋯ | |
|
Distinguished Co-aliases (DC)
| │⋯ | |
| │[τ and υ are co-aliases] | |
| │⋯ | |
| │¬ τ = υ | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │[τ and υ are co-aliases] | |
| │⋯ | |
| │¬ τ = υ | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n DC | ││⊥ | |
| │⋯ | |
|
QED given equations (QED=)
| │⋯ | |
| │[τ1…τn and υ1…υn | |
| │ are co-alias series] | |
| │⋯ | |
| │Pτ1…τn | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │├─ | |
| ││Pυ1…υn | |
| │⋯ | |
|
→
|
| │⋯ | |
| │[τ1…τn and υ1…υn | |
| │ are co-alias series] | |
| │⋯ | |
| │Pτ1…τn | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n QED= | ││Pυ1…υn | |
| │⋯ | |
|
Note: Two series of terms are co-alias series when their corresponding members are co-aliases.
Non-contradiction given equations (Nc=)
| │⋯ | |
| │[τ1…τn and υ1…υn | |
| │ are co-alias series] | |
| │⋯ | |
| │¬ Pτ1…τn | |
| │⋯ | |
| │Pυ1…υn | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │[τ1…τn and υ1…υn | |
| │ are co-alias series] | |
| │⋯ | |
| │¬ Pτ1…τn | (n) |
| │⋯ | |
| │Pυ1…υn | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││● | |
| │├─ | |
n Nc= | ││⊥ | |
| │⋯ | |
|
Note: Two series of terms are co-alias series when their corresponding members are co-aliases.
Co-alias Equation (CE)
| │⋯ | |
| │[τ and υ are co-aliases] | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │[τ and υ are co-aliases] | |
| │⋯ | |
| │ | |
| ││⋯ | |
n CE | ││τ = υ | X |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
Congruence (Cng)
| │⋯ | |
| │[τ1…τn and υ1…υn | |
| │ are co-alias series] | |
| │⋯ | |
| │θτ1…τn | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │[τ1…τn and υ1…υn | |
| │ are co-alias series] | |
| │⋯ | |
| │θτ1…τn | (n) |
| │⋯ | |
| │ | |
| ││⋯ | |
n Cng | ││θυ1…υn | X |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
Note: θ can be an abstract, so θτ1…τn and θυ1…υn are any formulas that differ only in the occurrence of terms and in which the corresponding terms are co-aliases.
Rules from chapter 7
Universal Instantiation (UI)
| │⋯ | |
| │∀x …x… | |
| │⋯ | |
| │ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │∀x …x… | τ:n |
| │⋯ | |
| │ | |
| ││⋯ | |
n UI | ││…τ… | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
Universal Generalization (UG)
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││∀x …x… | |
| │⋯ | |
|
→
|
| │⋯ | |
| ││⋯ | |
| ││ⓐ | |
| │││ | |
| ││├─ | |
| │││…a… | n |
| │├─ | |
n UG | ││∀x …x… | |
| │⋯ | |
|
Rules from chapter 8
Proof by Choice (PCh)
| │⋯ | |
| │∃x θx | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │∃x θx | n |
| │⋯ | |
| ││⋯ | |
| ││ⓐ | |
| │││θa | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││φ | n |
| │├─ | |
| ││φ | |
n PCh | │⋯ | |
|
Non-constructive Proof (NcP)
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││∃x θx | |
| │⋯ | |
|
→
|
| │⋯ | |
| ││⋯ | |
| │││∀x ¬± θx | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││⊥ | n |
| │├─ | |
| ││∃x θx | |
n NcP | │⋯ | |
|
Existential Generalization (EG)
| │⋯ | |
| │θτ | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
→
|
| │⋯ | |
| │θτ | n |
| │⋯ | |
| ││⋯ | |
n EG | ││∃x θx | X |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|