The Coq mailing list

["Gilles Kahn" <Gilles.Kahn AT inria.fr>]

David Nowak a écrit dans le message
<1998Jan13.135105.20270 AT sophia.inria.fr>...
>Bonjour,
>
>Mon énoncé n'est certes pas démontrable en Coq mais il est pourtant
>vrai.
>
>J'ai remarqué dans différents développements en Coq, que les auteurs
>n'hésitent pas à rajouter un axiome pour passer de l'égalité
>extensionnelle à l'égalité intensionnelle (Dans le module Ensembles de
>la librairie standard par exemple). L'ajout de l'axiome suivant
>remettrait-il en cause la cohérence du système Coq ?


Il y a peu de risque pour Coq, tout au plus pour la théorie développée.
Dans le cas du module Ensembles, je me suis résolu à rajouter l'axiome
d'extensionnalité
parce que je n'arrivais pas à faire autrement. Je me suis satisfait des
réponses de
l'époque, dans le genre de celle d'Eduardo, sans aller plus loin parce que
mon objectif n'était
pas de faire de la méta-théorie. Je n'ai jamais été capable de démontrer des
choses incongrues
grâce à cet axiome. J'ai pensé que mon attitude avait pour précédent celle
des mathématiciens
qui laissent les logiciens faire leur travail et qui font avancer leur
propre domaine.

Ceci dit, si j'avais disposé d'une preuve de l'innocuité de l'axiome,
j'aurais été ravi, évidemment.

Gilles Kahn