4.3.s. Summary
While a disjunction does not settle the truth values of its disjuncts, it says enough about them that adding the information that one is false will tell us that the other is true. This principle is known traditionally as modus tollendo ponens. Since each disjunct entails the disjunction, we know that, if one disjunct is false, then the disjunction and the other disjunct provide the same information. This idea is implemented in a further rule for exploiting disjunctions, also known as Modus Tollendo Ponens (MTP). The not-both form ¬ (φ ∧ ψ) is analogous to disjunction and analogous principles apply. Specifically, a principle modus ponendo tollens tells us that ¬ (φ ∧ ψ) together with the assertion of one of φ and ψ entails the denial of the other. And, since the denial of either φ or ψ entails ¬ (φ ∧ ψ), we can have a rule Modus Ponendo Tollens (MPT) for exploiting not-both forms. The rules MTP and MPT are examples of detachment rules. The resource exploited in each is its main resource and the additional resource that must be available is the auxiliary resource.
We will refer to as weakening the principle that disjunctions and not-both forms are entailed by assertions of components (in the case of disjunctions) or their denials (in the case of the not-both form). This principle provides the basis for two further attachment rules, both called Weakening (Wk), that license the addition of inactive resources. Since the second resource we must have in order to apply a detachment rule need only be available, attachment rules can be used to prepare for the use of detachment rules as well to prepare for the use of rules that close gaps.
We now have examples of all the types of rules we will employ:
Rules for developing gaps
|
|
for resources
|
for goals
|
atomic
sentence
|
|
IP
|
negation
¬ φ
|
CR
(if φ is not atomic
and the goal is ⊥)
|
RAA
|
conjunction
φ ∧ ψ
|
Ext
|
Cnj
|
disjunction
φ ∨ ψ
|
PC
|
PE
|
|
|
Rules for closing gaps
|
when to close
|
rule
|
the goal is also
a resource
|
QED
|
sentences φ and ¬ φ are
resources & the goal is ⊥
|
Nc
|
⊤ is the goal
|
ENV
|
⊥ is a resource
|
EFQ
|
|
Basic system
|
Detachment rules (optional)
|
main resource
|
auxiliary resource
|
rule
|
φ ∨ ψ
|
φ or ψ
|
MTP
|
¬ (φ ∧ ψ)
|
φ or ψ
|
MPT
|
|
|
Attachment rules
|
added resource
|
rule
|
φ ∧ ψ
|
Adj
|
φ ∨ ψ
|
Wk
|
¬ (φ ∧ ψ)
|
Wk
|
Rule for lemmas
|
prerequisite
|
rule
|
the goal is ⊥
|
LFR
|
|
Added rules
(optional)
|