The Coq mailing list

[Benjamin Werner <Benjamin.werner AT inria.fr>]

Let me shift the frontier of what we know to know:

Call dd1 and dd2 your two axioms; so dd2->dd1 is obvious.

You can show that dd1+ext -> ~~dd2
(where ext is harmless extentionality for functions :

Axiom ext : forall A : Type , forall B : A->Type , forall f g :  
(forall a:A,(B a)) ,
(forall a:A , (f a)=(g a)) -> f=g.

so if you accept ext, if you can reformulate the above

~dd2 -> ~dd1

so you do not further endanger consistency by switching from dd1
to dd2.

If you drop the condition for your relation R to be functional, you
do not need ext anymore.

Whether you really need ext, I do not know :-)

So all these axioms are OK with the standart set-theoretic
semantics.

To answer Pierre : all you lose is the assurance that you will
be able to extract a program form any proof. But from the
consistency point of view, requiring that
exists f : A -> B , ...
is already quite strong, since it requires (for most model
constructions) that the function f exists in the model.

I attach the two proof files. They certainly need some
cleaning. Maybye they could even be made really shorter ?

You can thank my kid who made my night short !

Best wishes to all,


Benjamin


Le 10 févr. 06 à 10:41, Yves Bertot a écrit :

> I am dissatisfied with the form of the axiom of dependent description,
> as it is given in Logic/ClassicalDescription.v and the associated
> theorems.
>
> Axiom
>   dependent_description :
>     forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
>       (forall x:A,
>           exists y : B x, R x y /\ (forall y':B x, R x y' -> y =  
> y')) ->
>        exists f : forall x:A, B x, (forall x:A, R x (f x)).
>
>
> This axioms gives me the existence of a function but not the  
> possibility
> to use this function easily in further definitions.  I believe a
> stronger version would be the following one:
>
> Axiom
>   dependent_description' :
>     forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
>       (forall x:A,
>           exists y : B x, R x y /\ (forall y':B x, R x y' -> y =  
> y')) ->
>        sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
>
> (the difference between dependent_description and  
> dependent_description'
> is that I replaced the last exists by sigT. )
>
> I would like to know whether adding this axiom would yield an
> inconsistent logic.  Morally, I would be satisfied with the idea that,
> in classical logic, the functional notation of Coq is just a short- 
> hand
> for "set-theory-like" functions but I am aware that we may be  
> navigating
> close to Cantor's naive set theory
>
> I believe the answer can fall in three categories:
>
> 1/ No problem, you can already derive dependent_description' from
>    dependent_description using other axioms of classical logic that
>    are thought to be sensible (a coq proof would be great).
>
> 2/ Big problem, once you do that, you can encode one of the well-known
>    paradoxes (again a coq proof would be great).
>
> 3/ Nobody knows.
>
> Does anyone have a quick answer in the direction of 1 or 2?  Does  
> anyone
> know that we don't know?
>
> Yves
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/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