The Logic Resource Center

Public Alpha

Systems

Public Alpha

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: ~
Systems: LRC_F OLI The Logic Book LRC_P LRC_O

Start a Problem →

Negation Elimination

i.

~ϕ

A

ii.

ψ

Goal

iii.

~ψ

Goal

iv.

ϕ

~E: i, ii, iii

Backward

Select a goal formula
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