Negation Introduction

How to apply ¬I Forwards

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

• Watch a demonstration of ¬I applied forwards

How to apply ¬I Backwards

1. Select ¬I from the Intro Rules menu in the ToolBox.
   Show me
2. Select the negation 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 ¬I applied backwards

Troubleshooting

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