Log in

No account? Create an account

Intuitionistic vs Classical proofs

A quote from an interview with Kohlenbach which makes me think things over:

A common view is that a (fully) constructive proof per se is superior (contains more information) than a prima facie classical argument. Experience from the unwinding of classical arguments, however, shows that usually only small parts of a proof contribute to the computational content of a proof while the bulk of the proof may well be proven ineffectively. Sometimes, using a more ineffective argument helps to push further parts of a proof into lemmas which are not needed to be analyzed at all. Replacing ineffective analytic or geometric steps in a proof by constructive induction arguments can result in bounds that are much less good than those extractable from the original classical proofs (see e.g. [7]). Often even ineffective parts in a proof which do matter for the computational content can be systematically transformed in such a way that computationally relevant information can be read off.

Indeed, sometimes it is not easy to see what the computational content of a constructive proof is, even when you spend a few months formalising it in a proof assistant yourself. The reason may well be that there is none.