[TYPES] What's a program? (Seriously)

[Guillaume Munch-Maccagnoni]

Le 22/05/2021 à 18:43, streicher at mathematik.tu-darmstadt.de 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