P. Martin-Löf a proposé, dès les années 70, de reprendre à nouveaux frais la question du fondement des mathématiques. Il a amélioré la théorie des types de Russell en formalisant une théorie intuitionniste des types, la théorie constructive des types (TCT). Cette théorie a connu plusieurs formes. La dernière date de 1995. La TCT forme un projet ambitieux et très actuel.
Pour une présentation complète de l’histoire de la TCT et de ses aspects philosophiques, nous renvoyons à l’ouvrage exhaustif de G. Sommaruga, History and Philosophy of Constructive Type Theory, ainsi qu’aux ouvrages et articles principaux de Martin-Löf lui-même112. Nous nous contentons de présenter les principes du système de Martin-Löf, de manière à la fois à formaliser une grammaire dans la seconde partie de la thèse, et à apprécier philosophiquement les avantages (et les défauts) de son œuvre. Quelles que soient nos réserves théoriques sur la TCT, il convient de souligner qu’elle forme un système logique apte à fonder les mathématiques sur une base différente de celles du logicisme historique et, croyons- nous, à dépasser les apories de celui-ci. Comme l’œuvre de Lesniewski, avec laquelle elle comporte beaucoup d’affinités, la TCT permet également d’envisager une grammaire pour la langue naturelle, du fait de sa richesse catégorielle113. Nous ne comparons pas ici les deux œuvres, qui marquent à nos yeux une même volonté d’enrichir les catégories de la logique et de repenser de manière radicale les fondements des mathématiques. Nous nous contentons d’une introduction sommaire, mais suffisante cependant pour souligner que la TCT représente une
111
A. Koslow, Op.cit., chapitres 22 et 23.
112
P. Martin-Löf, Intuitionnistic Type Theory, Bibliopolis, Naples, 1984. Pour une bibliographie complète, se reporter aux pages 353-354 de Sommaruga, opus cité.
113
Pour une présentation d’ensemble de l’œuvre de Lesniewski, voir : D. Miéville, Un développement
des Systèmes logiques de Stanislaw Lesniewski. Protothétique-Ontologie-Méréologie, Berne, Peter
Lang, 1984, ainsi que les Travaux de logique du CDRS, Université de Neuchâtel, Introduction à
l’œuvre de S. Lesniewski, Fascicules I-IV, 2003-2006.
Pour la grammaire catégorielle voir notamment: P. Joray, La subordination logique, une étude du nom
logique de la preuve qui allie le PCL et le PCM, et formalise en ce sens le holisme minimal.
La TCT est un système qui comprend des types logiques ; il existe un premier système constructif de type « inférieur », où les types sont identifiés à des ensembles (au sens de la théorie des ensembles), et un second système « supérieur », où les types sont équivalents à des catégories. Une catégorie est définie par la donnée d’un élément quelconque d’un ensemble, et par une règle d’égalité qui définit quand deux objets quelconques sont équivalents. Une catégorie ne forme pas nécessairement un ensemble, mais peut être une proposition, un type de quantificateur, etc.. La notion de catégorie est ainsi plus générale que celle d’ensemble. La TCT d’ordre supérieur comprend donc la TCT d’ordre inférieur. La TCT d’ordre supérieur, mise à part sa plus grande généralité, permet de formuler les règles d’élimination et d’égalité pour le produit cartésien de manière unifiée par rapport aux autres opérations de formation de type114. Elle rend également possible la formalisation d’une grammaire catégorielle servant de base à un langage de programmation115.
La notion de catégorie est définie de manière plus lâche que celle d’ensemble : les règles de formation des catégories ne sont pas exhaustives. En effet, il est possible de comprendre ce qu’est une catégorie sans connaître exhaustivement ses membres. Ainsi, chaque ensemble détermine une catégorie (la catégorie des membres de cet ensemble) mais la converse est fausse. La notion de type représente quant à elle une notion générique: un type est en effet soit une catégorie, soit un ensemble. Selon Martin-Löf, la confusion des deux notions a alors inexorablement mené au paradoxe de Russell. Si un type est défini comme l’ensemble des valeurs possibles d’une fonction propositionnelle, le type est un ensemble. Par contre, si l’on parle de types simples comme les propositions, les propriétés d’individus, etc. (à la différence des types ramifiés qui sont des ensembles), le type forme une catégorie116. Cette distinction entre type et ensemble permet de parler alors sans risque de contradiction de « tous les ensembles », car il s’agit d’une catégorie et non d’un ensemble. Ainsi, cette sémantique typée ne tombe pas sous le coup du paradoxe de Russell du plus grand ensemble.
Il existe une autre distinction essentielle dans la TCT : celle entre proposition et jugement. Une proposition est une phrase vraie ou fausse qui peut être combinée par un opérateur logique (∃, ¬ , ⊃, …). Martin-Löf, comme Frege, utilise le signe de jugement pour signifier qu’une proposition A est jugée comme vraie : ⊢ A. Quant au jugement, il forme une notion logiquement première, parce qu’il permet de préciser quand une proposition est vraie. Les notions de proposition et de vérité dépendent donc de la notion (épistémique) de jugement : elles en sont dérivées. Les prémisses et la conclusion d’une inférence logique représentent des jugements, et non des propositions. Le caractère sémantiquement premier du jugement permet d’expliciter dans un langage-objet ce qui demeure implicite dans le raisonnement mathématique.
114
P. Martin-Löf, Op.cit, introduction.
115
A. Ranta, Type Theoretical Grammar, chapitre 8.
116
P. Martin-Löf, Op.cit., pp. 21-23 ; là aussi, une comparaison systématique avec l’analyse par Lesniewski du paradoxe des ensembles et des fonctions propositionnelles chez Russell s’imposerait.
De même, en TCT, la vérité des propositions est explicitée par des règles de formation, comme :
A prop. B prop. A vraie A ∨ B vraie
Une telle règle spécifie à la fois que A et B sont des propositions, et que l’on peut inférer de la vérité de A que A ou B sont vraies.
La vérité de A peut aussi se formaliser par un signe de jugement:
⊢ A. Ainsi, en
TCT, les jugements sont totalement explicités dans le langage-objet (et non laissés implicites dans le métalangage, comme ils le sont chez Gentzen). Par ailleurs, la TCT comporte quatre formes fondamentales de jugements :(1) A est un ensemble.
(2) A et B sont des ensembles égaux.
(3) a est un élément de l’ensemble A (a ∈A).
(4) a et b sont des éléments égaux de l’ensemble A (a=b ∈ A).
Dans la TCT de type inférieur, les ensembles sont identifiés à des propositions. La règle (3) signifie que l’ensemble a est non vide et/ou qu’il existe une preuve de A. (1) peut se lire aussi comme « A est une intention » et (3) comme « a est une méthode de réalisation de l’intention A ».
Si l’on assume l’hypothèse que A représente un ensemble, alors la première forme de jugement prend la forme hypothétique « B(x) ensemble (x∈A) », qui signifie que B(x) est un ensemble sous l’hypothèse que x∈A, c’est-à-dire que B(x) forme une famille d’ensembles sur A. L’hypothèse déchargée dans la déduction est notée entre parenthèses ; ces recommandations permettent de formuler la règle de substitution suivante :
(x ∈A)
a∈ A B(x) ensemble B (a) ensemble
Un tel jugement peut se lire comme « B (a) est un ensemble si a est un élément de A ». Il en va de même pour la deuxième forme de jugement qui spécifie que B (a) et B(c) sont des ensembles égaux si et seulement si a et c sont des éléments égaux de A.
Martin-Löf généralise par ailleurs la notion de jugement hypothétique de manière à inclure un nombre arbitraire n de jugements. Le sens des jugements en contexte multiple (sous plusieurs hypothèses) se fait par induction sur le sens préalablement déterminé de n-1 hypothèses. Faisons donc l’hypothèse que :
A1 est un ensemble,
A2(x1) est une famille d’ensembles sur A1x2,
A3(x1, x2) est une famille d’ensembles avec deux indices x1∈A1 et x2∈A2(x1), …,
xn-1∈An-1(x1, …, xn-2),
…
An(x1, …, xn-1) est une famille d’ensembles avec n-1 indices x1∈A1, x2∈ A2(x1),
… xn-1∈ An-1(x1,…, xn-2).
Un jugement sous n-1 hypothèses prend la forme suivante :
A(x1,…, xn ) ensemble (x1∈a1, x2∈A2(x1),…, xn ∈An(x1, …, xn-1))
Un tel jugement signifie alors que A (a1, …, an) est un ensemble si et seulement si
a1∈A1, a2∈ A2 (a1), …, an∈ An (a1, …, an-1).
Ainsi, le jugement A(x1, …, xn) détermine une famille d’ensembles avec n indices.
Les n-1 hypothèses dans un tel jugement forment ce que Martin-Löf appelle un contexte (Γ).
Cette procédure « pas à pas » ressemble au contexte des hypothèses de Gentzen. Mais le contexte est ici tout à fait explicite et intégré au langage-objet, ce qui n’est pas le cas chez Gentzen. Par ailleurs, la formalisation sémantique des contextes donne ipso facto une interprétation contextuelle des constantes, de telle manière que l’introduction d’une constante introduise en même temps un contexte de preuves.
Par ailleurs, la TCT comprend quatre genres de règles pour chaque opération : la formation de l’ensemble, les règles d’introduction, celles d’élimination, celles d’égalité. Les règles de formation assurent qu’il est légitime de former un ensemble (ou une proposition) à partir de certains autres ensembles (ou propositions). Les règles d’introduction définissent des éléments canoniques de l’ensemble (et les éléments canoniques égaux). Les règles d’égalité relient les règles d’introduction et les règles d’élimination entre elles en montrant comment une fonction peut être définie par la règle d’élimination. A chaque règle relative aux ensembles correspond donc une règle pour l’égalité des ensembles et de leurs éléments. Les règles de formation sont utilisées pour formaliser des propositions, les règles d’introduction et d’élimination correspondent aux règles de Gentzen, et les règles d’égalité aux règles de réduction de Prawitz-Dummett. Ces règles sont inanalysables au sens où elles relèvent en dernière analyse d’intuitions.
Löf défend donc une forme cartésienne de la signification, qui est relative à l’intuition que l’on peut avoir des règles logiques :
(…) in the end, no explanation can substitute each individual’s understanding117.
Puis Martin-Löf définit les quantificateurs universel et existentiel sur la base du produit cartésien de deux ensembles. Sa définition est particulièrement intéressante. D’une part, elle formalise une contextualisation des quantificateurs, qui introduisent à chaque fois des contextes. D’autre part, ces quantificateurs définissent des variables dépendantes, comme en tant que A ou en tant que B, ce qui est particulièrement utile en grammaire pour déterminer la sémantique des pronoms de reprise de termes quantifiés.
Etant donnés un ensemble A et une famille d’ensembles B(x) sur l’ensemble A, on peut alors définir un produit cartésien :
Π- formation :
(x∈A) A ens B(x) ens (Πx ∈ A) B(x) ens
Cette règle assure que quelque chose est bien un ensemble. Pour savoir de quel ensemble il s’agit, il est nécessaire de définir les éléments canoniques de cet ensemble au moyen de la règle d’introduction suivante :
Π- introduction :
(x∈A) b(x)∈B(x)
(λx) b(x) ∈(Πx ∈ A) B(x)
Löf définit également BA≡ A→B≡ (Πx∈A) B par une règle d’égalité. Cela permet d’interpréter les ensembles comme des propositions et de donner les règles de formation, d’introduction et d’élimination des quantificateurs universel et existentiel (∀ et ∃). La règle d’élimination de Π (avec une règle d’application) permet de déterminer un élément canonique de B(a) :
Π- élimination :
c ∈(Πx∈A) B(x) a∈A Ap (c, a) ∈ B (a)
La constante d’application Ap s’explique ainsi : Ap(c, a) est une méthode pour obtenir un élément canonique de B (a). Pour exécuter cette méthode, il est nécessaire de procéder ainsi : si c ∈(Πx ∈A) B(x), c’est-à-dire si c est une preuve de (Πx∈A) B(x), alors c est une méthode qui donne l’élément canonique (λx) b(x) de (Πx∈A) B(x) comme résultat. On prend alors a∈A et on le substitue à x dans b(x), ce qui donne b (a) ∈ B(A) ; puis, en calculant b(a), on obtient un élément canonique de
117
B(a). Il ne s’agit pas en l’occurrence d’un calcul effectif, mais d’un schéma de calcul. La constante Ap correspond à la règle (ca) de la logique combinatoire.
Si B(x) est une fonction propositionnelle, on peut former le quantificateur universel, soit :
∀- formation :
(x ∈ A) A ens B(x) prop (∀x ∈A) B(x) prop
Cette règle assure que la quantification universelle forme des propositions. Elle porte sur l’ensemble A comme domaine de quantification. Elle forme une instance de la règle de formation de « Π », c’est-à-dire une interprétation propositionnelle de la règle de formation sur les ensembles. Quant à la règle d’introduction du quantificateur universel, elle est la suivante :
∀-introduction :
(x∈A) B(x) vraie (∀x ∈A) B(x) vraie,
Cette règle d’introduction du quantificateur universel est obtenue par la suppression de la règle b(x). Comme il est ici question de propositions, on n’explicite pas le fait que a est élément de A, mais uniquement que a est vraie et que A est une proposition. En ce qui concerne l’élimination du quantificateur universel, nous avons :
∀-élimination :
a∈A (∀x ∈A) B(x) vraie B (a) vraie
Cette règle revient à affirmer, en restaurant les preuves, que si c est une preuve de (∀x∈A) B(x), alors Ap(c, a) est une preuve de B (a). Une preuve de (∀x∈A) B(x) est donc définie comme une méthode qui prend un élément arbitraire (ou quelconque) de A dans une preuve de B (a). Ainsi, la règle d’élimination du quantificateur universel en TCT s’accorde avec l’interprétation intuitionniste de la quantification, car elle n’a de sens que par la donnée des éléments du domaine de quantification, et non pas sur l’univers indéterminé de toutes les valeurs. La quantification universelle permet quant à elle de définir la conjonction logique:
A ⊃ B ≡ A→ B ≡ BA ≡ (Πx ∈ A) B où B ne dépend pas de x.
Une telle définition signifie que si nous sommes en situation de juger que B est un problème sous la condition expresse que le problème A a été résolu, ou qu’il peut l’être à un « moment » du système, cela est suffisant pour que le problème « A ⊃ B » fasse sens. Par son caractère contextuel, la TCT formalise l’interprétation de Kolmogorov des constantes en termes de « problèmes à résoudre ». Elle permet d’en rendre compte en construisant les propositions sur des ensembles à l’aide
d’opérations sur le produit cartésien. Ainsi, le quantificateur universel et la conditionnelle représentent deux interprétations différentes de l’opérateur « Π ». Une telle approche n’est pas absolument nouvelle par rapport à celle de Gentzen ou celle de Dummett, mais sa force réside dans sa capacité de formalisation des contextes sémantiques dans un langage interprété. En un mot, la TCT rend compte du sens en contexte.
Le deuxième groupe de règles concerne l’union disjointe d’une famille d’ensembles. Cette union se note ainsi :
Σ-formation :
(x ∈A) A ens B(x) ens (Σx ∈ A) B(x) ens
Une fois encore, Martin-Löf explique le sens de l’ensemble formé par la formation de ses éléments canoniques (avec la règle d’introduction) :
Σ- introduction :
a∈A b∈B(a) (a, b) ∈(Σx ∈A) B(x)
(La règle d’élimination s’explique par l’introduction d’une constante E et par l’obtention d’un élément canonique « e », élément de C(c))118.
L’union disjointe de deux ensembles permet alors de définir le quantificateur existentiel :
(∃ x ∈ A) B(x) ≡ (Σx ∈A) B(x)
Avec B(x) interprétée comme une fonction propositionnelle sur A , on obtient les deux règles suivantes:
∃-formation :
(x∈A) A ens B(x) prop (∃x ∈A) B(x) prop ∃-introduction :
a∈A B(a) vraie (∃x ∈A) B(x) vraie
Cette règle d’introduction détermine qu’une preuve canonique de (∃x∈A) B(x) est une paire (a, b) où b est une preuve que a satisfait B ; elle donne un sens intuitionniste à l’existence d’un a qui satisfait B(x), en termes de preuve effective de son existence. Le résultat de la preuve, que Löf appelle une preuve-objet, est une proposition vraie qui correspond aux réquisits de sa preuve considérée comme processus.
118
Par ailleurs, le produit disjoint donne les règles de la conjonction par la définition suivante :
A ∧ B ≡ A × B ≡ (Σx ∈A) B où B ne dépend pas de x.
Les règles de la conjonction sont des instances de la règle de formation de Σ : ∧-formation : (A vraie) A prop B prop A ∧ B prop ∧- introduction : A vraie B vraie A ∧ B vraie ∧-élimination : (A vraie, B vraie) A ∧ B vraie C vraie C vraie
Avec C= A et B, on obtient alors les règles standard de l’élimination de la conjonction.
Ce qui est particulièrement intéressant ici, c’est qu’à partir d’une preuve de (∃x ∈A) B(x), il est possible d’obtenir un élément de A pour lequel B vaut par une règle de projection (à gauche en l’occurrence). Soit :
Projection à gauche : c∈(∃x ∈A) B(x) p(c) ∈ A Projection à droite : c∈(∃x ∈ A) B(x) q (c) ∈B (p(c))
Une telle projection à droite est construite à partir de la donnée préalable de la projection à gauche.
De telles règles de projection sont essentielles à un traitement compositionnel des pronoms car elles permettent de définir un élément de A qui satisfait B, comme « l’âne qui est battu » à partir de la preuve c de « tout fermier qui possède un âne », nous le verrons plus en détail peu après.
En conséquence, la compositionnalité de la TCT est assurée par les règles de formation des constantes qui déterminent comment les propositions complexes sont formées à partir de leurs constituants simples. Par ailleurs, la TCT formalise les règles de Gentzen comme des abréviations de preuves complètes, preuves qui comprennent des preuves-objets, c’est-à-dire les résultats des processus de preuve.
Par exemple, la règle d’introduction de Gentzen se formule ainsi : A vraie B vraie
A ∧ B vraie
La preuve complète donnée en TCT présuppose la règle de formation suivante : a : A b : B
(a, b) A ∧ B
Ces règles explicitent parfaitement la vérité intuitionniste de la conjonction : l’introduction de la conjonction de A et de B présuppose non seulement que A et B soient vraies mais aussi que nous avons prouvé qu’elles le sont (« a » est une preuve de A dans la règle de formation). La signification présuppose l’évidence : il est nécessaire, en effet, de disposer d’une preuve de A et de B pour introduire la conjonction logique de manière légitime. Cette preuve se base en dernier ressort sur l’évidence que les propositions A et que B sont vraies. Une telle analyse implique les considérations suivantes:
La notion intuitionniste de vérité d’une proposition est subordonnée à la notion de déduction de cette proposition : connaître une proposition comme vraie revient à connaître une preuve de cette proposition (directe ou indirecte). Une preuve indirecte consiste quant à elle à savoir comment construire une preuve directe de la proposition, c’est-à-dire à connaître l’action qu’il est nécessaire d’accomplir pour obtenir une évidence. Par ailleurs, d’une manière générale, la connaissance de la vérité d’une proposition est identique à la démonstration directe de cette proposition. En TCT, la vérité présuppose ainsi la possibilité de la reconnaissance du vrai comme tel ; une telle subordination du vrai à la démonstration définit l’intuitionnisme comme un anti-réalisme sémantique.
En outre, un jugement est le résultat d’une preuve : juger que A est vraie revient à prouver que a : A, c’est-à-dire que a est une preuve de A ; le jugement représente alors l’objet d’un acte de connaissance; la preuve d’un jugement consiste alors dans l’évidence de la vérité de celui-ci. L’objet intuitionniste d’une connaissance est identique à ce que l’on prouve, c’est-à-dire à un jugement119. Une telle analyse des notions de vérité et de jugement ne va pas sans poser problème. Nous y reviendrons au chapitre 3.2 du présent travail.
Enfin, nous avons vu que la conjonction et la quantification logiques sont des cas particuliers de l’opérateur d’union disjointe « Σ », alors que l’implication et la quantification universelle sont des cas particuliers de l’opérateur produit « Π ». Considérons, en effet, la règle d’introduction du jugement de quantification existentielle :
a : A B(a) est vraie (Σ x A) B(x) est vraie
119
P. Martin-Löf, « Truth of a Proposition, Evidence of a Judgement, Validity of a Proof », Synthese
Une telle règle donne une explication intuitionniste de l’existence ; « quelque A est B » est jugé de manière justifiée si et seulement s’il existe une paire (a, b) de preuves, c’est-à-dire une preuve a de A et une preuve b du fait que a satisfait la fonction propositionnelle B(x). Autrement dit, la proposition « Quelque A est B » ne peut être jugée de manière correcte que dans un contexte formé de la donnée de l’ensemble A d’une part, et d’une preuve de l’existence d’au moins un A satisfaisant B(x), d’autre part. Il existe ainsi, en TCT, une dépendance fonctionnelle entre le type B et le type A : B dépend sémantiquement de A, qui lui sert de contexte. Une proposition est ainsi toujours jugée en contexte, et les règles d’introduction introduisent ipso facto un contexte.
La compréhension d’une proposition équivaut donc à la saisie de sa vérité par l’intermédiaire d’une preuve. Ainsi, la preuve et le jugement ne concernent pas un univers absolu de valeurs à la Frege, mais un contexte sémantique construit à l’aide d’une réitération d’hypothèses. La TCT offre donc une manière holiste de rendre compte de la preuve, tout en assurant la compositionnalité du langage à l’aide des règles explicites de formation des constantes.
En résumé, la TCT forme un système de la dépendance sémantique des types entre eux. Elle construit en effet des ensembles enchâssés de contextes à l’aide de types logiques successifs qui dépendent les uns des autres. Une telle approche contextuelle apparente les formalisations de la TCT à la progressivité d’un discours dans lequel l’étape discursive n dépend de la compréhension des étapes n-1. Elle formalise la notion d’une proposition en contexte grâce à la dépendance de cette proposition comprenant n variables vis-à-vis de n-1 variables données inductivement. Cette capacité holiste de la TCT permet la formalisation de la sémantique essentiellement contextuelle des pronoms anaphoriques (voir 2.5 du présent travail). Sur ce point la TCT est donc bien supérieure au molécularisme de Dummett qui, nous l’avons vu, ne cesse de minimiser l’importance de la dépendance sémantique et cherche à réduire un texte à une succession de phrases dont le sens est indépendant. En conséquence de quoi, Dummett affirme sans sourciller qu’il est