[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

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