Negation Elimination

How to apply ¬E Forwards

1. Select ¬E from the Elim Rules menu in the ToolBox.
   Show me
2. Select the falsum on the last line of the subderivation opened by the assumption of the negation of the formula to be derived in the Fitch.
   Show me
3. Click the Apply Rule button in the ToolBox.
   Show me

• Watch a demonstration of ¬E applied forwards

How to apply ¬E Backwards

1. Select ¬E from the Elim Rules menu in the ToolBox.
   Show me
2. Select the formula you want to derive in the Goal Tree.
   Show me
3. Click the Apply Rule button in the ToolBox.
   Show me

• Watch a demonstration of ¬E applied backwards

Troubleshooting

If you're having trouble applying ¬E, click on the statement below that best describes the problem you're having.