nLab refutation by contradiction

Refutation by contradiction


Refutation by contradiction is the “basic” method of formal proof for proving a negation: if assuming PP leads to a contradiction, then we conclude ¬P\neg P. It is the introduction rule for the connective of negation in intuitionistic logic; if ¬P\neg P is defined as PP\to \bot (the function type from PP to false), then it follows from the introduction rule for implication.

Refutation by contradiction is also called proof of negation, but this can be confusing because there may be other “indirect” ways to prove a negation.

Rarely one finds logics that have a basic notion of “refutation of AA” that is distinct from (though generally closely related to) a “proof of ¬A\neg A(Nelson 1949). In that case, refutation by contradiction is more precisely a method of refuting AA by deriving a contradiction from an assumption of AA, which might be distinguished from other more “direct” ways of refuting AA (for example, a refutation of a universally quantified statement x.B(x)\forall x.B(x) that exhibits an explicit counterexample, i.e., a term tt together with a refutation of B(t)B(t)).


Last revised on May 4, 2017 at 10:22:53. See the history of this page for a list of all contributions to it.