Comment by zozbot234
1 day 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."
> 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.
> 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... 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.
You can actually make that a rigorous statement in linear logic, which reintroduces the duality that's lost in intuitionistic logic while still making it possible to assess whether some claim is constructive. But linear logic is significantly more complex than either classical or intuitionistic logic.