Résumé
On peut opposer logique classique et logique intuitionniste comme deux ennemis irréductibles, comme dans la polémique entre hilbert et Brouwer en 1927. Plus positivement, on peut, comme Gödel dans les années 1930, utiliser la logique intuitionniste pour mieux comprendre la logique classique. Tout d’abord, la logique classique peut être vue comme la logique intuitionniste à laquelle on ajoute un axiome classique, comme le tiers exclu « P ou ¬P » qui donne son titre à ce cours. Plus surprenant : la logique classique se plonge dans la logique intuitionniste via une traduction par double négation. Si P est une formule propositionnelle, P est vraie en logique classique si et seulement si ¬ ¬P, « P n’est pas faux », est démontrable en logique intuitionniste. Kolmogorov, Gödel, Gentzen, Kuroda étendent cette traduction doublement négative à des formules avec quantificateurs.
Coup de théâtre en 1990 : Murthy et Griffin mettent en correspondance ces approches de la logique classique avec le concept de continuation dans les langages de programmation. Dans un langage fonctionnel, la continuation d’une expression a est le calcul qui reste à faire pour terminer le programme une fois a évaluée. On peut voir cette continuation comme une fonction de la valeur de a vers la valeur du programme complet. Un programme peut agir sur ses continuations de deux manières : soit on l’écrit en style à passage de continuation (CPS, Continuation-Passing Style), où chaque expression reçoit sa continuation en argument supplémentaire ; soit on ajoute au langage de programmation des opérateurs de contrôle permettant de réifier les continuations, comme l’opérateur call/cc du langage Scheme. Murthy est le premier à observer que les transformations CPS, qui mettent un programme en forme CPS, correspondent, au sens de Curry-Howard, avec les traductions par double négation en logique. En parallèle, Griffin observe que certains opérateurs de contrôle admettent des types qui correspondent, au sens de Curry-Howard, avec des axiomes de logique classique. Ainsi, l’opérateur call/cc correspond à la loi de Clavius, (¬P ⇒ P) ⇒ P, et l’opérateur C de Felleisen à l’élimination de la double négation, ¬¬P ⇒ P.
Ces beaux résultats permettent déjà d’identifier le contenu calculatoire de démonstrations classiques. Cependant, un aspect important de la logique classique est perdu : la dualité entre conjonction et disjonction via la négation, visible dans la loi de de Morgan ¬ (P ∧ Q) ⇔ ¬P ∨ ¬Q et magistralement exprimée dans le calcul des séquents classiques de Gentzen (1934). Quel langage de programmation correspond par Curry-Howard à ce calcul des séquents classique ? Les travaux récents de Parigot, Curien, Herbelin, Wadler et d’autres donnent des éléments de réponse à cette question.
