Règles et signification : le point de vue de la logique classique
p. 213-233
Texte intégral
1Il s’agit ici d’évaluer l’impact philosophique de l’extension de l’« isomorphisme de Curry-Howard » à la logique classique ; nous chercherons à comprendre ce que cette extension veut dire du point de vue d’une théorie antiréaliste de la signification, révisionniste en matière logique. L’isomorphisme de Curry-Howard reflète en effet les propriétés de la logique intuitionniste qui en font la bonne logique pour un antiréaliste soucieux de satisfaire aux réquisits de Michael Dummett en matière de théorie de la signification. Que cet isomorphisme puisse être étendu à la logique classique, voilà qui constitue par conséquent un achèvement technique remarquable et surprenant. Dans le meilleur des cas, on serait alors en droit d’attendre que cette extension fournisse les bases d’une théorie de la signification qui satisferait ces réquisits, ou à peu près, sans être pour autant révisionniste. Voilà précisément la question que nous voulons discuter.
2Dans la première section, nous présentons le cadre de ce débat : l’approche antiréaliste est fondée sur un réquisit de manifestabilité, qui conduit à adopter une sémantique en termes de conditions de prouvabilité plutôt qu’en termes de conditions de vérité (1.1) ; ceci peut être fait pour les constantes logiques dans le format de la déduction naturelle, et l’isomorphisme de Curry-Howard reflète alors les propriétés sémantiquement pertinentes de la déduction naturelle intuitionniste (1.3). Michael Dummett soutient que ces bonnes propriétés ne sont pas partagées par la déduction naturelle classique (1.4). Le problème abordé dans la seconde section est donc de savoir si l’extension au cas classique de l’isomorphisme réfute ces arguments. Après une présentation de l’extension elle-même (2.1), il apparaît que seule une partie des bonnes propriétés sémantiques est donnée par l’extension (2.2) ; une réfutation complète du révisionnisme, c’est-à-dire l’établissement d’une théorie de la signification sur les bases de l’isomorphisme, demande une explication du contenu calculatoire des preuves classiques (2.3) que nous présentons dans le cas de l’arithmétique. Nous concluons sur la question ouverte du statut du principe d’harmonie dans le cas classique (2.4).
1. L’isomorphisme de Curry-Howard et l’approche antiréaliste de la signification
1.1 L’approche antiréaliste de la signification
3Notre point de départ réside dans les arguments sémantiques que Dummett propose dans [Dummett 1978a] en faveur de la logique intuitionniste, son idée étant que la meilleure justification possible pour le choix d’un cadre logique n’est pas ontologique mais sémantique. Rappelons brièvement cette stratégie, afin de voir comment elle conduit à la thèse selon laquelle une théorie de la signification pour les énoncés mathématiques doit nécessairement s’appuyer sur la notion intuitionniste de preuve.
4Le réquisit central, qui ressort d’une simple analyse de ce qu’est la signification et que toute théorie raisonnable de la signification doit donc satisfaire, est un réquisit de manifestabilité. Une théorie de la signification pour un langage doit nous donner une théorie de ce que c’est que connaître ce langage ; le réquisit de manifestabilité impose que cette connaissance soit toujours manifestable. La connaissance de la signification des termes d’un langage ne saurait aller au-delà de la capacité à en faire un usage correct. Plusieurs arguments peuvent être invoqués à l’appui de cette thèse. D’abord, la signification est par nature quelque chose de communicable. Or un individu ne saurait communiquer à un autre quelque chose qui transcenderait l’usage correct qu’il fait du langage et ne résiderait que dans son esprit ; comme le dit Dummett, « un individu ne peut communiquer ce qu’on ne peut observer qu’il communique ». Ensuite, on peut tirer argument de ce qu’on apprend quand on apprend une langue. Cet apprentissage n’est rien d’autre que l’apprentissage de certaines pratiques, donc si la signification devait être quelque chose de plus, elle ne saurait être apprise. Enfin, si la connaissance des significations peut s’exprimer parfois explicitement en termes de connaissance d’autres significations, par exemple à travers l’aptitude à gloser un terme ou à donner des synonymes, mais, sous peine de régression à l’infini, elle ne peut se réduire à cela, en dernière analyse : elle doit se ramener à des connaissances implicites, ces connaissances implicites doivent être manifestables, si l’on veut pouvoir les attribuer à quelqu’un.
5C’est sur la base de ce réquisit ainsi justifié que se pose la question de savoir si une théorie de la signification en termes de conditions de vérité pour des énoncés logiques ou mathématiques est possible. Prawitz [Prawitz 1976] a proposé le dilemme suivant en guise de réponse négative à cette question, qu’il appelle le dilemme platoniste (est dite platoniste une théorie de la signification pour laquelle saisir la signification d’un énoncé consiste à savoir ce que c’est, pour cet énoncé, que d’être vrai) :
soit une théorie platoniste est inutile. En effet, la connaissance des conditions de vérité d’un énoncé F doit être rendue manifeste sous la forme d’une connaissance de ce qui devrait compter comme preuve de F, la théorie platoniste est alors inutile parce qu’elle doit être doublée par une théorie des conditions de prouvabilité ;
soit elle est sans fondement. Si le défenseur d’une théorie platoniste refuse cette béquille et maintient que la connaissance concernant les conditions de vérité transcende la connaissance concernant les preuves, il est alors forcé d’admettre que cette connaissance n’a pas de conséquence empirique. En effet, dans le cas où la vérité d’un énoncé est indécidable, c’est-à-dire dans le cas où la connaissance des conditions de vérité ne peut pas s’appuyer sur la connaissance d’une méthode pour décider la vérité, on ne voit pas comment pourrait se manifester la connaissance des conditions de vérité.
6Si l’on accepte ce dilemme, on doit donc accepter de faire des preuves l’ingrédient essentiel d’une théorie de la signification des termes logiques et mathématiques.
1.2 La signification des constantes logiques : quatre éléments clés
7Lorsqu’on cherche à développer selon ces lignes une théorie de la signification pour les constantes logiques, on est conduit à utiliser le formalisme de la déduction naturelle afin d’y lire les conditions de prouvabilité des énoncés comportant tel connecteur comme connecteur principal. En effet, les règles d’introduction de la déduction naturelle déterminent précisément les conditions auxquelles il est permis d’affirmer un énoncé. Mais une théorie de la signification pour les constantes logiques doit en outre satisfaire des réquisits propres au domaine de la logique ; en particulier, on attend d’elle qu’elle justifie en retour la pratique déductive.
8Suivant [Dummett 1978b], la justification de la déduction comporte deux aspects différents. D’une part, il faut en expliquer la légitimité, il faut rendre compte de la validité des preuves que l’on peut obtenir à partir d’un certain système de règles. Mais il faut expliquer d’autre part son utilité, ce qui est à l’origine de la fécondité de la déduction. Répondre à ces questions nécessite de distinguer deux aspects complémentaires de la signification : il faut distinguer les conditions d’assertabilité d’un énoncé, ce qui nous donne le droit de l’asserter d’un côté, et ce qu’on pourrait appeler ses conditions d’exploitabilité de l’autre. Cette dualité correspond à la dualité des règles d’introduction et d’élimination de la déduction naturelle. Par exemple dans le cas de l’implication (voir figure 1), la règle d’introduction nous dit que l’on est position d’asserter A → B si l’on dispose d’une preuve conditionnelle de B sous l’hypothèse A. La règle d’élimination nous dit quant à elle ce que l’on peut faire si l’on est en droit d’asserter A → B : on peut exploiter cet énoncé pour obtenir une preuve de B si l’on a également une preuve de A. La validité de ce couple de règles vient alors d’une forme d’harmonie entre celles-ci : on ne doit pas pouvoir inférer plus à partir d’un énoncé que ce que l’on est en droit d’inférer du fait qu’on est en droit de l’asserter. Techniquement, l’harmonie se révèle alors à travers les étapes locales de la procédure de normalisation, à travers les procédures de conversion (voir figure 1). Celles-ci consistent à éliminer une règle d’introduction suivie d’une règle d’élimination dont la prémisse principale vient d’être obtenue à partir de la règle d’introduction : elles nous disent précisément qu’on obtient par ce détour plus que ce qu’on avait déjà. À la suite de Dummett, Prawitz a élaboré précisément cette idée dans [Prawitz 1973] en généralisant l’idée selon laquelle les procédures de conversion constituaient en fait des justifications pour les règles d’élimination. De plus, nous avons ici tous les éléments pour expliquer la fécondité de la déduction, à travers la distinction entre preuves directes (normalisées) et preuves indirectes (au sens de non normalisées) :les preuves indirectes sont fécondes parce que, lorsque nous en avons une, il nous est possible de reconnaître un énoncé comme vrai, c’est-à-dire de savoir qu’il en existe une preuve directe, alors même que cette possibilité n’a pas été actualisée, puisque nous n’avons encore qu’une preuve indirecte, laquelle donne fournit une preuve directe après normalisation.
9En combinant la perspective générale et les spécificités d’une théorie de la signification appliquée aux constantes logiques, il nous semble possible de ressaisir ainsi les éléments clés de la théorie antiréaliste de la signification des constantes logiques comme celle de M. Dummett et D. Prawitz :
C’est une théorie moléculariste de la signification, elle entend montrer comment la signification d’un énoncé est déterminé par sa structure interne. Elle s’oppose à une attitude holiste qui consisterait simplement à dire : voilà les règles de la logique classique et ce sont elles qui déterminent globalement la signification des connecteurs classiques. Au contraire, on cherche à expliquer la compétence des locuteurs, plutôt qu’à renvoyer simplement la signification des termes du langage à l’usage total du langage. Ce n’est qu’à partir d’une telle perspective que se posent la question des conditions spécifiques d’assertabilité des énoncés ayant tel ou tel connecteur principalx et la question de la justification de la pratique déductive.
C’est une théorie de la signification en termes d’opérations : elle nous dit ce qu’une preuve d’un énoncé doit faire pour être une preuve de cet énoncé (par exemple, une preuve de A → B doit nous donner une preuve de A à partir d’une preuve de B).
Le réquisit d’harmonie est la pierre de touche de l’admissibilité de nouvelles constantes logiques ou de nouvelles règles. C’est seulement à cause de ce réquisit que cette théorie est potentiellement révisionniste, puisque l’harmonie est une norme de l’usage des termes logiques dans les preuves.
Cette théorie repose de manière essentielle sur la compréhension de ce qu’est une preuve. Pouvoir reconnaître un énoncé comme vrai signifie connaître une preuve de cet énoncé ; les preuves sont les objets du genre de connaissance que décrit la théorie de la signification. En particulier, cela implique que les preuves doivent pouvoir être considérées comme des objets (de connaissance), et donc au moins que l’on dispose de critères d’identité des preuves, en vertu du slogan qui ni en selon lequel il n’y a pas d’entités respectables sans critères d’identité pour ces entités.
1.3 En quoi Curry-Howard reflète ces éléments clés
10L’isomorphisme de Curry-Howard met en rapport les preuves intuitionnistes et les termes du lambda-calcul : il permet d’associer des lambda-termes aux preuves de manière à ce que la réduction du lambda-calcul corresponde à la normalisation des preuves, et donc de voir les preuves comme d’authentiques programmes. Par exemple (voir figure 1), l’introduction de l’implication correspond à la lambda-abstraction, tandis que la règle d’élimination correspond à l’application. L’étape de conversion correspond alors à la β-réduction. La correspondance est loin d’être arbitraire, puisque le plongement des preuves dans le langage de programmation fonctionnel idéalisé qu’est le lambda-calcul, permet précisément de donner une interprétation précise aux intuitions fonctionnelles de l’interprétation dite BHK (pour Brouwer-Heyting-Kolmogorov) des constantes intuitionnistes selon laquelle, par exemple, une preuve de A → B est une fonction qui rend une preuve de B lorsqu’on lui donne en argument une preuve de A. Mieux, on peut voir qu’à chacun des éléments clés mis en évidence précédemment l’isomorphisme fait correspondre un élément du côté programme :
Théorie de la signification | Via l’isomorphisme... |
1. molécularisme | énoncés comme spécification de type |
2. opérationalité | preuves comme programme |
3. harmonie | compatibilité de la réduction avec le typage |
preuves comme objets égalité | entre les termes induite par la réduction |
11Ainsi la signification de l’isomorphisme de Curry-Howard se laisse reconduire à la mise en évidence de nos quatre propriétés.
12Premièrement, la connaissance de la signification d’un énoncé est expliquée comme la connaissance de ce qui devrait compter comme une preuve de cet énoncé. L’isomorphisme nous permet de voir les énoncés comme spécifiant des types pour les programmes : le type A d’un programme (ce que fait un programme) est précisément une manière de dire ce qu’une preuve de A doit faire pour être une preuve de A. Et ceci est moléculariste parce que les spécifications peuvent être directement lues de manière compositionnelle à partir des énoncés.
13Deuxièmement, les preuves peuvent directement être vues comme des programmes. Au contraire, par exemple, la théorie de la réalisabilité de Kleenne ne donnait accès que de manière indirecte, via des codages, à la signification constructive des preuves intuitionnistes (voir Jean Fichot [Fichot2002]). En particulier, cela signifie que les preuves peuvent être utilisées pour obtenir des algorithmes, ainsi l’extension du système de typage à l’arithmétique fonctionnelle du second ordre fournie par Krivine, permet d’utiliser les preuves intuitionnistes pour obtenir des programmes qui font des calculs sur les entiers (Krivine et Parigot [Krivine-Parigot 1990]).
14Ensuite, l’harmonie correspond à préservation des types à travers la réduction (voir figure 1). Les formes normales pour les termes correspondent aux preuves directes, et l’existence de formes normales pour les termes typables montre comment les preuves indirectes donnent des preuves directes.
15Enfin, l’existence et l’unicité des formes normales permettent de donner des critères d’identité raisonnables pour les preuves qui ne sont ni suffisamment fins (un même théorème admet différentes preuves) ni suffisamment larges (les preuves qui ont la même signification computationnelle sont identifiées).
16À ce stade, le cadre de discussion de l’impact philosophique de l’extension de l’isomorphisme est posé : si l’importance de l’existence de l’isomorphisme pour le projet réaliste réside bien dans les quatre points que nous avons mis en évidence, l’importance de l’extension de celui-ci à la logique classique doit pouvoir être décidé à partir de la préservation ou non de ces propriétés.
1.4 Pourquoi le révisionnisme logique
17Reste à voir pourquoi une théorie de la signification qui prétendait se fonder sur l’usage, donc en l’occurence sur les preuves, aboutit à une position révisionniste, selon laquelle la logique n’est pas la logique la plus couramment en usage, à savoir la logique classique, mais la logique intuitionniste. Voyons les arguments proposés par Dummett pour établir qu’une sémantique en termes de conditions de prouvabilité justifie la logique inuitionniste, mais pas la logique classique.
18Pour obtenir la logique classique, il faut ajouter aux règles intuitionnistes de la déduction naturelle, une règle supplémentaire. Ce peut être par exemple la règle d’élimination de la double négation (voir figure 2) qui vient alors compléter les deux règles attendues pour la négation. Pour Dummett, le problème est que le système ainsi obtenu viole le réquisit d’harmonie. Si c’est bien le cas, la logique classique n’est pas justifiée du point de vue d’une sémantique en termes de conditions de prouvabilité1.
19Pourquoi exactement le réquisit d’harmonie est-il violé ? Selon la perspective adoptée, toute règle correspond soit à des conditions d’assertabilité, soit à des conditions d’exploitabilité ; pour rejeter une règle, il faut donc établir qu’elle ne peut être comprise selon aucune de ces deux options, c’est-à-dire qu’elle ne peut être considérée ni comme une règle primitive d’introduction, ni comme une règle dérivée d’élimination accompagnée d’une procédure de justification.
20Il est facile de voir qu’elle ne peut être considérée comme une règle d’élimination. L’élimination de la négation s’accompagne d’une procédure de conversion très simple ; en revanche, si l’on considère la règle de la double négation comme une autre règle d’élimination de la négation, on n’est pas en mesure de fournir la même chose (voir figure 2), tout simplement parce qu’il n’y a pas en général de moyen d’extraire d’une preuve du faux, sous l’hypothèse de la négation de A, une preuve de A.
21Il faut également pouvoir argumenter que la règle de la double négation ne peut pas être vue comme une règle d’introduction pour la formule A ; le point ici est plus délicat car il n’y a pas, semble-t-il, de contrainte apriori sur les règles d’introduction. L’argument de Dummett [Dummett 1991] repose sur le fait qu’elle vit mal avec les autres règles d’élimination. Ainsi si la conclusion d’une règle de double négation est soumise à une règle d’élimination de la disjonction (voir figure 3), on peut certes déplacer l’application de la première règle de manière à ce qu’elle ne soit pas suivie par la seconde, mais pour autant on n’est pas parvenu à éliminer l’application de la règle d’élimination, ce qui devrait être le but de la normalisation vue comme procédure de justification, et il n’est pas possible de transformer cette preuve en une preuve directe de la conclusion. Néanmoins, on sait grâce à Prawitz que l’usage de la règle spécifiquement classique qu’on ajoute à la déduction naturelle intuitionniste peut être restreint aux formules atomiques2, il faut donc pousser plus loin l’argument et établir que la double négation n’est pas admissible même comme règle d’introduction pour les seuls atomes. Ici peuvent intervenir plusieurs arguments locaux : on dira que les conditions d’assertabilité des formules atomiques doivent rester en dehors du champ d’application de la logique, que faire cela conduirait à briser la définition inductive des conditions d’assertabilité puisqu’on doit alors prendre en compte les conditions d’assertabilité de ¬A pour donner celles de A. Mais il y a également un motif plus global : en ajoutant une règle classique, on perd inévitablement la signification constructive associée aux conditions d’assertabilité. Même si, par exemple, les règles d’introduction et d’élimination du quantificateur existentiel restent techniquement en harmonie, il n’est plus vrai qu’une preuve d’un énoncé existentiel nous donne le témoin que l’on attend, de sorte qu’il n’est plus vrai que l’on puisse toujours obtenir les preuves directes attendues. Il est donc bien clair que même vue comme une règle d’introduction restreinte aux formules atomiques, la règle de la double négation entraîne une perturbation globale du système.
22À ce stade, rien ne semble moins attendu qu’une extension de l’isomorphisme de Curry-Howard. Parce que le point de vue adéquat pour une justification de la logique classique est soit holiste (« voilà les règles que l’on utilise ») soit platoniste (en termes de condition de vérité), et aussi pour d’autres raisons techniques (parce que les preuves classiques ne se comportent pas aussi bien que les preuves intuitionnistes), il ne semble pas possible d’expliquer la signification d’un énoncé classique en termes de ce que devrait faire une preuve. Donc en un sens, la simple idée d’étendre l’isomorphisme peut sembler étrange. Il nous faut donc examiner attentivement ce quia été fait dans cette direction.
2. L’impact de l’extension de Curry-Howard
2.1 Une brève histoire de l’extension
23Deux points de vue sont possibles sur l’isomorphisme :
le point de vue des programmes. La logique est vue comme un système de typage. Les questions intéressantes sont : quel genre d’instructions sont typables ? En particulier, est-ce que le typage force un style de programmation fonctionnelle ou est-ce qu’on peut aussi utiliser des instructions qui relèvent de la programmation impérative ?
le point de vue des preuves. Le lambda-calcul permet de mettre en avant des propriétés structurelles des preuves. Les questions posées sont typiquement : quelles propriétés des preuves peut-on étudier grâce à l’isomorphisme, et quel genre de règles peut-on traiter au sein de l’isomorphisme ?
24Dans quelle perspective l’extension a-t-elle été imaginée ? La réponse est sans ambiguïté : l’article séminal de Griffin de 1990 ([Griffin 1990]) montre comment il est possible d’étendre à un langage de programmation, un « Scheme » idéalisé, le paradigme des preuves comme types. Scheme contient, en plus d’une base de lambda-calcul avec une procédure d’évaluation particulière, une instruction de contrôle du contexte, « call/cc », qui permet d’accéder à la continuation courante. Griffin montre qu’une instruction analogue à call/cc, l’opérateur C de Felleisen, peut être typée en utilisant la loi de la double négation. Le point important est que cette loi classique est appelée par le problème de typage. Sans entrer dans les détails de la procédure d’évaluation du langage, on peut le montrer en donnant les règles d’évaluation de l’opérateur C et de l’opérateur A qui l’accompagne3 :
25E[C(M)] >C M (λz. A(E[z])) et E[A(M)] >A M
26Dans cette définition, E désigne un contexte d’évaluation, M un terme clos. L’opérateur A est définissable en termes de C par : A(M) = def C(λd.M). On décrit parfois cette évaluation en disant que « A jette le contexte et continue l’évaluation du terme ».
27Le raisonnement de Griffin est le suivant. Soient G et H deux types arbitraires, supposons que le contexte E ait pour type G et qu’il attende un terme de type H. Comme (λz. A(E(z))V >E(V) pour toute valeur V et que E(V) est de type G, le terme λz. A(E(z) doit être de type H → G. Par ailleurs, dans la règle d’évaluation pour C, le terme E[C(M)] a pour type G, donc M (λz.A(E[z])) aussi, donc M doit être de type (H → G) → G. Comme E attend un terme de type H, il faut que C soit de type ((H → G) → G) → H. Mais on remarque que, un terme N de type G ’étant donné, le terme C(λd. N) peut être typé de n’importe quel type H. Afin de préserver la consistance du système, on doit donc prendre G =⊥ (où ⊥ est le type vide).
28Le système de Griffin présente des défauts techniques et, surtout, il ne nous montre pas quelles sont les propriétés structurelles des preuves qui sont révélées par cette nouvelle correspondance. C’est le travail de Michel Parigot sur la déduction naturelle classique et le λµ-calcul([Parigot 1992], [Parigot 1993]) qui prolonge la découverte de Griffin en en donnant l’interprétation du point de vue des preuves qui est bien sûr celui dont nous pouvons attendre des bénéfices pour la perspective philosophique qui est ici la nôtre.
29Techniquement (voir figure 4), Parigot utilise un système de déduction naturelle multi-conclusion avec une formule active distinguée. Il ajoute au λ-calcul usuel un nouveau lieur, µ, et de nouvelles variables. Pour avoir une intuition du fonctionnement des lieurs µ, on peut les voir comme des canaux qui font rentrer tous les arguments du terme à l’intérieur du terme aux places marquées par les µ-variables. En ce qui concerne le typage, on ajoute des contextes à droite, afin de prendre en charge les conclusions multiples. La règle pour µ permet de gérer les changements de formule active ; elle comprend comme cas particuliers la règle d’affaiblissement (si β n’est pas déjà dans le contexte) et la règle de contraction (si α est déjà dans le contexte). Du point de vue de la procédure de normalisation, l’effet de la µ-reduction (voir figure 5 où (µα. u)v >µ µα. u'4) est de permettre aux arguments d’une formule ayant été active à un moment donné d’atteindre l’endroit de la preuve où ces formules l’étaient effectivement. C’est donc cette étape nécessaire de la normalisation pour un système multi-conclusion qui est traitée spécifiquement par le lieur µ qui étend le lambda-calcul.
2.2 Contenu opérationnel et critères d’identité
30Que nous donne la correspondance de Parigot entre preuves classiques et termes du λµ-calcul ? Nous obtenons immédiatement deux des quatre propriétés recherchées : la propriété 2 et la propriété 4.
31D’une part, l’extension donne un contenu calculatoire aux preuves classiques. Par exemple (voir [Parigot 1993]), le terme λf.µα[α](f)λx.µδ[α]x qui code une preuve de la loi de Pierce ((A → B) → A) → A a un comportement analogue à l’opérateur call/cc de Scheme. Soient t un terme et u1,..., un un contexte d’évaluation, l’exécution du programme donne :
32Ce qui veut dire notamment que, si t est de la forme λz.u et, si dans la suite du calcul de u[z : = λx.µδ[α](xu1) ...un)] avec les arguments u1,..., un, on rencontre une étape (λx.µδ[α](xu1) ...un))w, alors le programme va exécuter le terme w dans le contexte de départ.
33D’autre part, le λµ-calcul a de bonnes propriétés calculatoires ; il est confluent et les termes typables normalisent fortement. Ceci nous donne un notion syntaxique d’égalité entre les termes typables. Cette notion nous fournit un bon critère d’identité pour les preuves, qui n’identifie pas toutes les preuves d’un même théorème (en particulier, par exemple, les entiers ne sont pas identifiés). C’est loin d’être trivial, car cela revient à apporter une solution dans le cadre de la déduction naturelle classique au problème du non-déterminisme de l’élimination des coupures pour les séquents classiques. L’argument selon lequel les preuves classiques ne peuvent pas jouer le rôle des preuves intuitionnistes pour une théorie de la signification parce qu’elles ne se comportent pas suffisamment bien (parce qu’elles serait ambiguës et impossibles à désambiguïser) est réfuté.
34L’extension de l’isomorphisme nous permet de comprendre quand deux preuves sont identiques. Il nous permet aussi de voir les preuves comme des programmes, lesquels ont des traits de programmation impérative. C’est une première étape nécessaire si l’on veut utiliser les preuves comme support pour une théorie de la signification. Mais en même temps, de ce point de vue, l’extension pourrait sembler décevante, car c’est loin d’être suffisant. Il ne semble pas en particulier que nous soyons capables pour autant de construire la théorie de la signification moléculaire qui était la contrepartie intuitionniste de la spécification des types. Parce que la déduction naturelle classique utilise des conclusions multiples, les règles d’introduction ne peuvent plus être vues comme des règles donnant la signification, ou alors il faudrait présupposer une explication classique de la disjonction. Sans tout cela, la préservation des types par la réduction n’est plus très significative, parce que nous ne savons pas comment interpréter l’harmonie. Les deux propriétés qui manquent sont donc cruciales.
2.3 La spécification
2.3.1 La spécification comme problème
35Dans la mesure où l’extension de la correspondance ne nous donne pas de spécification pour les énoncés classiques (c’est-à-dire un résultat établissant le comportement calculatoire commun à toutes les preuves d’un même théorème classique), l’antiréaliste semble fondé à nier que cette extension soit significative : même si elle nous permet de voir les preuves comme des programmes, avec potentiellement un contenu computationnel intéressant, la signification des énoncés reste indéterminée. Nous manquons d’une détermination de ce que font les preuves classiques, dans l’esprit de ce que nous avions pour les preuves intuitionnistes. Le caractère inattendu des programmes qui correspondent à certaines preuves classiques constitue même un argument de plus. Mais tout ceci ne veut pas dire que l’on ne puisse pas déterminer la spécification, mais seulement que déterminer la spécification associée aux théorèmes d’une théorie classique est un problème à part entière. Pour le dire autrement, le passage à la logique classique introduit un élément holiste. On ne peut plus lire la spécification des théorèmes à partir des règles d’introduction des constantes, certes, mais s’il est possible de voir quand même les preuves comme des programmes ayant un bon comportement, l’espoir naît de pouvoir retrouver une explication de ce que font les preuves des théorèmes seulement à partir de la structure syntaxique de ces théorèmes. C’est précisément ce que permet l’application de la réalisabilité au problème de la spécification, telle qu’elle a été développée en particulier par Jean-Louis Krivine (Danos et Krivine [Danos-Krivine 2000], Krivine [Krivine 2003]). Mais n’importe quel résultat de spécification ne conviendra pas pour notre entreprise, il faut préciser ce que l’on exige quand on exige la propriété1 :
nous avons besoin de résultats suffisamment généraux pour servir à une théorie de la signification. Les résultats doivent s’appliquer à tout un langage ou au moins à une partie significative d’un langage. En particulier, cela veut dire que les résultats qui cherchent à exploiter la réalisabilité du point de vue des programmes, pour déterminer comment des classes restreintes de formules peuvent servir à typer des instructions particulières, ne nous sont d’aucune aide ;
nous exigeons la compositionnalité afin de préserver l’approche moléculariste : la spécification doit pouvoir se lire à partir de la structure syntaxique de la formule.
2.3.2 La solution de Krivine pour les théorèmes arithmétiques
36Voyons le résultat de Krivine [Krivine 2003]. En utilisant le λκ-calcul5, Krivine a appliqué les outils de la réalisabilité à l’arithmétique classique du second ordre avec l’axiome du choix dépendant. Chaque énoncé F en forme prénexe est associé à un jeu sémantique GF à deux joueurs, Pet O : l’alternance des quantificateurs définit l’alternance des coups des joueurs ; P choisit un entier pour instancier les quantificateurs existentiels et O choisit pour les quantificateurs universels. Le jeu est asymétrique, au sens où, à tout moment, P peut revenir à une position précédemment atteinte dans le jeu et changer son coup. Le gain est défini de la manière suivante : P gagne si et seulement si il atteint une position terminale gagnante, c’est-à-dire une position correspondant à un énoncé arithmétique sans quantificateur vrai, tandis que O gagne si et seulement si le jeu dure infiniment longtemps (la condition est asymétrique car si l’on arrive sur une position terminale perdante pour P, celui-ci a toujours l’expédient de revenir en arrière). Le résultat de Krivine établit alors que :
il existe une stratégie gagnante sur GF si et seulement si F est vrai dans le modèle standard ;
on peut restreindre les stratégies gagnantes aux stratégies effectives sans perte de généralité (s’il existe une stratégie gagnante, il existe une stratégie gagnante effective),
une preuve de F (précisément, un λµ-terme représentant une preuve de F) est un strategie gagnante sur GF.
37Ainsi, dans le cas particulier d’un énoncé Σ0, le résultat s’énonce précisément comme suit :
38Théorème Si AP2 + ACD + t : ∃x∀yF (x, y), alors t ∗ Tk.π > kn, p ∗ π' avec F (n, p) vraie6.
39La constante k représente ici les coups de O en réponse aux coups de P, la règle de calcul qui lui est associée est ainsi k ∗ sn0.ξ.π >> ξ ∗ sp0.kn,p.π. On voit que le terme t est un programme interactif qui réagit en fonction des coups de O. Une exécution du programme correspond donc au fait de jouer une partie sur le jeu GF : le théorème nous dit que toutes les parties jouées selon la stratégie t sont gagnantes pour P.
40Le réquisit de généralité est bien satisfait : le résultat vaut pour tous les théorèmes arithmétiques, avec cette restriction mineure que seuls les énoncés en forme prénexe sont considérés, mais toute formule est équivalente à une formule en forme prénexe. Le réquisit de compositionnalité est satisfait également, puisque la définition du jeu GF est inductive. Néanmoins, bien sûr, la spécification n’est plus lue à partir des règles d’introduction ; c’est ainsi que se manifeste la réinterprétation globale de la contribution des constantes logiques et mathématiques à la signification des énoncés complexes imposée par l’addition d’une règle classique.
2.3.3 Une théorie de la signification à deux niveaux
41Sommes-nous pour autant fondés à interpréter la spécification associée à un énoncé comme ce dont la connaissance de la signification de cet énoncé devrait être la connaissance ? Écartons tout d’abord l’objection de l’implausibilité psychologique de l’attribution de ce genre de connaissance. Il est évident que le genre d’approche suivi ici ne saurait apporter une explication de notre usage quotidien du mot « signification » appliqué aux énoncés arithmétiques. L’entreprise qui est la nôtre est, dans l’esprit de Dummett, une entreprise de reconstruction ; nous cherchons à rendre compte de la maîtrise d’un langage au sens où quelqu’un qui connaîtrait la théorie de la signification associée à un langage devrait savoir tout ce qui est nécessaire pour que l’on puisse dire de lui qu’il connaît la signification (en un sens cette fois non technique) de toutes les expressions de ce langage.
42Reste à voir si l’on échappe vraiment au dilemme platoniste de Prawitz. La connaissance des conditions de vérité était critiquée pour sa vacuité quand elle n’était pas articulée à une connaissance des conditions de prouvabilité, de sorte qu’une théorie de la signification fondée sur les conditions de vérité était soit redondante soit fausse. Si nous identifions la connaissance de la signification avec la connaissance de la spécification des algorithmes qui nous donneraient le droit de l’asserter7, nous n’aurons pas progressé face au dilemme. En effet, même s’il est question d’algorithmes, de procédures effectives, le réquisit de manifestabilité n’est pas pour autant satisfait. Celui-ci exige que nous soyons capables de reconnaître qu’un algorithme possède la bonne spécification. Que l’on ait réinterprété la connaissance de conditions de vérité en termes de connaissance d’une propriété d’algorithmes ne change rien au problème : nous n’avons pas pour autant de procédure de décision pour faire cela (si nous en avions une, la vérité mathématique serait décidable, car il existe un algorithme simple tel que s’il existe une stratégie gagnante, alors celui-ci correspond à une stratégie gagnante). La seule méthode générale pour montrer qu’un algorithme possède la bonne spécification consiste à le typer, ce qui implique de produire une preuve.
43Connaître la signification d’un énoncé arithmétique serait alors connaître deux choses : d’une part la spécification qui lui est associée, d’autre part le système de preuves permettant de montrer qu’un programme possède bien cette spécification. Au niveau de la spécification, la signification est encore partiellement indéterminée, parce que la propriété « être une stratégie gagnante », exactement comme la « propriété être vrai », dépasse nos capacités de reconnaissance. Mais au seul niveau des preuves formelles et du système de typage, on obtiendrait un concept de signification qui serait trop étroit, parce que l’on peut parfaitement imaginer d’étendre le système de typage avec de nouveaux axiomes, de manière à ce que de nouveaux programmes deviennent typables et que des types cessent d’être vides. La solution proposée consiste donc à articuler les deux composantes du dilemme de Prawitz ; on refuse le dilemme platoniste dans la mesure où on refuse de choisir de choisir entre vérité et preuves, parce que la signification est déterminée par l’interaction entre les deux niveaux de la signification. Notre suggestion consiste alors, semble-t-il, à revenir à la vieille articulation réaliste entre vérité et preuves, selon laquelle les preuves nous donnent accès à des vérités préexistantes ; c’est la thèse défendue, par exemple, par Tarski. La situation n’est pourtant pas si simple. D’une part, le gain réside dans l’interprétation computationnelle des preuves classiques : on est capable de dire ce qu’il faut qu’une preuve classique fasse pour être une preuve d’un certain énoncé. D’autre part, rien ne nous force à admettre des vérités qui soient au-delà de nos capacités de reconnaissance, le premier niveau de la signification rend seulement compte de l’ouverture du système de typage à des additions possibles. Reste que l’écart entre deux types d’algorithmes donnant des stratégies gagnantes, ceux qui sont typables et les autres, reflète bien l’écart entre vérités prouvables et non prouvables.
2.4 L’harmonie, perdue ou retrouvée ?
44Qu’en est-il de l’harmonie ? Dans le cadre de la réalisabilité, il y a quelque chose d’analogue à l’idée de Prawitz de règle dérivée associée à une procédure de justification, c’est le fait que chaque nouvelle règle ou axiome vient avec une nouvelle constante– et sa règle de calcul qui en donne le contenu computationnel. Par conséquent, étant un résultat général de spécification pour une théorie, il y a un sens clair dans lequel un nouvel axiome, par exemple, peut être dit en harmonie avec les anciens, c’est le cas si on peut lui associer une instruction qui soit pour lui un réalisateur ; la validité des règles repose sur une opération. Une instruction convient, si elle donne le théorème d’adéquation qui permet l’application de la méthode de la réalisabilité ; et le théorème de correction des règles relativement à des classes de modèles usuels n’est qu’un cas particulier du théorème d’adéquation en question ; autrement dit, quand on prouve l’adéquation, on prouve bien quelque chose de plus fort que la simple correction ; on prouve que l’instruction associée à la nouvelle règle vit bien avec les anciennes. En particulier, cela veut dire que si l’on avait obtenu un théorème de spécification, le théorème vaudra toujours. En ce sens précis, la nouvelle règle peut être dite en harmonie avec les précédentes. Mais, d’un autre côté, la démonstration d’un théorème d’adéquation met en jeu le même genre de circularité que la démonstration d’un théorème de correction : la question de savoir si cela constitue une objection suffisamment forte pour invalider l’approche proposée de justification de la déduction, qui est dans l’esprit de Dummett et de Prawitz mais qui utilise les résultats sur le contenu computationnel des déductions classiques, demande à être approfondie.
Bibliographie
Des DOI sont automatiquement ajoutés aux références bibliographiques par Bilbo, l’outil d’annotation bibliographique d’OpenEdition. Ces références bibliographiques peuvent être téléchargées dans les formats APA, Chicago et MLA.
Format
- APA
- Chicago
- MLA
Références
[Danos-Krivine 2000] V. Danos et J.-L. Krivine, « Disjunctive Tautologies as Synchronization Schemes », in CSL proceedings, p.292-30, 2000
[Dummett 1978a] M. Dummett, « Philosophical Basis of Intuitionistic Logic », in Truth and Other Enigmas, Harvard University Press, 1978(tr. fr.par F. Pataut in Philosophie de la logique, Editions de Minuit, Paris)
[Dummett 1978b] M. Dummett, « The Justification of Deduction », in Truth and Other Enigmas, Harvard University Press, 1978 (tr. fr.par F. Pataut in Philosophie de la logique, Editions de Minuit, Paris)
[Dummett 1991] M. Dummett, « The Logical Basis of Metaphysics », Harvard University Press, 1991
[Fichot2002] J. Fichot, Langage et signification, Le cas des mathématiques constructives, thèse de doctorat, Université Paris 1, 2002
[Griffin 1990] Th. Griffin, « A Formulae-as-Types Notion of Control », Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL’90, p. 47-57, ACM Press, New York, 1990
[Krivine 1994] J.-L. Krivine, « Classical logic, storage operators and second ordercalculus », in Annals of Pure and Applied Logic, vol. 68, p. 53-78, 1994
10.1016/S0304-3975(02)00776-4 :[Krivine 2003] J.-L. Krivine, « Dependent Choice, ‘quote’ and the Clock », Theoretical Computer Science, vol. 308, p. 259-276, 2003
[Krivine-Parigot 1990] J.-L. Krivine et M. Parigot, « Programming with Proofs », Journal of Information Processing and Cybernetics, vol. 26, n.3, p.149-167, 1990
10.1111/j.1755-2567.1977.tb00776.x :[Prawitz 1976] D. Prawitz, « Meaning and Proofs: On the Conflict Between Classical and Intuitionistic Logic », Theoria, 2-40, 1976
[Parigot 1992] M. Parigot, « Lambda-Mu Calculus : An Algorithmic Interpretation of Classical Natural Deduction », in Proc. of Internat. Conf. on Logic Programming and Automated Deduction, LNCS, vol. 624, n.3, p.190-201, Springer, 1992
[Parigot 1993] M. Parigot, « Classical Proofs as Programs », Lecture Notes in Computer Science, vol. 713, p. 263-276, Springer, 1993
10.1016/S0049-237X(09)70361-1 :[Prawitz 1973] D. Prawitz,« Towards a Foundation of a General Proof Theory », Logic, Methodology and Philosophy of Science, vol. IV, p.225-250, 1973
Notes de bas de page
1 Bien sûr, elle peut être justifiée relativement à la sémantique vériconditonnelle habituelle (théorème de correction), mais les arguments de la section 1.1 ont montré que cette sémantique n’est pas satisfaisante si l’on accepte les réquisits dummettiens sur une théorie de la signification.
2 Néanmoins, ceci est vrai seulement si la disjonction et le quantificateur existentiel ne sont pas pris comme primitifs mais définis de la manière habituelle.
3 Nous adoptons ici la notation de Griffin pour les termes.
4 Si la variable [α] apparaît à d’autres moments, la preuve de droite est dupliquée comme il convient avec des répercussions sur Δ et Δ' éventuellement, de telle sorte que les types restent cohérents.
5 On peut traduire le λκ et le λµ calculs l’un dans l’autre.
6 En fait les quantificateurs doivent être restreints aux entiers afin d’obtenir le résultat. Par ailleurs, T est ici un terme déterminé, qui correspond à un opérateur destockage [Krivine 1994].
7 Autrement dit, dans les termes des jeux sémantiques pour l’arithmétique, connaître la signification d’un énoncé, ce serait simplement connaître ce que doit faire une stratégie gagnante pour le jeu sémantique associé, ce qui revient simplement à savoir quel est le jeu associé.
Auteur
Le texte seul est utilisable sous licence Licence OpenEdition Books. Les autres éléments (illustrations, fichiers annexes importés) sont « Tous droits réservés », sauf mention contraire.
Agir et penser
Essais sur la philosophie d’Elizabeth Anscombe
Valérie Aucouturier et Marc Pavlopoulos (dir.)
2015