alt Hacker NewsConstructivists 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."
> Constructivists don't call a proof of ¬p a "proof by contradiction", they just call it a proof of ¬p.
I tend to agree with the opposition on this one. Concluding that p is false because its truth leads to a contradiction is fundamentally identical to concluding that p is true because its falsity leads to a contradiction... and in particular, it is reasonable to describe 'concluding that p is false because its truth leads to a contradiction' as a 'proof by contradiction'.
The reason that the first type is "constructive" while the second one isn't is due to a strange definition of falsity on the part of the constructivists.