Comment by thaumasiotes
19 hours ago
> 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.