The Coq mailing list

["Zhong Shao" <zhong.shao AT gmail.com>]

My students and I did some research about this type of axiom a few years ago (including asking experts in the community and checking out relevant literatures, I can forward a summary to you).  While there is still no proof saying that this is definitely inconsistent, the consensus is that it is a very dangerous thing to do and there is little hope building a model for it or showing its consistency. Since then, we have stayed away from using this and the Impredicative Set universe.  

 

-Zhong

On Tue, Jun 10, 2008 at 7:49 AM, Adam Chlipala <adamc AT hcoop.net> wrote:

Benjamin Pierce wrote:

If you add to the simply typed lambda-calculus a type Dynamic with an introduction rule analogous to your constructor plus a 'typecase' construct for eliminating Dynamics, you can write non-terminating programs.  But it's not clear to me whether injectivity gives you that much power.

Indeed, I'm using this type to model Turing-complete programming languages, and it's clear that any "computational" way of getting at the contents of a dynamic package can't work.  But the theorem I'm asking about is in Prop, so we know it can never affect computations in Set or (non-Prop) Type, which gives me some hope that it might be a consistent axiom.

On Mon, Jun 9, 2008 at 3:37 PM, Adam Chlipala <adamc AT hcoop.net <mailto:adamc AT hcoop.net>> wrote:

   Does anyone know if it would be consistent with (impredicative
   Set) CIC to assert the injectivity of the [Dyn] constructor below
   as an axiom?

   Inductive dynamic : Set :=
    | Dyn : forall T, T -> dynamic.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club