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
|
restricted universal
(∀x: ρx) θx
|
MCR
(if goal is ⊥)
|
RUG
|
existential
∃x θx
|
PCh
|
NcP
|
restricted existential
(∃x: ρx) θx
|
PRCh
|
RNcP
|
|
An alternative approach for restricted quantifiers, both universal and existential is to use rules for transforming those forms to and from forms using unrestricted quantifiers. These rules are RUP and RUC for the restricted universal and REP and REC for the restricted existential.
|
|
|
|
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
|
|
(∀x: ρx) θx
|
ρτ
|
SB
|
|
θτ
|
SC
|
|
In addition, if the conditions for meeting 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.
Additional rules (not guaranteed to be progressive)
|
Attachment rules
|
|
added resource
|
rule
|
|
φ ∧ ψ
|
Adj
|
|
φ → ψ
|
Wk
|
|
φ ∨ ψ
|
Wk
|
|
¬ (φ ∧ ψ)
|
Wk
|
|
τ = υ
|
CE
|
|
θυ1...υn
|
Cng
|
|
∃x θx
|
EG
|
|
(∃x: ρx) θx
|
REG
|
|
|
|
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=)
| │... | |
| │[<τ> and <υ> are co-alias series] | |
| │... | |
| │P<τ> | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| │├─ | |
| ││P<υ> | |
| │... | |
|
|
| │... | |
| │[<τ> and <υ> are co-alias series] | |
| │... | |
| │P<τ> | (n) |
| │... | |
| │ | |
| ││... | |
| ││● | |
| │├─ | |
| n QED= | ││P<υ> | |
| │... | |
|
(Notation: <τ> is a series of terms τ1, ..., τn. Two such series are co-alias series when they have the same length and their corresponding members are co-aliases. P<τ> is the predication Pτ1...τn.)
Non-contradiction given equations (Nc=)
| │... | |
| │[<τ> and <υ> are co-alias series] | |
| │... | |
| │¬ P<τ> | |
| │... | |
| │P<υ> | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │... | |
|
|
| │... | |
| │[<τ> and <υ> are co-alias series] | |
| │... | |
| │¬ P<τ> | (n) |
| │... | |
| │P<υ> | (n) |
| │... | |
| │ | |
| ││... | |
| ││● | |
| │├─ | |
| n Nc= | ││⊥ | |
| │... | |
|
(Notation: <τ> is a series of terms τ1, ..., τn. Two such series are co-alias series when they have the same length and their corresponding members are co-aliases. P<τ> is the predication Pτ1...τn.)
Co-alias Equation (CE)
| │... | |
| │[τ and υ are co-aliases] | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
|
| │... | |
| │[τ and υ are co-aliases] | |
| │... | |
| │ | |
| ││... | |
| n CE | ││τ = υ | X |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
Congruence (Cng)
| │... | |
| │[<τ> and <υ> are co-alias series] | |
| │... | |
| │θ<τ> | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
|
| │... | |
| │[<τ> and <υ> are co-alias series] | |
| │... | |
| │θ<τ> | (n) |
| │... | |
| │ | |
| ││... | |
| n Cng | ││θ<υ> | X |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
(Notation: <τ> is a series of terms τ1, ..., τn. Two such series are co-alias series when they have the same length and their corresponding members are co-aliases. θ<τ> and θ<υ> are sentences which differ only by corresponding members of the series <τ> and <υ>.)
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... | |
| │... | |
|
Making a Counterexample for Reductio (MCR)
| │⋯ | |
| │(∀x: ρx) θx | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││⊥ | |
| │⋯ | |
|
|
| │⋯ | |
| │(∀x: ρx) θx | τ:n |
| │⋯ | |
| ││⋯ | |
| │││ | |
| ││├─ | |
| │││ρτ | n |
| ││ | |
| │││θτ | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││⊥ | n |
| │├─ | |
| n MCR | ││⊥ | |
| │⋯ | |
|
Restricted Universal Generalization (RUG)
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││(∀x: ρx) θx | |
| │⋯ | |
|
|
| │⋯ | |
| ││⋯ | |
| ││ⓐ | |
| │││ρa | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││θa | n |
| │├─ | |
| n RUG | ││(∀x: ρx) θx | |
| │⋯ | |
|
Singular Barbara (SB)
| │⋯ | |
| │(∀x: ρx) θx | |
| │⋯ | |
| │ρτ | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
|
| │⋯ | |
| │(∀x: ρx) θx | τ:n |
| │⋯ | |
| │ρτ | (n) |
| │⋯ | |
| ││⋯ | |
| n SB | ││θτ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
Singular Camestres (SC)
| │⋯ | |
| │(∀x: ρx) θx | |
| │⋯ | |
| │θτ | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││⋯ | |
| │⋯ | |
|
|
| │⋯ | |
| │(∀x: ρx) θx | τ:n |
| │⋯ | |
| │θτ | (n) |
| │⋯ | |
| ││⋯ | |
| n SC | ││ρτ | |
| ││ | |
| ││⋯ | |
| │⋯ | |
|
Restricted Universal Premise (RUP)
| │⋯ | |
| │(∀x: ρx) θx | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
|
| │⋯ | |
| │(∀x: ρx) θx | n |
| │⋯ | |
| ││⋯ | |
| n RUP | ││∀x (ρx → θx) | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
Restricted Universal Conclusion (RUC)
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││(∀x: ρx) θx | |
| │⋯ | |
|
|
| │⋯ | |
| ││⋯ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││∀x (ρx → θx) | n |
| │├─ | |
| n RUC | ││(∀x: ρ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 |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
Proof by Restricted Choice (PRCh)
| │⋯ | |
| │(∃x: ρx) θx | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
|
| │⋯ | |
| │(∃x: ρx) θx | n |
| │⋯ | |
| ││⋯ | |
| ││ⓐ | |
| │││ρa | |
| │││θa | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││φ | n |
| │├─ | |
| ││φ | |
| n PRCh | │... | |
|
Restricted Non-constructive Proof (RNcP)
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││(∃x: ρx) θx | |
| │... | |
|
|
| │⋯ | |
| ││⋯ | |
| │││(∀x: ρx) θx | |
| ││├─ | |
| │││ | |
| ││├─ | |
| │││⊥ | n |
| │├─ | |
| n RNcP | ││(∃x: ρx) θx | |
| │... | |
|
Restricted Existential Generalization (REG)
| │⋯ | |
| │ρτ | |
| │⋯ | |
| │θτ | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
|
| │⋯ | |
| │ρτ | |
| │⋯ | |
| │θτ | |
| │⋯ | |
| ││⋯ | |
| n REG | ││(∃x: ρx) θx | X |
| ││ | |
| │├─ | |
| ││φ | |
| │... | |
|
Restricted Existential Premise (REP)
| │⋯ | |
| │(∃x: ρx) θx | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
|
| │⋯ | |
| │(∃x: ρx) θx | n |
| │⋯ | |
| ││⋯ | |
| n REP | ││∃x (ρx ∧ θx) | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
Restricted Existential Conclusion (REC)
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| ││ | |
| ││ | |
| │├─ | |
| ││(∃x: ρx) θx | |
| │⋯ | |
|
|
| │⋯ | |
| ││⋯ | |
| │││ | |
| │││ | |
| ││├─ | |
| │││∃x (ρx ∧ θx) | n |
| │├─ | |
| n REC | ││(∃x: ρx) θx | |
| │⋯ | |
|
|
|
| │⋯ | |
| │∃x (ρx ∧ θx) | |
| │⋯ | |
| ││⋯ | |
| ││ | |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|
|
| │⋯ | |
| │∃x (ρx ∧ θx) | n |
| │⋯ | |
| ││⋯ | |
| n REC | ││(∃x: ρx) θx | X |
| ││ | |
| │├─ | |
| ││φ | |
| │⋯ | |
|