Avertissement

Cette spécification a été écrite dans un but pédagogique, en reprenant le style axiomatique des spécifications algébriques telles qu'elles étaient présentées aux étudiants. Isabelle a été choisi comme outil pour permettre aux étudiants de manipuler concrètement ce type de spécification. Toutefois, cette spécification a un vice caché dans l'utilisation de datatype pour définition les opérations Not, And et Or.

En effet, datatype permet de définir les constantes et les constructeurs d'un type, et implicitement, l'hypothèse est faite que les différents constructeurs produisent des termes différents. Ainsi, d'après cette définition, false est différent de tout terme construit avec Not, alors que l'axiome b1 dit que false = Not true. À partir de cette contradiction, on peut démontrer n'importe quoi, comme le montre l'exemple suivant :

Une définition axiomatique qui semble raisonnable peut donc se révéler très risquée...