[Agda] Agda with excluded middle is inconsistent

[Martin Escardo]

Nils Anders Danielsson wrote:
> On 2010-01-08 12:05, Noam Zeilberger wrote:
>> In intuitionistic second-order logic you can prove ∀ P.~~(P \/ ~P),
>> but not ~~(∀ P. P \/ ~P).
> 
> If you allow bar recursion you can prove some double-negation shift
> lemma. I suspect that this means that a sufficiently strong variant of
> bar recursion is not compatible with injective type constructors.

The double negation shift (DNS) obtained by bar recursion is

       (∀ n : N. ~~ A n) -> ~~  ∀ n: A n.

Only quantifications over N (natural numbers) can be shifted. Bar 
recursion (in its many manifestations) crucially exploits the structure 
of N (and in some/most forms of bar recursion, also continuity is 
crucially invoked). Essentially, bar recursion is recursion on 
well-founded trees, where functions (n : N)-> A n are paths in such 
trees. The catch is that such trees are not given as W-types (data 
definitions in agda), but as continuous functions from sequences to a 
discrete type. In summary, bar recursion cannot possibly handle DNS for 
quantifications over propositions (as above). I would guess that the 
instance of DNS you want (certainly not realizable by anything that 
could be sensibly called bar recursion), is "very classical" (question: 
is it classical, in the sense that it implies excluded middle? I haven't 
thought about that.)

Martin