[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Le 22/05/2021 à 18:43, [email protected] a écrit :
As long as one does not reason about programs extracted from classical proofs it is no problem if they are cluttered with such fancy constructs. But if one does it becomes a nightmare since one does not know how to do this. That is a problem already for continuations though there exist axiomatizations for them. Therefore, the 'unwinders' rather follow the path of negative translation followed by some functional interpretation. But as soon as you go beyond Pi^0_2 the negative translation of a meaningful statement becomes fairly obscure. In any case it is very different from the original statement understood constructively. A typical example is the socalled Specker phenomenon. When you classically prove the existence of a real number then often you can extract a computable Cauchy sequence for which there does not exist a computable modulus of convergence meaning that you can't extract sufficiently good approximations. Thus, all this extraction business works only for Pi^0_2 sentences. But for those ZFC is conservative over ZF for which ordinary control operators work! Thomas
To give some context to Thomas' message, I would like to share this accessible introduction to what proof unwinding (or proof mining) is about: <https://prooftheory.blog/2020/06/06/what-proof-mining-is-about-part-i/>. It is in 4 parts, hosted on the nice Proof Theory blog that appeared last year.
-- Guillaume Munch-Maccagnoni Researcher at Inria Bretagne Atlantique Team Gallinette, Nantes
