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)
Glen Helman 30 Sep 2004