Negation Introduction vs Indirect Proof: Choose the Assumption from the Goal

Choose the temporary assumption from the exact goal

To prove ¬A by negation introduction, assume A and derive a contradiction. To prove A by the classical indirect-proof rule, assume ¬A and derive a contradiction. The two rules use different target shapes and export different sentences.

In the forall x: Calgary TFL package, ¬I discharges an A-to-⊥ subproof to conclude ¬A. IP discharges a ¬A-to-⊥ subproof to conclude A. The contradiction sign ⊥ records incompatible results within the proof; it is not an ordinary extra premise that you may insert without justification.

Formal background: [2] [3].

Our two original proofs contrast these patterns. They also show why applying ¬I to an assumption ¬P yields ¬¬P, rather than silently yielding P. Classical double-negation elimination can bridge that difference when your system permits it.

Compare the opening assumption and exported sentence

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

Rule labels vary between proof systems. The table states the package used here, including its explicit IP rule. If your course uses reductio, RAA or a different presentation, consult the precise rule statement instead of treating the abbreviation as a universal definition.

Prove ¬P by assuming P

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

Under the temporary P assumption, line 4 follows by conditional elimination. Its main conjunction lets line 5 extract Q. Premise ¬Q remains available, so line 6 records a contradiction using Q and ¬Q. The whole range 3–6 then supports ¬P by ¬I.

The conclusion retains the two original premises as dependencies. It does not assert that ¬P was derived without any premises. The P assumption has been discharged; the premises have not.

Notice that R is not needed after extracting Q. Its presence in the conditional’s consequent does not invalidate the proof. What matters is that the whole antecedent P is supplied, the conjunction is actually derived, and the clash uses an accessible Q with the given ¬Q.

Prove P by assuming ¬P in the classical package

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

Download both complete proofs and their rule comparison

The assumed ¬P triggers the conditional on line 1, giving Q. That contradicts premise ¬Q. IP discharges the ¬P assumption and concludes P at the outer level. The rule is explicitly classical here.

If you apply ¬I to the same range 3–5 instead, treat its opening ¬P as A. The output is ¬A=¬¬P. To reach P through that route, add a licensed double-negation-elimination step. Writing P immediately with a ¬I label would misstate the rule even if the intended argument is classically valid.

Formal background: [1].

The premises differ between the two worked proofs: the first has P→(Q∧R), while the second has ¬P→Q. This comparison illustrates two rule patterns, not an unexplained inference that the same premises establish both P and ¬P.

A contradiction must be derived at an accessible level

In the displayed package, ¬E takes an accessible A and ¬A to obtain ⊥. Deriving unrelated P and ¬Q does not satisfy that rule. The formulas must be an actual contradictory pair, with the same structured A under the negation.

Likewise, a Q inside an already closed inner block cannot be combined with an outer ¬Q through an ordinary line citation. Export the appropriate result using a licensed discharge rule first. A contradiction found under a special temporary assumption must retain that scope until the rule removes it.

A subproof for ¬I or IP must end at ⊥ at that subproof’s own level. If the contradiction still sits inside a deeper assumption block, close that work correctly before claiming the outer range is complete. The same endpoint-level audit used for conditional proof applies here.

If you already have ⊥ at the current level, classical explosion permits deriving a sentence there. It does not by itself tell you which assumptions have been discharged. Use the range-based rule separately when your target requires a discharged conditional or negation.

Formal background: [2].

Keep the classical step separate from the general idea of inconsistency

Classically, a valuation satisfying ¬P→Q and ¬Q cannot have P false. P=F would make ¬P true and require Q true, while ¬Q requires Q false. Therefore P must be true whenever those premises are true. This semantic explanation corroborates the second proof’s result.

It does not license IP in every proof system. Intuitionistic logic does not generally identify ¬¬A with A or permit the unrestricted classical IP pattern. Other logics may also handle contradiction differently. Use this guide only with the stated package, or check your course’s rule set before transferring the derivation.

For your own proof, write the desired sentence before opening an assumption. Mark whether you want A, ¬A or ¬¬A. Then check the exported formula after discharge, rather than relying on the informal phrase “proof by contradiction” to conceal which rule was applied.

Try six negation and IP decisions

Apply the rule as stated, including its exact output.