[Agda] Postulating double-negated consistent axioms without breaking canonicity?

[Nils Anders Danielsson]

Hi,

It's annoying, but unavoidable, that there are total functions which
cannot be implemented in Agda (assuming consistency). Last week we
discussed one instance of this problem here at Chalmers. For some
properties A and B I proved the following:

   ((P : ℕ → Set) → A P → ¬ ¬ B P)  ⇔  (∀ P → DNS P)

Here DNS stands for double-negation shift:

   DNS : (ℕ → Set) → Set
   DNS P = (∀ i → ¬ ¬ P i) → ¬ ¬ (∀ i → P i)

It is known that ∀ P → DNS P cannot be proven in some type theories, but
also that other type theories support this principle, without
sacrificing canonicity or strong normalisation. One could add something
like bar recursion to Agda and strengthen the statement above to the
following:

   (P : ℕ → Set) → A P → ¬ ¬ B P

However, Ulf Norell conjectured that we could fix this problem in an
easier way. He remarked that all we are doing is proving that something
implies ⊥, and then it seems to be fine to assume consistent classical
axioms. In particular he conjectured that we can add the following as an
axiom, without any computational interpretation, /without breaking
canonicity/ (because ⊥ is empty in the empty context):

   em : ¬ ¬ ((P : Set) → P ⊎ ¬ P)

Do you know if this conjecture holds up to closer scrutiny? Do you see
any other problems with it? (Thierry Coquand pointed out that this axiom
is inconsistent in the presence of impredicativity.)

-- 
/NAD