The Logic Resource Center

Public Alpha

Systems

Public Alpha

Negation Introduction

In systems with the falsum this rule allows inferring the negation of an assumption when the falsum can be derived from it. In systems without the falsum it expresses the classical Reductio Ad Absurdum

Constants: ¬
Systems: LRC_F OLI The Logic Book LRC_P LRC_O

Start a Problem →

Negation Introduction

i.

ϕ

A

⋮

ii

ii.

⊥

Goal

⋮

iii.

¬ϕ

¬I: i, ii

Forward

Cite a formula and the falsum
Enter the negation of that formula
Hit Return

Preview shown for the Typed Forward Strict derivation type in the LRC_F system