Remix.run Logo
zozbot234 2 hours ago

Constructivists don't call a proof of ¬p a "proof by contradiction", they just call it a proof of ¬p. To them, a "proof by contradiction" of some p that isn't in the negative fragment is just nonsense, because constructive logic doesn't have the kind of duality that even makes it necessary to talk about contradiction as a kind of proof to begin with. They'd see the classical use of "proof by contradiction" as a clunky way of saying "I've actually only proven a negative statement, and now I can use De Morgan duality to pretend that I proved a positive."