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.

ψ

Goal

iii.

~ψ

Goal

iv.

~ϕ

~I: i, ii, iii

Backward

Select a goal negation
Enter the formula involved in the contradiction you intend to derive
Click "Apply"

Preview shown for the Point And Click derivation type in the The Logic Book system