[Agda] Re: Classical Mathematics for a Constructive World

Jan Burse janburse at fastmail.fm
Mon Nov 26 22:22:13 CET 2012

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).

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.


More information about the Agda mailing list