2 ms·
Although the standard proof of the incomputability of the halting problem assumes it is computable and then reaches a contradiction. And that's more or less the
by Scarblac 5y ago
Although the standard proof of the incomputability of the halting problem assumes it is computable and then reaches a contradiction. And that's more or less the central proof of everything to do with computability.
- siraben 5y agoThat'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.