4.3.2. Attachment rules
The principles that lie behind the rules MTP and MPT were based in part on the fact that the weak compounds φ ∨ ψ and ¬ (φ ∧ ψ) are entailed by certain information about their components. We will refer to the principles asserting these entailments as weakening principles:
φ ⇒ φ ∨ ψ
ψ ⇒ φ ∨ ψ
φ ⇒ ¬ (φ ∧ ψ)
ψ ⇒ ¬ (φ ∧ ψ)
They provide the basis for further attachment rules (in addition to Adj). These rules allow us to enter the conclusions of the weakening principles as inactive resources when their premises are already available.
| │... | |
| │φ [available] | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
 |
| │... | |
| │φ | (n) |
| │... | |
| │ | |
| ││... | |
| n Wk | ││φ ∨ ψ | X |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
|
| │... | |
| │ψ [available] | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
|
| │... | |
| │ψ | (n) |
| │... | |
| │ | |
| ││... | |
| n Wk | ││φ ∨ ψ | X |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
Fig. 4.3.2-1. Developing a derivation at stage n by adding an inactive disjunction that weakens one of the available resources.
| │⋯ | |
| │φ [available] | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
|
| │⋯ | |
| │φ | (n) |
| │... | |
| │ | |
| ││... | |
| n Wk | ││¬ (φ ∧ ψ) | X |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
|
| │⋯ | |
| │ψ [available] | |
| │... | |
| │ | |
| ││... | |
| ││ | |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
|
| │⋯ | |
| │ψ | (n) |
| │... | |
| │ | |
| ││... | |
| n Wk | ││¬ (φ ∧ ψ) | X |
| ││ | |
| │├─ | |
| ││θ | |
| │... | |
|
Fig. 4.3.2-2. Developing a derivation at stage n by adding an inactive negated conjunction that weakens one of the available resources.
These rules can be used, as we have used Adj, to provide material for closing gaps. But the rules MTP and MPT now provide a further way of using inactive resources, and Wk can provide material for them, too (as can Adj). For example, below are two approaches to the same argument. The argument is designed as an illustration but can be given an English interpretation as follows:
Suppose we know in general that either Ann and Bill were both at the party or Carol and Dave were both there. And also that it is not the case that both Bill and Ed were there along with either Fred or Gail. Then, assuming we know in particular that Ed and Fred were both there, we can conclude that Carol was, too.
| │(A ∧ B) ∨ (C ∧ D) | 6 |
| │¬ ((B ∧ E) ∧ (F ∨ G)) | 3 |
| │E ∧ F | 1 |
| ├─ | |
| 1 Ext | │E | (4) |
| 1 Ext | │F | (2) |
| 2 Wk | │F ∨ G | X,(3) |
| 3 MPT | │¬ (B ∧ E) | 4 |
| 4 MPT | │¬ B | (5) |
| 5 Wk | │¬ (A ∧ B) | X,(6) |
| 6 MTP | │C ∧ D | 7 |
| 7 Ext | │C | (8) |
| 7 Ext | │D | |
| │● | |
| ├─ | |
| 8 QED | │C | |
|
|
| │(A ∧ B) ∨ (C ∧ D) | 4 |
| │¬ ((B ∧ E) ∧ (F ∨ G)) | 7 |
| │E ∧ F | 1 |
| ├─ | |
| 1 Ext | │E | (6) |
| 1 Ext | │F | (8) |
| │ | |
| ││¬ C | |
| │├─ | |
| 3 Wk | ││¬ (C ∧ D) | X,(4) |
| 4 MTP | ││A ∧ B | 5 |
| 5 Ext | ││A | |
| 5 Ext | ││B | (6) |
| 6 Adj | ││B ∧ E | X,(7) |
| 7 MPT | ││¬ (F ∨ G) | (9) |
| 8 Wk | ││F ∨ G | X,(9) |
| ││● | |
| │├─ | |
| 9 Nc | ││⊥ | |
| ├─ | 2 |
| 2 IP | │C | |
|
Both begin with the third premise, but they use the other two premises in a different order. The derivation on the left produces a direct proof of the conclusion C while the one of the right reaches C by an indirect proof showing that ¬ C is incompatible with the premises.