The Coq mailing list

[Judicael Courant <Judicael.Courant AT ens-lyon.fr>]

Bonjour,

   Mon énoncé n'est certes pas démontrable en Coq mais il est pourtant
   vrai.

Bien que non-spécialiste des problèmes d'égalité, il me semble qu'il
n'est justement pas nécessairement vrai. Dans la plupart des cas, on
est effectivement très intéressé par les axiomes d'extensionnalité,
mais il est parfois tout à fait intéressant de se placer dans des
théories dans lesquelles cet axiome n'est pas vrai.

L'intensionnalité est très intéressante par exemple lorsqu'on
considère des systèmes de programmation modulaire : on ne veut pas que
deux modules soient égaux par accident, mais uniquement par
intention. Ainsi, si deux modules m et m' définissent les memes champs
avec les memes valeurs, on n'aura pas nécessairement l'égalité de m et
m'.

Cordialement,

Judicael.
-- 
Judicael.Courant AT ens-lyon.fr,
 http://www.ens-lyon.fr/~jcourant/
tel : (+33) 04 72 72 82 28