[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).
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
More information about the Agda
mailing list