Cela fait un certain temps que je me dis que je devrais écrire une
ou plusieurs entrées sur ce blog sur des sujets tournant autour de la
logique intuitionniste et des mathématiques constructives. La
présente entrée est une sorte de TODO étendu
où je mélange, de façon malheureusement confuse et désorganisée, des
remarques introductives voire vulgarisatrices sur le sujet (et
expliquant de quoi il est question), des remarques d'ordre méta
(où je dis que je devrais parler de ceci ou de cela, ou bien me
demande comment je pourrais le faire, ou encore me dis que je ne
comprends pas bien telle ou telle chose) et des explications de fond
assez disparates (et faites à des niveaux de prérequis, il faut bien
le dire, complètement incohérents). Même l'ordre dans lequel je dis
les choses est assez bizarre (à la limite, je me demande s'il ne vaut
pas mieux lire cette entrée en commençant par la fin). Je pense que
ça vaut quand même la peine de publier tout ça, en conseillant au
lecteur de simplement sauter les passages qui lui semblent obscurs
(puisque de toute façon il y a très peu de dépendances dans ce que je
vais raconter).
★
En fait, au départ, je me suis surtout dit que ce serait intéressant d'écrire quelque chose sur le topos effectif et la réalisabilité de Kleene. Je peux au moins recopier l'introduction informelle que j'ai commencé à rédiger à ce sujet :
Pour dire très très très sommairement et très très très vaguement de quoi il est question,
- un
toposest une sorte de « monde mathématique alternatif » régi par les lois de la logique intuitionniste (une logique plus faible que la logique usuelle, ou classique, dans laquelle on a essentiellement supprimé la loi du tiers exclu qui affirme que toute formule logique est soit vraie soit fausse, ou, de façon équivalente, que tout ce qui n'est pas faux est vrai) ; de façon un peu plus précise, un topos est une catégorie (peu importe ce qu'est exactement une « catégorie ») qui possède un certain nombre de propriétés communes avec la catégorie des ensembles, ce qui permet d'y mener un certain nombre de constructions mathématiques usuelles, mais dont le comportement va néanmoins être différent sur un certain nombre de choses, et notamment la logique ; et- le
topos effectifest un topos particulier qui présente un intérêt particulier en calculabilité : il présente un monde alternatif dans lequel toutes les fonctions ℕ→ℕ sont calculables, ce qui nous offre un regard neuf sur la calculabilité par rapport à sa présentation classique, où la logique intuitionniste éclaire ce que sont les raisonnements effectifs (voir à ce sujet cet article introductif d'Andrej Bauer, qui ne parle pas du topos effectif mais explique en quoi travailler en logique intuitionniste peut rendre plus facile ou plus naturelle la calculabilité).
Mais reculons d'un cran : pour parler du topos effectif, je me suis dit qu'il fallait d'abord que j'écrive quelque chose sur la réalisabilité de Kleene, qui en est en quelque sorte le prélude. (Si vous voulez savoir très très très sommairement et très très très vaguement de quoi il est question, S. C. Kleene a introduit dès 1945 une notion appelée « réalisabilité », en tentant de donner un sens précis à l'intuitionnisme, et — en très très très gros — le fait qu'une formule arithmétique φ soit « réalisable » [par un entier naturel n] signifie que n en apporte une sorte de « témoignage algorithmique », par exemple, si φ est une formule du type ∀x.ψ(x) affirmant que ψ(x) est vraie pour tout x, alors « réaliser » cette formule va se faire en apportant un programme qui prend en entrée un entier k et en sortie calcule un entier qui réalise ψ(k) ; pour un peu plus de détails, voir le début de cette question que j'ai posée sur MathOverflow, ou pour encore plus, voir le texte Realizability: An [sic] Historical Essay de Jaap van Oosten.) Le lien entre la réalisabilité de Kleene et le topos effectif est très fort : disons que le topos effectif est défini en cherchant une généralisation assez directe de la réalisabilité à des formules plus complexes que celles de l'arithmétique (et les formules arithmétiques qui sont réalisables sont exactement celles qui sont vraies dans le topos effectif).
Ajout : voir cette entrée ultérieure au sujet de la réalisabilité, où je la définis proprement. Nouvel ajout : le billet sur le topos effectif est ici.
Bon, mais je me suis alors rendu compte que ce serait commencer in media res de parler du topos effectif ou même de réalisabilité si je ne commençais pas par parler d'intuitionnisme ou de mathématiques constructives. Et là, je suis embêté par le fait que j'ai à la fois trop de choses à dire et pas assez (trop, parce que ça touche à énormément de sujets ; pas assez, parce qu'en ce faisant ça touche aussi à trop de questions sur lesquelles je ne sais pas grand-chose).
Ajout : ce nouveau billet est une tentative de réécriture complète de celui qui suit, et il est peut-être plus clair (ou peut-être que les deux s'éclairent l'un l'autre, je ne sais pas).
★
La logique intuitionniste est une logique plus faible que la
logique classique dans laquelle on s'interdit la loi du tiers exclu
(qui dit que tout énoncé P est soit vrai soit faux ;
c'est-à-dire : P∨¬P) ; cela revient
essentiellement à s'interdire le raisonnement par l'absurde (ou plus
exactement, le raisonnement par l'absurde de la forme je veux
montrer P : supposons par l'absurde que P soit
faux <…>, j'arrive à une contradiction, donc P ne
peut pas être faux, c'est-à-dire qu'il est vrai
— c'est la
dernière partie qui coince en logique intuitionniste ; en revanche, on
peut toujours dire je veux montrer que P est faux :
supposons par l'absurde que P soit vrai <…>, j'arrive
à une contradiction, c'est-à-dire que P est faux
, parce
que P est faux
signifie précisément que la vérité
de P est absurde). Faire des maths sans le tiers exclu
peut ressembler à un exercice aussi futile qu'essayer de boxer avec
les deux mains attachées derrière le dos, et dans une certaine mesure
ça y ressemble effectivement, mais cela présente néanmoins un certain
intérêt : non seulement c'est intéressant du point de vue de la pure
logique de se demander ce qu'on peut faire sans cet axiome (et cette
question a des connexions inattendue avec toutes sortes d'autres
parties des mathématiques) ; mais par ailleurs, une démonstration en
logique intuitionniste apporte véritablement plus de contenu qu'une
démonstration classique : pour commencer, elle est valable de façon
plus large (et notamment dans les topoï [pluriel
de topos
]), mais aussi, elle est constructive (au
moins si on part de certains axiomes), c'est-à-dire qu'elle exhibe les
objets dont elle affirme l'existence.
Une des idées centrales des maths constructives (qui sont à peu
près, quoique pas forcément exactement, la même chose que les
mathématiques exercées dans le cadre de la logique intuitionniste) est
que si on veut prouver P ou Q
(en
symboles, P∨Q), il devrait être
suffisant mais aussi nécessaire de prouver soit P,
soit Q (et notamment, de savoir lequel des deux est
vrai !) : ceci va manifestement complètement à l'encontre du tiers
exclu qui postule que pour tout énoncé P,
soit P est vrai soit ¬P l'est, sans qu'on puisse
forcément trancher lequel (et parfois, effectivement, on ne peut
prouver ni l'un ni l'autre). De même, si on veut prouver il existe
un x tel que P(x)
(en symboles,
∃x.P(x)), il devrait être
suffisant mais aussi nécessaire d'exhiber un x
pour lequel on peut prouver P(x) : de nouveau,
ceci va à l'encontre des raisonnements par l'absurde qui ressemblent
à supposons qu'aucun tel x n'existe <…>, j'arrive
à une contradiction, donc un tel x doit exister
(mais
au final ne donnent aucune information pour en construire un).
Ajout () : Juste après avoir publié cette entrée je me rends compte que j'ai oublié d'insérer un paragraphe que je comptais écrire sur l'interprétation de Brouwer-Heyting-Kolmogorov qui tente d'expliquer au moins informellement le sens des connecteurs de la logique intuitionniste. Spécifiquement, il s'agit de variations autour des explications suivantes :
- une preuve de P∧Q (conjonction) est un couple formé d'une preuve de P et d'une de Q,
- une preuve de P∨Q (disjonction) est la donnée d'une preuve de P ou d'une preuve de Q (avec, bien sûr, l'information de laquelle des deux),
- une preuve de P⇒Q (implication) est une manière de transformer une preuve de P en une preuve de Q,
- une preuve de ⊤ (le vrai) est triviale,
- une preuve de ⊥ (le faux) n'existe pas,
- une preuve de ∀x.P(x) est une manière de transformer un x en une preuve de P(x),
- une preuve de ∃x.P(x) est la donnée d'un t particulier et d'une preuve de P(t).
Je répète que, telles quelles, ces explications n'ont pas vraiment
de sens (notamment à cause des mots manière de transformer
), et
d'ailleurs il en existe beaucoup de variations (Kolmogorov parlait
de problèmes
et de solutions
de ces problèmes plutôt que
de preuves d'énoncés ; c'est d'ailleurs ce qui motive la logique de
Medvedev dont je parlerai plus bas). Mais elles servent au moins à
motiver la manière dont on veut que la logique intuitionniste
se comporte, et ce sont des formalisations de ces idées qui conduisent
à la réalisabilité de Kleene (ce dernier essayait de rendre précise
l'interprétation de Brouwer-Heyting-Kolmogorov) et la logique de
Medvedev (cf. plus loin).
★
Je ne suis pas historien des maths et pas spécialement compétent
pour en parler, et par ailleurs l'article Wikipédia sur
la controverse
Hilbert-Brouwer me semble bizarrement écrit et lui-même sujet à
controverse ; donc je ne tenterai pas sérieusement de faire l'histoire
du sujet. Ce
que L. E. J. Brouwer,
inventeur de l'intuitionnisme, appelait intuitionnisme
, n'est
pas vraiment ce que les matheux actuels appellent ainsi (notamment
parce que je crois comprendre que Brouwer avait une grande méfiance de
la logique, et plus encore de la logique formelle, alors que
maintenant — depuis Gödel, il me semble — on considère tout ce sujet à
la lumière de la logique), mais le tiers exclu est assurément un point
central d'achoppement entre Brouwer, qui le rejetait pour son
caractère non-constructif, et Hilbert, qui l'acceptait comme une
évidence de l'orthodoxie logique. Ironiquement, la controverse est
partiellement due à deux théorèmes d'existence non-constructifs dus à
Hilbert et Brouwer eux-mêmes, à savoir
le théorème
de la base de Hilbert (dont la recherche d'une démonstration
constructive a cependant mené indirectement à la théorie des bases de
Gröbner) et
le théorème
du point fixe de Brouwer.
Mais pour donner peut-être une saveur de [hum, comment on
dit a taste of
en français, déjà ?] choses qui
pouvaient déranger Brouwer, je peux proposer l'exemple de raisonnement
suivant, qui me semble intéressant parce qu'un de mes collègues,
pourtant informatheux expérimenté, a été vraiment dérangé par cet
argument avant de concéder qu'il était valable :
Contexte : On ignore, actuellement, essentiellement tout sur l'écriture décimale de π (à part qu'elle n'est pas ultimement périodique puisque π n'est pas rationnel). On ne sait, notamment, pas prouver que chaque chiffre ou à plus forte raison chaque suite finie de chiffres, y apparaît infiniment souvent, et on ne sait même pas le prouver pour un chiffre ou une suite finie particulière de chiffres. On conjecture cependant que les décimales de π se comportent, pour ce genre de choses, essentiellement comme si elles étaient tirées au hasard, c'est-à-dire que chaque suite finie de longueur r apparaît en moyenne une fois toutes les 10r décimales (et notamment, infiniment souvent). Je ne fais aucune hypothèse particulière sur les décimales de π dans ce qui suit (et vous pouvez le remplacer par le nombre réel calculable de votre choix).
Affirmation : Il existe un programme qui, donné un entier k en entrée, termine toujours en temps fini et renvoie soit l'emplacement de la première occurrence de k fois consécutivement le chiffre 7 dans l'écriture décimale de π, soit
faux(ou∞si on préfère) si une telle occurrence n'existe pas.Preuve : Soit f: ℕ → ℕ∪{∞} la fonction qui à k associe l'emplacement de la première occurrence de k chiffres 7 consécutifs dans l'écriture décimale de π, ou bien ∞ si cette occurrence n'existe pas. Il s'agit de montrer que cette fonction f est calculable algorithmiquement. De deux choses l'une : soit il existe k₀ tel que f(k)=∞ pour k≥k₀ (i.e., k₀−1 est la longueur de la plus grande suite de 7 consécutifs dans π) ; soit f(k)<∞ pour tout k. Dans le premier cas, la fonction f est calculable algorithmiquement par un programme puisqu'elle est constante à partir d'un certain rang (le programme peut renvoyer ∞ pour k≥k₀ et faire un nombre fini de cas pour toutes les valeurs inférieures) ; dans le second cas, il existe des suites de 7 consécutifs arbitrairement longues, et f est calculable par le programme qui calcule toutes les décimales successivement jusqu'à trouver une telle suite de longueur assez grande.
Commentaire : Ce qui rend ce raisonnement gênant est que beaucoup de gens (dont le collègue évoqué ci-dessus) vont rétorquer
oui, mais on ne sait pas calculer k₀, ni même s'il existe !— pourtant, ce raisonnement, qui ferait sans doute frémir d'horreur Brouwer, est classiquement correct, c'est-à-dire correct dans la théorie de la calculabilité enseignée dans le cadre des mathématiques usuelles (classiques, orthodoxes, comme vous voudrez l'appeler). Le problème est que je montre que quelque chose est calculable (qu'un programme pour le calculer existe) sans exhiber un tel programme : quelle que soit la valeur de k₀ (ou si k₀ n'existe pas), un tel programme existe, mais moi je ne sais pas ce qu'il est. Seulement, classiquement,f est calculablesignifie qu'un programme calculant f existe, pas que je suis capable de l'exhiber. (Bon, on peut quand même se mettre d'accord que la convention usuelle de langage, en l'absence d'éclaircissement par ailleurs, quand on ditf est calculableest qu'en fait non seulement f est calculable mais qu'on s'apprête à en exhiber un algorithme explicite ; mais c'est déjà une forme de constructivisme.)
★
Maintenant, faire des maths en logique intuitionniste ressemble effectivement un peu à faire de la boxe sans utiliser ses poings (la comparaison est de Hilbert) : un matheux habitué aux maths classiques sera horrifié de ne pas avoir le droit de dire que, si x est un réel, on a soit x>0 soit x<0 soit x=0 ; ou qu'une partie d'un ensemble fini est finie ; ou que l'image d'un ensemble fini est finie ; ou toutes sortes de choses de ce genre. Pourtant, on peut quand même faire beaucoup de maths, et de façon même pas si différente de ce dont on a l'habitude : c'est quelque chose qu'E. Bishop et ses disciples ont montré (constructivement !).
À part l'aspect scientifique proprement dit, je suis tenté de
trouver que ça a un réel intérêt pédagogique
(voire métapédagogique, i.e., pour enseigner la pédagogie) :
en obligeant à se rendre compte de la manière dont on utilise le tiers
exclu (et à chercher à l'éviter), cela amène à réfléchir à la manière
dont on construit des raisonnements mathématiques (et dont toutes
sortes de faits « évidents » comme si tous les éléments d'un
ensemble sont égaux alors il existe un élément auquel ils sont tous
égaux
sont démontrés) ; cela peut aussi amener le mathématicien
classique, en le plaçant sur un terrain non familier et glissant pour
lui, à reréfléchir à ce qu'il trouve évident, et peut-être à mieux
comprendre les étudiants et autres débutants en mathématiques en
comprenant leurs difficultés. Je pense d'ailleurs un peu la même
chose du fait de s'obliger à repérer ou à éviter l'usage de l'axiome
du choix
(cf. d'ailleurs cette
question sur la comparaison entre les deux) ou d'autres axiomes de
la théorie des ensembles (Remplacement me vient à l'esprit).
En fait, ce qui est peut-être remarquable, c'est qu'on s'habitue relativement vite à raisonner en logique intuitionniste, et notamment, que même les matheux qui ne connaissent pas la logique formelle comprennent ce que cela signifie que de s'interdire le tiers exclu (alors qu'on pourrait se dire a priori que cela dépend du mécanisme mental précis qu'ils ont en tête pour représenter la logique classique).
(Cf. aussi cette entrée passée qui a un rapport avec le sujet.)
★
Pour la complétude de cette entrée (enfin, pour faire semblant), je vais quand même lister ici rapidement des règles permettant de définir la logique intuitionniste, un peu à la manière de celles que j'ai utilisées pour définir la logique linéaire dans cette entrée (même si cette présentation n'est peut-être pas la plus logique pour le genre de sujets que je veux évoquer concernant la logique intuitionniste ; et même si je répète qu'en fait, Brouwer avait horreur de la logique formelle et que quand on ouvre un livre tel que ceux de Bishop, il commence directement à faire des maths sans essayer d'expliquer formellement les règles — ce sont plutôt les informaticiens qui aiment ce genre de formalisme).
Comme dans mes règles pour la logique linéaire, j'introduis un
symbole supplémentaire, qui ne fait pas partie de la logique
elle-même mais sert à la définir : il s'agit du symbole ‘⊢’
(prononcé thèse
ou taquet
), mais une différence avec la
logique linéaire (ou classique) est que les séquents sont asymétriques
gauche-droite, ils sont de la forme Γ⊢P
où Γ est une suite (finie) quelconque de (zéro ou plus)
formules séparées par des virgules (les antécédents
ou hypothèses du séquent) et P est
une unique formule (le conséquent ou
la conclusion du séquent). Dans les règles qui suivent, les
lettres latines majuscules (A,B,C…)
sont à remplacer par des formules quelconques de la logique
intuitionniste, et les lettres grecques majuscules
(Γ,Σ) par des suites (finies) quelconques de
formules séparées par des virgules (ces formules-là, ainsi que celles
que j'ai dénoté par la lettre P, ne seront pas modifiées et
portent le nom collectif de contexte d'application de la
règle — enfin, peut-être que P mériterait plutôt le nom
de continuation) :
- Coupure : si Γ⊢A [est un séquent valable] et A,Σ⊢P [en est un], alors Γ,Σ⊢P [en est encore un].
- Identité : on a A⊢A [c'est un séquent valable].
- Échange : si Γ⊢P alors Γ′⊢P où Γ′ s'obtient en permutant de façon arbitraire les formules de Γ. (Remarque : on peut passer complètement sous silence l'utilisation de la règle d'échange en considérant que la liste à gauche du symbole taquet, dans un séquent, est un multiensemble, c'est-à-dire que son ordre n'est tout simplement pas défini.)
- Affaiblissement : si Γ⊢P alors Γ,A⊢P ; contraction : si Γ,A,A⊢P alors Γ,A⊢P.
- Introduction du ∧ : si Γ⊢A et Σ⊢B, alors Γ,Σ⊢A∧B ; élimination du ∧ : si Γ,A,B⊢P alors Γ,A∧B⊢P.
- Introduction du ∨ : si Γ⊢A ou bien Γ⊢B alors Γ⊢A∨B ; élimination du ∨ : si Γ,A⊢P et Γ,B⊢P, alors Γ,A∨B⊢P.
- Introduction du ⊤ : on a ⊢⊤ ; élimination du ⊤ : si Γ⊢P alors Γ,⊤⊢P (remarque : ceci est redondant avec la règle d'affaiblissement, mais il me semble logique de l'écrire quand même).
- Élimination du ⊥ : [quels que soient Γ et P,] on a Γ,⊥⊢P. (Il n'y a pas de règle d'introduction du ⊥.)
- Introduction du ⇒ (=abstraction) : si Γ,A⊢B alors Γ⊢A⇒B ; élimination du ⇒ (=application) : si Γ⊢A et Σ,B⊢P, alors Γ,Σ,A⇒B⊢P.
- Introduction du ∀ : si Γ⊢A(y) où y est une variable n'apparaissant nulle part libre dans Γ alors Γ⊢∀x.A(x) ; élimination du ∀ : si Γ,A(t)⊢P où t est un terme, alors Γ,∀x.A(x)⊢P.
- Introduction du ∃ : si Γ⊢A(t) où t est un terme, alors Γ⊢∃x.A(x) ; élimination du ∃ : si Γ,A(y)⊢P où y est une variable n'apparaissant nulle part libre dans Γ ou P, alors Γ,∃x.A(x)⊢P.
- Pour ce qui est de la négation, ¬A doit être traité comme un simple raccourci de langage pour A⇒⊥.
Sur cette présentation, la différence avec la logique classique réside dans le fait de n'autoriser qu'une seule formule à droite du symbole ‘⊢’ (i.e., on pourrait décrire la logique classique essentiellement en symétrisant les règles ci-dessus par exemple en comparant avec ce que j'ai écrit pour la logique linéaire). On pourrait aussi autoriser un axiome P∨¬P, mais ce serait moins naturel.
Un théorème du calcul des prédicats intuitionniste est une formule P telle que ⊢P [soit un séquent valable au sens ci-dessus]. Si on permet Γ⊢P où Γ sont des hypothèses prises parmi un ensemble T d'axiomes, on dira que P est un théorème de la théorie T. Pour bien faire, il faudrait que je propose des règles pour l'égalité et des axiomes pour l'arithmétique (par exemple), mais je n'ai pas la patience de le faire ici : disons juste que les axiomes usuels de l'arithmétique de Peano donnent en logique intuitionniste une théorie qu'il est habituel d'appeler l'arithmétique de Heyting.
À titre d'exemple, ¬(p∨q) et ¬p∧¬q sont équivalents, c'est-à-dire que ¬(p∨q) ⇒ (¬p∧¬q) et (¬p∧¬q) ⇒ ¬(p∨q) sont des théorèmes de la logique intuitionniste, comme en logique classique, en revanche, seule l'implication (¬p∨¬q) ⇒ ¬(p∧q) est valable et pas sa réciproque.
★
Ajout () : Je me rends compte (cf. les commentaires de cette entrée) que quelque chose dont je n'ai pas du tout évoqué (ni même méta-évoqué) est ce qu'on peut dire sur les traductions et interprétations des logiques les unes dans les autres. Essayons d'en dire un minimum, en petits caractères parce que c'est vraiment une digression qui me sert un peu de bloc-notes (j'en ai marre d'avoir toujours du mal à retrouver ce qui suit) :
Le point de départ, c'est la traduction de Glivenko, qui observe que, dans le cadre du pur calcul propositionnel (c'est-à-dire sans quantificateurs), une formule P est démontrable en logique classique si et seulement si ¬¬P (la double négation de P) est démontrable en logique intuitionniste : ceci permet, au moins dans le cadre propositionnel, d'interpréter ou de traduire la logique classique à l'intérieur de la logique intuitionniste. La traduction de Gödel-Gentzen généralise celle de Glivenko au cas où on admet les quantificateurs : on définit une formule PGG (de la logique intuitionniste) pour toute formule P (de la logique classique) par :
- si P est atomique (c'est-à-dire, sans connecteur logique) alors PGG est ¬¬P ;
- (A∧B)GG est (AGG)∧(BGG) ;
- (A∨B)GG est ¬¬(AGG∨BGG) (ou, ce qui revient au même, ¬(¬(AGG)∧¬(BGG))) ;
- ⊤GG est ⊤ ;
- ⊥GG est ⊥ ;
- (A⇒B)GG est (AGG)⇒(BGG) ;
- (¬A)GG est ¬(AGG) ;
- (∀x.A(x))GG est ∀x.(A(x)GG) ;
- (∃x.A(x))GG est ¬¬∃x.(A(x)GG) (ou, ce qui revient au même, ¬∀x.¬(A(x)GG)) ;
et dans ces conditions, la logique intuitionniste démontre PGG (sans hypothèse) si et seulement si la logique classique démontre P (sans hypothèse).
Dans le sens contraire, on ne peut pas ramener la logique intuitionniste à la logique classique (disons que la logique intuitionniste est plus précise), mais on peut la ramener à la logique linéaire (dont je parlais ici) par la traduction suivante due à Girard :
- si P est atomique (c'est-à-dire, sans connecteur logique) alors PGi est P ;
- (A∧B)Gi est (AGi)&(BGi) ;
- (A∨B)Gi est (!(AGi))⊕(!(BGi)) ;
- ⊤Gi est ⊤ ;
- ⊥Gi est 0 ;
- (A⇒B)Gi est (!(AGi))⊸(BGi) ;
- (¬A)Gi est (!(AGi))⊸0 ;
- (∀x.A(x))Gi est ∀x.((A(x)Gi)) ;
- (∃x.A(x))Gi est ∃x.(!(A(x)Gi)) ;
toujours au sens où la logique linéaire démontre PGi (sans hypothèse) si et seulement si la logique intuitionniste démontre P (sans hypothèse).
De même, on peut ramener la logique intuitionniste à la logique classique modale S4 (c'est-à-dire enrichie d'un modalisateur □, « il est nécessaire », vérifiant la règle que de ⊢P on peut tirer ⊢□P, et les axiomes □(P⇒Q)⇒□P⇒□Q et □P⇒P et □P⇒□□P) par la traduction suivante que je crois due à Kripke (et visiblement très analogue à la traduction de Girard évoquée ci-dessus) :
- si P est atomique (c'est-à-dire, sans connecteur logique) alors PKr est P ;
- (A∧B)Kr est (AKr)∧(BKr) ;
- (A∨B)Kr est (□(AKr))∨(□(BKr)) ;
- ⊤Kr est ⊤ ;
- ⊥Kr est ⊥ ;
- (A⇒B)Kr est (□(AKr))⇒(BKr) (ou, ce qui revient au même, (¬□(AKr))∨(BKr) puisqu'on est ici en logique classique !) ;
- (¬A)Kr est ¬(□(AKr)) ;
- (∀x.A(x))Kr est ∀x.((A(x)Kr)) ;
- (∃x.A(x))Kr est ∃x.(□(A(x)Kr)) ;
ou encore par la suivante, qui est due à Gödel et Tarski :
- si P est atomique (c'est-à-dire, sans connecteur logique) alors PGT est □P ;
- (A∧B)GT est (AGT)∧(BGT) ;
- (A∨B)GT est (AGT)∨(BGT) ;
- ⊤GT est ⊤ ;
- ⊥GT est ⊥ ;
- (A⇒B)GT est □((AGT)⇒(BGT)) (ou, ce qui revient au même, □(¬(AGT)∨(BGT)) puisqu'on est ici en logique classique !) ;
- (¬A)GT est □(¬(AGT)) ;
- (∀x.A(x))GT est □∀x.((A(x)GT)) ;
- (∃x.A(x))GT est ∃x.((A(x)GT)) ;
et la logique modale S4 démontre PKr, ou, de façon équivalente, PGT (sans hypothèse) si et seulement si la logique intuitionniste démontre P (sans hypothèse) ; et en général, on a PGT ⇔ □(PKr) (équivalence démontrable dans S4).
L'une ou l'autre de ces traductions permettent peut-être de se
faire une idée intuitive du « sens » des connecteurs de la logique
intuitionniste en comprenant □P par quelque chose
comme P est nécessaire (c'est-à-dire, vrai dans tous les
mondes possibles [accessibles depuis celui-ci])
ou
peut-être P sera toujours vrai à l'avenir quoi qu'il
arrive
(mais attention à bien vérifier que le sens imagine qu'on
choisit valide les axiomes
□(P⇒Q)⇒□P⇒□Q et
□P⇒P et □P⇒□□P de la
logique S4).
Si on a lu ce que je raconte ci-dessous [oui, cette entrée est un véritable puzzle à remettre dans le bon ordre] sur la sémantique du calcul propositionnel par les ouverts d'un espace topologique, alors on peut retrouver cette sémantique en lisant □ comme l'opérateur « intérieur » (qui à une partie E de X associe le plus grand ouvert Int(E) qu'elle contient) et les connecteurs classiques ∧, ∨ et ¬ comme l'intersection, la réunion et le complémentaire.
★
L'intuitionnisme et les mathématiques constructives intéressent
aussi l'informatique et les informaticiens, notamment par le biais
d'un dictionnaire appelé
la correspondance
[ou l'isomorphisme
] de Curry-Howard ou la correspondance
preuves-programmes, qui fait correspondre, dans des conditions qu'il
n'est pas ici lieu d'expliciter plus précisément, les preuves
mathématiques et les théorèmes démontrés par ces preuves, avec des
programmes (termes
serait sans doute plus exacts) dans des
langages de programmations fonctionnels fortement typés et les types
de ces termes. (Une façon de définir la correspondance serait, dans
les règles de démonstration que j'ai énumérées ci-dessus, de dire à
chaque fois à quoi elles correspondent au niveau de la construction de
termes, où Γ⊢P va correspondre à un terme de
type P ayant des variables libres de types Γ ;
par exemple, la coupure correspond à la substitution d'un terme dans
un autre, l'identité à l'utilisation d'une variable libre,
l'élimination du ⇒ à l'application d'une fonction à un terme et
l'introduction du ⇒, au contraire, à la création d'une fonction par
lambda-abstraction. À titre d'exemple, le terme S
:=
λx.λy.λz.(xz)(yz),
c'est-à-dire la fonction qui prend en entrée trois
variables x, y, z et renvoie le
résultat de l'application de x à z appliqué au
résultat de l'application de y à z, a pour type
(p→q→r)→(p→q)→p→r
en notant u→v le type des fonctions prenant en
entrée le type u et en sortie le type v,
où p→q→r serait le type
de x, p→q celui de y
et p celui de z ; et il correspond par
l'isomorphisme de Curry-Howard à la preuve de la tautologie
(p⇒q⇒r)⇒(p⇒q)⇒p⇒r
consistant à dire : supposons
(x) que p⇒q⇒r soit vrai et
(y) que p⇒q le soit et
(z) que p le soit ; alors d'après (x)
et (z), on voit que q⇒r est vrai, et
par ailleurs d'après (y) et (z) que q
l'est, donc finalement r est vrai comme annoncé
.) La
correspondance de Curry-Howard est assez naturellement intuitionniste
en ce sens que les preuves
dont il est question sont des
preuves en logique intuitionniste ; et c'est plus ou moins cette
correspondance qui assure que la logique intuitionniste est
constructive au sens où d'une preuve on peut (dans certaines
conditions) extraire un programme calculant l'objet dont elle affirme
l'existence.
☆ Il faut néanmoins nuancer tout ça par le fait que
la loi de
Peirce, c'est-à-dire la tautologie de la logique classique
((p⇒q)⇒p)⇒p
essentiellement équivalente à la règle du tiers exclu, correspond au
type ((p→q)→p)→p de la
fonction
classique call/cc
de langages tels que Scheme ou SML/NJ (sur
laquelle j'avais commencé à
écrire une page il y a
une éternité, qui n'a jamais été finie ; mais je remarque au passage
que je suis mentionné dans la page Wikipédia sur
le call/cc
). Bref, l'usage du call/cc
correspond à peu près, par rapport à un langage de programmation qui
ne l'a pas, à l'usage du tiers exclu (enfin, de la loi de Peirce) par
rapport à la logique intuitionniste. (Et donc on se dit que sans
doute, d'une preuve en logique classique on doit pouvoir extraire des
programmes utilisant le call/cc
qui est, après tout, tout
à fait implémentable — il faudrait creuser pour voir exactement ce qui
vaut et ne vaut pas.)
Ajout/digression
() : Décrivons cependant brièvement
à quoi peut ressembler un terme de type p∨¬p
écrit en utilisant le call/cc
. Autrement dit, il s'agit,
de renvoyer un type union entre un type p (quelconque,
donné, sur lequel on ne sait rien) et le type p→⊥ des
fonctions prenant un p en entrée et renvoyant quelque chose
qui n'existe pas : on est donc censé renvoyer soit l'un soit l'autre
(en précisant lequel). Voici ce que fait le programme : il renvoie
(dans le type union) une fonction de type p→⊥ qui se
comporte de la façon suivante : si on lui passe un objet de
type p (auquel cas il est censé renvoyer quelque chose
d'impossible !), il « change d'avis », revient en arrière dans le
temps (enfin, dans la pile d'appels) en utilisant la continuation
qu'il avait soigneusement sauvegardée au moyen
du call/cc
, et renvoie plutôt (dans le type union)
l'objet de type p qu'on lui a passé. Ceci satisfait la
promesse annoncée : on fournit un objet de type p→⊥ jusqu'à
ce qu'un objet de type p se manifeste, auquel cas on
fournit un objet de type p ; mais on peut se dire que ce
programme a manifestement triché ! En quelque sorte, je suis tenté de
dire que le problème en présence du call/cc
est que les
types union peuvent changer d'avis sur ce qu'ils font par l'invocation
d'une continuation plus tard dans le programme.
★
Bref, je voudrais écrire quelque chose sur l'intuitionnisme, mais je ne sais pas par quel bout le prendre, et j'ai peut-être trop de choses à dire.
Une possibilité serait de commencer par parler du seul calcul
propositionnel, c'est-à-dire sans quantificateurs, juste avec les
connecteurs logiques ⇒ (implication), ∧ (conjonction),
∨ (disjonction), ¬ (négation, mais ¬P est juste une
abréviation de P⇒⊥), ⊤ (vrai) et ⊥ (faux), un peu comme
j'ai parlé de logique linéaire il
n'y a pas si longtemps, et avec laquelle je pourrais essayer de faire
le lien. La logique intuitionniste est intéressante même au niveau du
simple calcul propositionnel (alors que la logique classique ne l'est
franchement pas trop : il s'agit juste de faire des tables de vérité
pour décider ce qui est tautologique ou pas), et il y a déjà
énormément à en dire. Par exemple, juste avec une variable,
on peut fabriquer
une infinité
d'énoncés différents et non équivalents entre eux (on parle du
treillis de Rieger-Nishimura ; pour comparaison, en logique classique
on ne peut en faire que quatre, ⊥, p, ¬p et ⊤ ;
cf. aussi cette
question MathOverflow et la belle réponse que j'a reçue). Il y a
une structure algébrique qui est l'équivalent pour la logique
intuitionniste de ce que sont
les algèbres
de Boole pour la logique classique, à savoir
les algèbres de
Heyting. On peut y penser comme les ouverts d'un espace
topologique (enfin, si on sait ce que ça veut dire) : si sur un espace
topologique X on définit les opérations entre ouverts
de X que sont l'intersection
(notée A∩B ou A∧B) et la
réunion (notée A∪B ou A∨B)
mais surtout en notant A⇒B pour l'intérieur
Int(B∪(X∖A)) de la
réunion B∪(X∖A) de B et du
complémentaire de A (et notamment ¬A pour
Int(X∖A), complémentaire de l'adhérence
de A, également appelé pseudocomplémentaire
de A), et si on interprète ⊥ comme X tout entier
et ⊤ comme ∅ (le vide), alors les ouverts de X forment une
algèbre de Heyting (par ailleurs complète ; ceci est à mettre en
parallèle avec le fait que les
ouverts réguliers,
de X forment une algèbre de Boole complète, les opérations
étant un petit peu différentes de celles que j'ai définies) ; et un
formule propositionnelle est démontrable dans la logique
intuitionniste si et seulement si elle donne l'ouvert plein dans
n'importe quel espace topologique (c'est le cas, par exemple,
de p⇒p, mais pas de p∨¬p).
Une autre façon d'interpréter (i.e., donner une sémantique à) la
logique intuitionniste passe par
les modèles de
Kripke, et fait le lien avec la logique modale.
Rien que le sujet du calcul propositionnel est, en logique intuitionniste, déjà fort intéressant. Il y a quantité de formules propositionnelles qui sont démontrables en logique classique, pas en logique intuitionniste, mais qui sont néanmoins valides dans telle ou telle sémantique particulière de la logique intuitionniste, par exemple certains espaces topologiques (ou certains topoï), ou par exemple dans le cadre de la réalisabilité de Kleene (ou, ce qui revient au même, dans le topos effectif), ou encore dans le cadre de la « logique de Medvedev » dont je dois aussi dire un mot. Par exemple l'axiome de Scott ((¬¬p⇒p) ⇒ (p∨¬p)) ⇒ (¬¬p∨¬p) ou bien l'axiome de Kreisel-Putnam (¬p⇒(q₁∨q₂)) ⇒ ((¬p⇒q₁) ∨ (¬p⇒q₂)), dont le sens intuitif n'est pas du tout évident à imaginer, pas plus que la signification sur un espace topologique (voir ici au sujet du premier, là pour le second), qui ne sont, en l'occurrence, pas valides dans la réalisabilité de Kleene mais le sont dans la logique de Medvedev (voir aussi cette réponse MathOverflow) ; la formule de Ceitin (¬(p₁∧p₂) ∧ (¬p₁⇒(q₁∨q₂)) ∧ (¬p₂⇒(q₁∨q₂))) ⇒ ((¬p₁⇒q₁) ∨ (¬p₁⇒q₂) ∨ (¬p₂⇒q₁) ∨ (¬p₂⇒q₂)) qui est valide dans la réalisabilité de Kleene et dans la logique de Medvedev mais n'est quand même pas un théorème de la pure logique intuitionniste ; ou encore l'étrange formule ((¬¬p₁⇔(¬p₂∧¬p₃)) ∧ (¬¬p₂⇔(¬p₃∧¬p₁)) ∧ (¬¬p₃⇔(¬p₁∧¬p₂)) ∧ ((¬p₁⇒(¬p₁∨¬p₃)) ⇒ (¬p₂∨¬p₃)) ∧ ((¬p₂⇒(¬p₂∨¬p₁)) ⇒ (¬p₃∨¬p₁)) ∧ ((¬p₃⇒(¬p₃∨¬p₂)) ⇒ (¬p₁∨¬p₂))) ⇒ (¬p₁ ∨ ¬p₂ ∨ ¬p₃) qui, elle, est valide dans la réalisabilité de Kleene mais pas dans la logique de Medvedev (enfin, il paraît — franchement, je n'y vois rien). J'aimerais me faire une idée intuitive de ce que ces formules « signifient » mais je reste face à elles comme une poule face à un couteau. Je crois cependant comprendre que je ne suis pas le seul et que c'est un sujet sur lequel « on » ne sait vraiment pas dire grand-chose. Tout le sujet des logiques intermédiaires (entre les logiques classique et intuitionniste) est miné de problèmes ouverts.
★
La définition de la logique de
Medvedev est assez jolie et simple pour mériter ici une mention rapide
en un paragraphe. On appellera problème fini un couple
(X,S) où X≠∅ est un ensemble fini non
vide appelé l'ensemble des candidats
du problème
et S⊆X en est une partie appelée ensemble
des solutions
du problème. On définit les connecteurs logiques
entre problèmes finis de la façon suivante :
(X,S)∧(Y,T) :=
(X×Y, S×T) (i.e., les
candidats et les solutions d'une conjonction sont juste les couples
des objets correspondants des deux problèmes) ;
(X,S)∨(Y,T) :=
(X⊎Y, S⊎T)
où X⊎Y := (X×{0})∪(Y×{1})
dénote la réunion rendue disjointe (i.e., les candidats et les
solutions d'une disjonction sont juste les objets correspondants de
l'un ou l'autre des deux problèmes) ; et
(X,S)⇒(Y,T) :=
(YX, U)
où YX est l'ensemble des
fonctions X→Y et U est la partie
formée des f∈YX telles
que f(s)∈T pour
tout s∈S (autrement dit, les candidats et les
solutions d'une implication sont respectivement les fonctions entre
candidats et celles qui transforment une solution de l'un en solution
de l'autre) ; enfin, ⊥ est défini comme ({*},∅) et ⊤ comme ({*},{*}),
ce qui permet d'identifier ¬(X,S) comme
({*},{*:S=∅}) et ¬¬(X,S) comme
({*},{*:S≠∅}). Bref. Une formule propositionnelle,
faisant intervenir des
variables p1,…,pk
est dite valide dans la logique de Medvedev lorsque pour
tous
ensembles X1,…,Xk
non vides il existe un s (ne dépendant que
de X1,…,Xk) tel
que quels que
soient Si⊆Xi
l'élément s soit solution du problème obtenu en substituant
(Xi,Si)
à la place de pi dans la formule.
Autrement dit, il s'agit des formules décrivant des problèmes qu'on
peut résoudre uniformément quels que soient les problèmes qu'on
injecte dedans (uniformément au sens des
ensembles Si de solutions). Par
exemple, la formule p⇒p est validé en prenant
pour s l'identité dans XX,
mais la formule p∨¬p n'est pas valide dans la
logique de Medvedev car on ne peut pas trouver un élément
de X⊎{*} qui appartienne à toute partie S non
vide de X et soit en même temps égal à * si S=∅.
Les formules valides de la logique de Medvedev incluent tout ce qui
est démontrable dans le calcul propositionnel intuitionniste et sont
incluses dans celles qui sont démontrables en logique classique, mais
ces deux inclusions sont strictes (et les axiomes de Scott et de
Kreisel-Putnam évoqués plus haut donnent des exemples de formules
Medvedev-valides mais non démontrables intuitionnistement). Malgré sa
définition très simple, on sait finalement très peu de choses sur la
logique de Medvedev. Notons que la réalisabilité de Kleene est assez
analogue, en fait, à la logique de Medvedev mais en remplaçant les
ensembles finis par des parties de ℕ et les fonctions par des
fonctions calculables. [Ajout : encoreune fois,
voir cette entrée ultérieure pour
une description de la réalisabilité.]
★
Il y a ensuite aussi énormément de choses à dire en dépassant le calcul propositionnel et en allant chercher la logique du premier ordre, voire d'ordre supérieur. On peut formuler tout un tas de principes valables en mathématiques classiques mais pas en mathématiques constructives (à titre d'exemple, le principe de Markov (∀n.(P(n)∨¬P(n)) ∧ ¬∀n.¬(P(n))) ⇒ ∃n.(P(n)) qui affirme que si α:ℕ→{0,1} est une suite binaire, dont tous les termes ne valent pas 0 alors elle a un terme qui vaut 1 ; celui-ci est classiquement valide et aussi validé par la réalisabilité de Kleene mais pas validé par les mathématiques constructives les plus générales), et chercher les implications entre elles : ceci donne naissance à une théorie des mathématiques à rebours mais (partiellement !) constructives : voir ce texte pour en savoir plus.
★
Bon, cette entrée est déjà beaucoup trop longue alors que je n'ai rien dit sauf parler de ce que je voudrais dire, donc je vais m'arrêter là un peu en queue de poisson : ça manque de conclusion mais je ne sais pas quoi y mettre, et il vaut mieux que je publie maintenant que laisser ce texte moisir dans mes cartons comme ça arrivera inévitablement si je me dis que je veux l'améliorer. (En plus, mon poussinet a allumé la télé qui parle en boucle de l'incendie de Notre-Dame, ça m'empêche de réfléchir.)