Negation Elimination
In systems with the falsum this rule allows inferring the a claim when the falsum can be derived from the assumption of its negation. In systems without the falsum it expresses the classical Reductio Ad Absurdum coupled, as is the falsum version, with Double Negation Elimination.
- Constants
- ¬
Negation Elimination
ii
i.
A
⋮
ii
ii.
Goal
⋮
iii.
¬E: i, ii
Forward
- Enter a formula
- Cite its negaton and the falsum
- Hit Return
Preview shown for the Typed Forward Strict derivation type in the LRC_O system