A.4. Derivation rules

Basic system

Rules for developing gaps
logical form as a
resource 		as a
goal
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
│├─
n NcP ││∃x θx
│⋯

Existential Generalization (EG)

│⋯
│θτ
│⋯
│
││⋯
││
││
│├─
││φ
│⋯
→
│⋯
│θτ (n)
│⋯
│
││⋯
n EG ││∃x θx X
││
│├─
││φ
│⋯
Glen Helman 01 Oct 2012