3 ms·
For finite proofs, proof by contradiction can be interpreted as continuation passing and then results in an algorithm. On the other hand, this algorithm may be
by tel 10y ago
For finite proofs, proof by contradiction can be interpreted as continuation passing and then results in an algorithm. On the other hand, this algorithm may be no better than exhaustive search.
- rocqua 10y agoWhat do you mean by 'finite proofs'? In cases where the set of all possible examples is finite, I can see this trick working. Maybe a similar approach still works when all possible examples are enumerable or even recursively enumerable. None of these hold for the intermediate value theorem on the real number line though.
- tel 10y agoDefinitely, it's super weak but at the same time constructive. The issue is that it essentially ends up becoming a search algorithm where contradiction is backtracking. If the search algorithm doesn't stumble upon the solution (at least in principle) in finite time then it's a bit tough to consider it constructive.