Rule RAA Glossary
Definition
| X, A ⊢ B | Y, A ⊢ NOTB | RAA |
| X, Y ⊢ NOTA | ||
The two input (source) lines hold a formula B and its negation NOTB. The output of the rule is a line holding the negation NOTA of a formula, which may be present as an assumption on one or other (or both or neither) of the input lines. It may be discharged by this rule. The assumptions on which the conclusion depends are those of the two premises put together, minus the discharged assumption if any.
Comments
The negation rules NOTI and NOTE encode the principle that if a set of assumptions leads to a contradiction, at least one of those assumptions must be false. This thought is encapsulated in the one rule RAA which may replace NOTE followed by NOTI if desired. Cite the two input line numbers, noting the discharge, and "RAA". Note that the conclusion is always a negation.
In the linear notation for natural deduction proofs, discharged assumptions are referenced by means of their numbers in (square) brackets after the cited source line numbers. If no assumption is discharged, the brackets are left empty.
Example
SP {p IMP q, p IMP NOTq ⊢ NOTp} PL {1} {1} {p IMP q} {A} PL {2} {2} {p IMP NOTq} {A} PL {3} {3} {p} {A} PL { 1,3 } {4} { q } {1, 3 IMPE} PL { 2,3 } {5} { NOTq } {2, 3 IMPE} PL { 1,2 } {6} { NOTp } {4, 5 [3] RAA}} EP|
|
|
||||||
Hover the mouse over elements in the proof or in the rule template above, to see how the inference at line 6 matches the abstract form of the rule.