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 (i.e., ones 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] → |
|
||||||||||||||||||||||||||||||||||||||||||||||||||
|
[available] → |
|
Fig. 4.3.2-1. Developing a derivation at stage n by adding an inactive disjunction that weakens one of the available resources.
|
[available] → |
|
||||||||||||||||||||||||||||||||||||||||||||||||||
|
[available] → |
|
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, since the detachment rules MTP and MPT can use inactive resources, attachment rules can provide material for them, too. For example, below are two approaches to the same argument. The argument is designed as an illustration but can be given the English interpretation that appears between them:
| │(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 |
Assume we know in general that either Ann and Bill were both at the party or Carol and Dave were both there. And assume 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) | 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 derivations begin by exploiting the third premise, but they exploit the other two premises in a different order. The first derivation produces a direct proof of the conclusion C while the second reaches C by an indirect proof showing that ¬ C is incompatible with the premises.