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

[Andreas Abel]

If you say that if all your axioms are negative, consistency implies 
canonicity, I would find that plausible.  Your axiom "em" still looks 
ugly to me.

As a research project, I suggest to try and add a classical, 
impredicative, proof-irrelevant universe Prop to Agda.  Maybe that would 
allow you to do your stuff?

Cheers,
Andreas

On 25.05.11 11:57 AM, Nils Anders Danielsson wrote:
> 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.)
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/