# [Agda] Re: Classical Mathematics for a Constructive World

Martin Escardo m.escardo at cs.bham.ac.uk
Mon Nov 26 22:07:28 CET 2012

```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
```