3 ms·
That's still constructive. This can be a confusion because there's actually two kinds of contradiction proofs: to show ¬ P, assume P then derive a contradic
by siraben 5y ago
That's still constructive. This can be a confusion because there's actually two kinds of contradiction proofs:
to show ¬ P, assume P then derive a contradiction (false, ⊥)
i.e., ¬ P := P -> ⊥. This is actually just fine and constructive, it's just how you prove a negation.
OTOH, there's another kind of contradiction proof:
to show P, assume ¬ P, then derive a contradiction (false, ⊥)
Written with function notation, this becomes P <-> (¬ P -> ⊥)
But if we unfold the definition of negation, we have that
P <-> ((P -> ⊥) -> ⊥)
The left to right direction holds classically and constructive, but the right to left direction uses double negation, which can is equivalent to the law of the excluded middle, AKA classical reasoning.
- momentoftop 5y agoSometimes, the strategy of proving ~P by showing how P entails absurdity is called "proof by negation". The phrase "proof by contradiction" is then reserved for the strategy of proving P by showing how ~P entails absurdity. On that usage, constructivists are happy with all proofs by negation, but not generally happy with proofs by contradiction.