refutation by contradiction in nLab (original) (raw)

Refutation by contradiction

Refutation by contradiction

• Idea
• Related concepts
• References

Idea

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 P→⊥P\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)).

• proof by contradiction

References

• Andrej Bauer, Proof of negation and proof by contradiction 2010
• E. G. K. López-Escobar, Refutability and Elementary Number Theory , Indag. Math. 34 1972 pp.362-374.
• David Nelson, Constructible Falsity, The Journal of Symbolic Logic, Vol. 14, No. 1 (Mar., 1949), pp. 16-26. (jstor)

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