[Agda] Agda with excluded middle is inconsistent

[Thorsten Altenkirch]

On 8 Jan 2010, at 11:05, Noam Zeilberger wrote:

> On Fri, Jan 8, 2010 at 11:33 AM, Noam Zeilberger
> <noam.zeilberger at gmail.com> wrote:
>> On Fri, Jan 8, 2010 at 11:18 AM, David Wahlstedt
>> <david.wahlstedt at gmail.com> wrote:
>>> Hi,
>>> I have read through the two threads on this topic, and:
>>> Sorry if I mention something that is "too basic" / "naive", but, to clarify
>>> even more on Thorstens remark about the compatibility of MLTT with EM, it
>>> should be recalled that ~~(P \/ ~P) is a theorem even in very basic
>>> intuitionistic logic.
>>> So if we add something to our system such that ~(P \/ ~P) becomes a theorem,
>>> we really have got an inconsistent system, without having to assume anything
>>> non-constructive. Or have I missed something ?
>> 
>> Of course you're right.
> 
> On second thought, I am not sure about this.  To derive a
> contradiction from Chung-Kil's example you would need to commute a
> second-order quantifier.  He uses:
> 
> LEM = ∀ P. P \/ ~P
> 
> In intuitionistic second-order logic you can prove ∀ P.~~(P \/ ~P),
> but not ~~(∀ P. P \/ ~P).
> 
> Noam

You are right. One doesn't even need 2nd order logic, while we can prove

	~((P0 \/ ~P0) /\ (P1 \/ ~P1) /\ .. /\ (Pn \/ ~Pn))

I don't think one can prove for any A:Set, P : A -> Prop

	~( forall a:A . P a \/ ~ (P a) )

but this is certainly used in Chung's proof (e.g. in the construction of J).

Thorsten