[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

Martin Escardo schrieb:
> What people call DNS in this context is
>
> forall n : N. ¬¬(A n) -> ¬¬forall n : A. A n.
>
> This is not provable intuitionistically.

Thanks for the clarification.

Looks like the barcan formula (BF) to me,
when  the K modality is used.

The inference rule is also call BF in
the following paper from 1986, which also
introduces the K modality (but just uses
the box for it).
http://www.mi.sanu.ac.rs/~kosta/%5BP%5D%5B15%5D.pdf

But I don't know how far he went,
since he writes (on page 89-90):

"We have not considered systems with BF till
now (save for S5, in which BF is provable)
because in at least one of our modal systems,
namely Hdn, this formula is undesirable"

Oki Doki.

Bye