The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

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