Herman Geuvers a montré que l'ajout d'un axiome fort de logique classique dans Coq (ça doit aussi marcher avec le Calcul des Constructions non inductives) aboutissait à une incohérence.

Son axiome fort est plus puissant que l'axiome habituel, qui est le tiers exclu (ou, de façon équivalente, l'axiome de Peirce) : en effet, il dit non seulement que pour tout P, P ou non P est vrai, mais qu'il y a un mécanisme qui retourne cette valeur de vérité sous forme d'un booléen au sens ordinaire de Coq (dans Set).

Mon intuition de l'argument de Geuvers, suite à un survol de l'article, est que si on a un lien si fort entre Prop et Set, on peut définir dans Set des fonctions qui dépendent par cas du contenu de termes dans Prop et aboutir à un paradoxe — mais je n'ai peut-être rien compris.

Je me demandais s'il n'y aurait pas une preuve du même fait par la calculabilité. En effet, l'axiome classique fort supposé revient, s je ne m'abuse, à supposer l'existence d'un oracle universel donnant effectivement la vérité ou la fausseté de toute proposition. On doit notamment pouvoir appliquer cela à l'arrêt d'un processus de calcul (p.ex. beta-réduction dans un système de calcul pas trop compliqué, genre lambda-calcul en indices de de Bruijn ou combinateurs SKI) et ainsi aboutir à une contradiction par diagonalisation à la Turing. Suis-je trop naïf ?