Description: Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by
contradiction.
Proofs, such as this one, which assume a proposition, here , derive
a contradiction, and therefore conclude , are valid
intuitionistically (and can be called "proof of negation", for
example by
Section 1.2 of [Bauer] p. 482). By
contrast, proofs which assume
, derive a
contradiction, and conclude , such as
condandc 849, are only valid for decidable propositions.
(Contributed by
NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
8-Mar-2013.) |