Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent


chronological Thread 
  • From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
  • To: David Wahlstedt <david.wahlstedt AT gmail.com>
  • Cc: Noam Zeilberger <noam.zeilberger AT gmail.com>, Chung Kil Hur <Chung-Kil.Hur AT pps.jussieu.fr>, coq-club AT inria.fr, Agda mailing list <agda AT lists.chalmers.se>
  • Subject: [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent
  • Date: Fri, 8 Jan 2010 10:37:46 +0000

Red face... :-)

Thorsten

On 8 Jan 2010, at 10:18, David Wahlstedt 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 ?

Best regards,

David Wahlstedt

On Thu, Jan 7, 2010 at 5:24 PM, Noam Zeilberger <noam.zeilberger AT gmail.com> wrote:
On Thu, Jan 7, 2010 at 4:15 PM, Thorsten Altenkirch <txa AT cs.nott.ac.uk> wrote:
>> ...I'm not sure about this expansion, and the analogy.  I think the
>> question is whether we view the declaration of type constructors in
>> the same way that we view the declaration of term constructors (i.e.,
>> as stipulating a new way of constructing things, in this case
>> inhabitants of Set).  If we do, then type constructors are by
>> definition injective.
>
> I don't see the analogy. A term constructor is injective because an inductive type is freely generated from constructors. Indeed, we can show that the structure map of an initial algebra is an isomorphism and hence injective. However the universe of sets is not freely constructed from type constructors but they are really definitions.

But freeness ("inductive type = no confusion + no junk") is only a
sufficient condition, right?  Injectivity = no confusion.

> We should justify principles like this (i.e. all type constructors are injective) by a semantic explanation or by a translation into a well understood core language e.g. (extensional) Marttin-Loef Type Theory with W-types and universes. I don't know any such explanation which would justify this principle. Moreover, Chung's example shows that this is not possible (without giving up something else) since pure type theory is consistent with EM.

Agreed that there should be a convincing explanation, but again, I do
think there is a strong intuition behind the principle (what Dan Doel
and I were getting at), and the fact that it plays an important role
in typechecking suggests that we shouldn't jump to conclusions.  I am
not sure that Agda should be conservative over classical mathematics:
it seems there is a fundamental tension between exploiting the full
power of a constructive type theory and upholding the fictions of
classical mathematics.  Chung-Kil's paradox shows that you can't
reason classically in Agda just by adding the law of excluded middle
-- okay, so don't do it that way.

Could you explain what you meant by: "Also while we may accept that
extensions of Type Theory may be anticlassical, we should expect that
core Type Theory is consistent with EM."?

Noam
_______________________________________________
Agda mailing list
Agda AT lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda





Archive powered by MhonArc 2.6.16.

Top of Page