Incohérence d'une version forte de la logique classique en théorie des types
Par David Monniaux le mercredi, janvier 18 2012, 13:51 - Théorie - Lien permanent
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 ?
Commentaires
En fait, l'axiome qu'il donne est incohérent avec Set imprédicatif (ce n'est plus le défaut dans coq, mais tu peux le récupérer avec le flag idoine). Coq actuel est cohérent avec l'axiome qui prétend l'équivalence entre Prop et bool (pas que ce soit un axiome particulièrement intéressant).
En revanche, l'axiome de Geuvers n'est évidemment pas cohérent avec la thèse de Church interne (qui dit que le système sait que chacune de ses fonctions est récursive).
Note aussi que l'axiome est équivalent au tiers exclu usuel si on ajoute l'axiome apparemment innocent (choix unique) :
∀x:A,∃!y:B, R x y → ∃f:A→B,∀x:A, R x (f x)
Pour A et B dans Set.
Après, je ne suis pas convaincu par ton intuition de pourquoi U- est incohérent. Ça n'a pas, me semble-t-il grand chose à voir avec le pattern-matching,
Donc je n'ai rien compris (enfin, je n'ai pas eu le temps de lire les choses).
Un doute m'assaille : Prop est imprédicatif et ça ne crée aucun paradoxe, quelle est la différence entre Set et Prop qui provoque la catastrophe si on établit cette correspondance entre True/False et bool ?
La différence c'est que dans Set on peut montrer que true et false (de type bool) sont différents. Dans Prop, on peut supposer que toutes les preuves des propositions sont égales (et si on suppose la tiers exclu, on peut le démontrer).
@Arnaud Spiwack: C'était ce à quoi je faisais allusion avec le pattern-matching: dans Set, tu peux différencier deux termes appartenant au même type en examinant leurs constructeurs, tandis que Prop est compatible avec l'axiome « proof irrelevance ». En revanche, je ne sais pas quelle règle de typage est subtilement différente ; j'aurais tendance à dire que dans Prop tu n'as pas le droit de faire dépendre le type de retour d'un match du terme effectivement matché, mais je peux me tromper.
C'est essentiellement ça. Ce n'est pas sans subtilité, mais la seule différence est dans ce qui est autorisé dans les clauses de retour du pattern matching.
Mais ce n'est, il me semble (je n'ai aussi lu le papier qu'en diagonale), qu'un détail dans le paradoxe de Geuvers, on s'en sert pour montrer que l'axiome implique un isomorphisme entre Prop et bool (dans Prop on peut montrer que True≠False, alors on va en avoir besoin dans bool, sinon on a rien dit d'utile). Une fois que cet isomorphisme est établi, on peut encoder le système U- qui n'a pas de pattern matching mais qui est incohérent.