Rule NOTI Glossary
Definition
| X, A ⊢ ⊥ | NOTI |
| X ⊢ NOTA |
The one input (source) line holds the absurd constant ⊥. The output of the rule is a line holding a negated formula NOTA. If A is one of the assumptions on which the premise ⊥ depends, it may be discharged by this rule. The assumptions on which the conclusion depends are those of the premise, 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. The NOTI part of the reasoning is that whatever leads to absurdity is false. Cite the one input line number and "NOTI", noting the discharge.
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 {NOTp ⊢ NOT(p AND q)} PL {1} {1} {NOTp} {A} PL {2} {2} {p AND q} {A} PL {1} {3} {p} {1 ANDE} PL { 1,2 } {4} { ⊥ } {1, 3 NOTE} PL { 1 } {5} { ¬(p AND q) } {4 [2] NOTI} EP|
|
|
Hover the mouse over elements in the proof or in the rule template above, to see how the inference at line 5 matches the abstract form of the rule.