[Agda] Re: Classical Mathematics for a Constructive World

[Martin Escardo]

What people call DNS in this context is

forall n : N. ¬¬(A n) -> ¬¬forall n : A. A n.

This is not provable intuitionistically.

A proof term of this type can be defined by disabling the termination 
checker. But termination (strong normalization_ is nevertheless 
guaranteed by Coquand and Spivak's results.

Spector was the first to define a recursion scheme in Godel's system T 
to give an interpretation of classical countable choice in the context 
of Godel's dialectica interpretation. His objective was to prove the 
consistency of analysis. Nowadays, especially in "proof mining", it is 
used to extract computational content from (some kinds of) classical 
proofs.

Martin

On 26/11/12 20:58, Jan Burse wrote:
> Martin Escardo schrieb:
>> But you can show that such a sequence not-not-exists, and more generally
>> that it K-exists. I.e. that classically it exists.
>
> Double negation shift (DNS) is already available in minimal
> logic, i.e. intuitionist logic without ex-falso quodlibet. A
> proof term can be extracted from:
>
>     ------ (id)  ------------ (id)
>     A |- A       A->f |- A->f
>     ------------------------- (MP)
>     A, A->f |- f
>     ---------------- (Right ->)
>     A |- ((A->f)->f)
>
> It can be used in connection with some double negation
> translation (DNT) to show the corrolar that an intuitionistic
> consequence is also a classical consequence.
>
> But the other way around, which is called the double
> negation elimination (DNE), is not intuitionistically
> valid in general.
>
> Therefore I wonder:
>
>  > If you postulate DNS (to interpret classical choice), anything
>  > else you postulate be better consistent with DNS.
>
> What do you mean by postulate DNS? It is already there
> in intuitionistic logic.
>
> Do you mean by postulate DNS the double negation translation
> (DNT)? Or is there some problem in having DNS derived in
> Agda? Some problem in using it in certain recursion schemes?
>
> Bye
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe