Logique intuitionniste

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

La logique intuitionniste est une alternative à la logique classique où la notion de vérité est remplacée par la notion de prouvabilité constructive. Une phrase comme "il pleut ou bien il ne pleut pas" (tiers exclu) est démontrable en logique classique alors qu'en logique intuitionniste, un énoncé de la forme "P ou non P" n'est pas forcément démontrable de manière constructive.

Histoire[modifier | modifier le code]

L'intuitionnisme est une position philosophique vis-à-vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer[1] comme une alternative à l'approche dite classique ; cela l'a conduit à ne pas inclure certaines formes du raisonnement mathématique traditionnel, qu'il jugeait contre-intuitives ː

  • Le tiers exclu, qui consiste à dire qu'étant donnée une proposition , on a soit ou alors non .
  • L'existentiel non constructif. Brouwer veut que quand un mathématicien affirme il existe tel que il donne aussi un moyen de construire qui satisfait .

Brouwer a prôné une mathématique qui rejetterait le tiers exclu et n'accepterait que l'existentiel constructif. Cette attitude a été assez violemment critiquée par des mathématiciens comme David Hilbert[réf. nécessaire] tandis que d'autres comme Hermann Weyl[réf. nécessaire] y ont souscrit.

Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko[2] et Arend Heyting. Kurt Gödel[3] et Andreï Kolmogorov[4]. La logique intuitionniste revisite aussi le concept d'implication. L'implication n'est plus l'implication matérielle . Quand un mathématicien intuitionniste affirme , il veut dire qu'il fournit un procédé de « construction » d'une démonstration de à partir d'une démonstration de . Ceci est d'ailleurs la clé du contenu calculatoire de la logique intuitionniste. Ils ont montré que l'on pouvait représenter la logique classique dans la logique intuitionniste et ceci bien que l'ensemble des formules valides de la logique intuitionniste soit strictement inclus dans l'ensemble des formules valides de la logique classique[5]. Gerhard Gentzen[6] a formulé des règles de déduction naturelle pour la logique intuitionniste.

Une fois formalisée, quatre faits font de la logique intuitionniste une logique à part entière : des systèmes de déduction (à la Hilbert, en déduction naturelle, en calcul des séquents), l'existence de modèles qui en font un système complet de déduction, un contenu calculatoire, connu sous le nom de correspondance de Curry-Howard, enfin une vision comme une logique modale étendant la logique classique avec une modalité dite de « prouvabilité »[7]. La logique intuitionniste n'a donc rien d'exotique.

Des travaux[8], notamment la correspondance de Curry-Howard, lui ont donné un statut central dans la logique et dans l'informatique, en faisant d'elle historiquement la première des logiques constructives. L'étude de la logique intuitionniste est aussi la clé pour bien comprendre la logique classique et ses subtilités. Allant plus loin, le logicien Jean-Yves Girard a proposé une logique plus faible que la logique intuitionniste, qu'il a appelée la logique linéaire qui permet de mieux comprendre la logique intuitionniste en particulier. D'autres logiques sous structurelles ont par ailleurs été étudiées. Notons à ce propos qu'il existe, entre la logique intuitionniste et la logique classique, une infinité de logiques intermédiaires, plus fortes que la logique intuitionniste et plus faibles que la logique classique.

Syntaxe du langage de la logique intuitionniste[modifier | modifier le code]

La syntaxe de la logique intuitionniste propositionnelle est la même que pour la logique propositionnelle classique. La syntaxe de la logique intuitionniste du premier ordre est la même que la syntaxe de la logique classique du premier ordre.

Syntaxe de la logique intuitionniste propositionnelle[modifier | modifier le code]

Construction Lecture intuitive en logique classique Lecture intuitive en logique intuitionniste
est vraie est prouvable
est vraie ou est vraie est prouvable ou est prouvable
est vraie et est vraie est prouvable et est prouvable
Faux Faux
Si est vraie alors est vraie Si est prouvable alors est prouvable
(abréviation de ) est fausse est contradictoire

Syntaxe de la logique intuitionniste du premier ordre[modifier | modifier le code]

Construction Lecture intuitive en logique classique Lecture intuitive en logique intuitionniste
il existe un élément tel que est vraie on peut construire un élément tel que est prouvable
pour tout élément , est vraie En prenant un élement quelconque , est prouvable

Non-interdéfinabilité des opérateurs[modifier | modifier le code]

La négation peut se définir à partir de l'implication ː se définit comme . En logique propositionnelle classique, on peut définir la disjonction (le "ou") à partir du "et" grâce aux lois de Morgan. Par exemple, peut se définir comme un raccourci d'écriture pour . En logique propositionnelle intuitionniste, ce n'est plus le cas et chaque opérateur a une interprétation différente (cf. tableau ci-dessus)[9]. De même, on ne peut pas définir comme .

Règles de déduction naturelle[modifier | modifier le code]

En logique intuitionniste, les opérateurs ne sont pas inter-définissables[10]. C'est pourquoi nous allons donner des règles pour chaque connecteur et pour l’absurde ⊥. Nous donnons une (ou des) règle(s) d'élimination et une (ou des) règle(s) d'introduction pour chaque connecteur (typique de la déduction naturelle). En déduction naturelle, se lit « de l'ensemble de propositions on déduit la proposition  ».

La logique implicative minimale[modifier | modifier le code]

La déduction naturelle en logique intuitionniste inclut les deux règles suivantes de la déduction naturelle en logique implicative minimale, qui est la logique propositionnelle avec uniquement l'implication comme connecteur ː

.

La règle s'appelle la règle d'élimination de l'implication. Elle se lit comme suit : si de l'ensemble d'hypothèses je déduis et si de plus de l'ensemble d'hypothèses je déduis alors de l'ensemble d'hypothèses je déduis . L'élimination de l'implication est aussi appelé modus ponens.

La règle s'appelle la règle d'introduction de l'implication. Elle se lit comme suit : si de l'ensemble d'hypothèses et de l'hypothèse je déduis alors de l'ensemble d'hypothèses je déduis .

Le système de déduction obtenu jusqu'ici est simple (rasoir d'Ockham) mais moins puissant que la logique classique ː par exemple, la loi de Peirce et la proposition ne sont pas démontrable.

La logique propositionnelle intuitionniste[modifier | modifier le code]

La déduction naturelle en logique intuitionniste contient les règles de la déduction naturelle de la logique implicative minimale et les règles de cette sous-section.

Ex falso quodlibet[modifier | modifier le code]

Cette règle est nommée principe d'explosion, ou en latin, ex falso quodlibet. Le principe d'explosion signifie que si un ensemble de propositions Γ conduit à l'absurde ⊥, alors de Γ, on peut déduire n'importe quelle proposition .

La négation[modifier | modifier le code]

Traditionnellement, on considère la négation comme l'abréviation et on ne donne donc pas habituellement de règles correspondant à la négation. Cependant on pourrait en donner et elles seraient ː

La conjonction[modifier | modifier le code]

Au connecteur (conjonction), on associe deux règles d'élimination, et , et une règle d'introduction.

se lit "A et B".

La disjonction[modifier | modifier le code]

Au connecteur (disjonction), on associe une règle d'élimination et deux règles d'introduction ː

.

On remarque que la règle d'élimination de la disjonction est une règle tryadique ː elle a trois prémisses.

Le calcul des prédicats intuitionniste[modifier | modifier le code]

En plus des règles du calcul propositionnel intuitionniste, le calcul des prédicats intuitionniste contient de nouvelles règles d'introduction et d'élimination pour les quantificateurs « quel que soit » et « il existe ».

Remarque : Nous rappelons que A[t/x] signifie le remplacement de toutes les occurrences librement substituables de la variable x par le terme t ; voir calcul des prédicats pour les notions de « variable », « terme », « substitution » et de « librement substituable ».

Le quantificateur universel[modifier | modifier le code]

Le quantificateur existentiel[modifier | modifier le code]

Sémantique de la logique intuitionniste[modifier | modifier le code]

Modèles de Kripke[modifier | modifier le code]

Un modèle de Kripke pour la logique intuitionniste. Plus on avance dans le temps, plus on apprend des variables propositionnelles.

On peut donner une sémantique à la logique intuitionniste qui est une sémantique de Kripke[11]. Un modèles de Kripke modèles sont des graphes où ː

  • les nœuds sont des mondes possibles. Selon Kripke, ces mondes représentent des contenus d'information fondés sur des preuve (evidential situations)[11]. Chaque monde est muni d'une valuation classique ː intuitivement, pour chaque variable propositionnelle p, p est vraie dans un monde si on a assez d'information pour prouver p et p est fausse sinon.
  • Une relation d'accessibilité de préordre sur les mondes ː une relation réflexive et transitive hiérarchisent les mondes. Pour Kripke, un arc m → m' signifie que m' est dans le "futur"[11],[12] de m.
  • La valuation est telle que si une variable propositionnelle p est vraie dans m et que m' est dans le "futur" de m, p est aussi vraie dans m' (on ne perd pas d'information et donc on peut toujours prouver p).

Pour dire qu'un monde satisfait une formule , on dit aussi que le monde force[11],[12] une formule . La relation forçage de (ou de réalisabilité) est définie par induction structurelle par ː

  • le monde force une variable propositionnelle si est vraie dans le monde m ;
  • le monde force si force et force  ;
  • le monde force si force ou force  ;
  • le monde force si pour tout le monde accessible depuis , si force alors force . (certains auteurs appellent l'ensemble des mondes accessibles depuis un cône[réf. nécessaire])

Une formule est valide, si pour tout monde de tout modèle , force .

Exemple[modifier | modifier le code]

Un modèle de Kripke où le monde de gauche ne force pas le tiers-exclu et ne force pas la loi de Peirce .

Considérons le modèle de Kripke à droite. Il ne satisfait pas le tiers-exclu . En effet, d'une part, le monde initial ne force pas (intuitivement, n'est pas prouvé car p est fausse donc cela signifie que l'on n'a pas encore assez d'informations). D'autre part, le monde initial ne force pas n'est pas contradictoire car en fournissant un peu plus d'effort, on peut "gagner plus d'informations" et arriver dans le monde de droite et prouver p. Le tiers-exclu n'est pas valide. Aussi ː

  • (loi de Peirce) n'est pas valide ː le monde de gauche du modèle de Kripke à droite ne force pas .
  • n'est pas valide.

Correction de la logique intuitionniste[modifier | modifier le code]

La logique intuitionniste est correcte vis-à-vis des modèles de Kripke[13], c'est-à-dire que toute formule démontrable (par exemple avec les règles de déduction naturelle de la section précédente) est valide. On peut utiliser ce résultat pour montrer qu'une formule n'est pas démontrable en logique intuitionniste. Par exemple, comme le tiers-exclu ou la loi de Peirce ne sont pas valides, elles ne sont pas démontrables.

Complétude de la logique intuitionniste[modifier | modifier le code]

Toute formule valide est démontrable[14]. La démonstration se fait de la façon suivante : si n'est pas démontrable alors on peut construire un contre-modèle (infini) de c'est-à-dire un modèle contenant un monde qui ne force pas .

Relations avec la logique classique[modifier | modifier le code]

Exemples de différences avec la logique classique[modifier | modifier le code]

Les opérations ne sont pas définies l’une par rapport à l’autre (voir plus loin), et ne sont définies qu’en elles-mêmes. Elles sont définies par l’interprétation qui doit en être faite. Pour cette raison, en plus des règles de calcul, sont données les interprétations qui doivent être faites des expressions de chaque opérateur[9].

Quelques validités[modifier | modifier le code]

Le tableau suivant donne quelques validités de la logique intuitionniste.

Validités en logique intuitionniste Explications pour Explications pour
Si A est prouvable, alors il est prouvé que A n'est pas contradictoire. Par exemple, il est prouvé que "il pleut" n'est pas contradictoire (on n'obtient pas de contradiction en supposant "il pleut"). Pourtant, "il pleut" n'est pas prouvable, sauf si on sort et qu'on se fait mouiller.
Si A est contradictoire, alors une preuve que n’est pas contradictoire donne une contradiction. Si on a une preuve que n’est pas contradictoire donne une contradiction, alors. A est contradictoire.
Si A est contradictoire ou B est contradictoire, alors "A et B" est contradictoire. Par exemple, être grand et petit est contradictoire. Pourtant, être grand n'est pas contradictoire et être petit n'est pas contradictoire.
Si on obtient une contradiction d'une preuve de A ou d'une preuve de B, alors A est contradictoire et B est contradictoire. Si A est contradictoire et B est contradictoire, alors d'une preuve de A ou d'une preuve de B, on obtient une contradiction.
Si A est contradictoire ou alors B est prouvable, alors si j'ai une preuve de A (ce qui n'existe pas ǃ), j'ai une preuve de B. Par exemple, je construis une preuve de "x>0" qui utilise une preuve "x>1". Pourtant, "x>1" n'est pas contradictoire et "x>0" n'est pas prouvable.
Si "il existe x tel que A(x)" est contradictoire, alors pour tout x, A(x) est contradictoire. Si pour tout x, A(x) est contradictoire, alors "il existe x tel que A(x)" est contradictoire.
Si je peux construire un x tel que A(x) donne une contradiction, alors "pour tout x, A(x)" est contradictoire. Par exemple, "pour tout x, x est pauvre" est contradictoire (car je vois qu'il existe des richesses). Pourtant, je ne peux pas trouver un individu x (riche) tel que x est pauvre soit contradictoire.

En logique classique, les formules obtenues en remplaçant les implications par des équivalences sont des validités (le tableau contiendrait que des ).


Négation[modifier | modifier le code]

On peut interpréter comme : « Il est démontré que est contradictoire ».

On dispose en logique intuitionniste du théorème suivant :

Mais on ne peut pas en conclure que est vrai. En effet, cette dernière équivalence ne peut être prouvée en logique intuitionniste.

Double négation[modifier | modifier le code]

On peut interpréter comme : « Il est démontré qu’il est contradictoire d’affirmer que est contradictoire », c'est-à-dire « Il est démontré que n’est pas contradictoire ». Mais on ne peut pas en déduire que «  est démontrable ».

Le théorème :

peut être démontré en logique intuitionniste. Mais la réciproque ne peut pas l'être. On n'a pas . L’expression peut s’interpréter comme « d'une démonstration de , on peut construire une démonstration de  ». Mais le fait que ne soit pas contradictoire n’est pas suffisant pour établir une démonstration de «  ».

À titre d'exemple, soit x un réel et la proposition x est rationnel. Démontrer , c'est donner deux entiers a et b tels que x = a/b. Si est contradictoire (et donc si on a ), c'est que x est non rationnel, ou irrationnel. Dire que l'on a , c'est dire que supposer x irrationnel conduit à une contradiction, et donc conclure que x n'est pas irrationnel. Mais ce n'est pas suffisant pour établir l'existence effective de deux entiers a et b tels que x = a/b. Ainsi, en logique intuitionniste, ne pas être irrationnel est une propriété différente et plus faible que celle d'être rationnel.

Conjonction[modifier | modifier le code]

L'interprétation de est : on dispose d'une preuve de et d'une preuve de (comparable à ce qu’il en est en logique classique).

En logique intuitionniste, la proposition suivante est un théorème :

Mais contrairement à ce qu’il en serait en logique classique, n’est seulement qu’une conséquence de , la réciproque étant fausse. En effet, supposer que est contradictoire, est insuffisant en logique intuitionniste pour conclure si seul l'est ou seul ou s'ils le sont tous les deux. Par exemple, supposer qu'un nombre est à la fois rationnel et irrationnel est contradictoire, mais insuffisant pour conclure si ce nombre est irrationnel ou non.

Disjonction[modifier | modifier le code]

L'interprétation de est : on a une preuve de ou une preuve de .

On dispose en logique intuitionniste du théorème suivant :

A et B s’excluent mutuellement et ne sont pas simultanément vrais. Cette situation est comparable à ce qu’il en serait dans la logique classique de Boole et Karnaugh.

Par contre, le théorème suivant :

est valide en logique intuitionniste, mais pas sa réciproque. En effet, si x est un nombre réel, on sait que s'il est rationnel alors il n'est pas irrationnel, mais on n'est pas pour autant capable de conclure si ce nombre est irrationnel ou non.

Quantificateur existentiel[modifier | modifier le code]

L'interprétation de est : nous pouvons créer un objet et prouver que . L'existence de x est ici effective ou constructive. Il ne s'agit pas d'une existence théorique d'un élément vérifiant .

On dispose du théorème suivant :

S’il n’existe pas de x qui vérifie A(x) alors pour tous les x on ne vérifie pas A(x), d’où l’équivalence (qui correspond à l’intuition et se formule naturellement). Cette propriété est comparable à ce qu’il en serait en logique classique.

Quantificateur universel[modifier | modifier le code]

L'interprétation de est : on a une preuve que pour chaque x appartenant à l’ensemble spécifié, on peut prouver A(x) (comparable à ce qu’il en est en logique classique).

On dispose en logique intuitionniste du théorème suivant :

Mais contrairement à ce qu’il en serait en logique classique, la réciproque est fausse. En effet, cette réciproque exigerait que, en supposant contradictoire l'universalité de la propriété , on soit capable d'exhiber explicitement un objet x invalidant , ce qui n'est rarement possible.

On peut aussi dire que, en logique intuitionniste, l'affirmation de est l'affirmation de l'existence effective et constructible d'un objet x validant , alors que n'en est que l'existence théorique, exprimant seulement qu'il est contradictoire que soit universellement contradictoire. La logique classique ne fait aucune distinction entre ces deux existences, alors que la logique intuitionniste considère la deuxième comme plus faible que la première.

Tiers exclu[modifier | modifier le code]

La proposition suivante

est un théorème de la logique classique, mais pas de la logique intuitionniste. Dans cette dernière, elle signifierait que nous pouvons prouver ou prouver , ce qui n'est pas toujours possible.

Par exemple, en arithmétique munie de la logique intuitionniste (dite arithmétique de Heyting), l’expression est valide, car pour tout couple d'entiers, on peut prouver qu'ils sont égaux, ou on peut prouver qu'ils sont différents. Il en est de même pour deux rationnels. Mais pour deux réels en analyse constructive, on ne dispose pas de méthode générale permettant de prouver que ou de prouver que . Cette situation correspond bien à ce qu'on rencontre en algorithmique, où l’égalité ou l’inégalité entre deux réels peut être non calculable, c'est-à-dire, non décidable.

Relations entre les règles[modifier | modifier le code]

Pour mieux comprendre, on remarquera dans ce qui précède, que contrairement à ce qu’il en est dans la logique de Boole, la conjonction ne peut pas être reformulée en termes de disjonction et que le quantificateur existentiel ne peut pas être reformulé en termes de quantificateur universel  ; ceci en vertu du principe du constructivisme. Dit d’une autre manière et dans des termes peut-être plus proches de l’informatique : il n’est pas permis de réduire les contraintes d’une expression.

Concernant la disjonction et le quantificateur universel , seules leurs expressions sous formes négatives peuvent être reformulées en termes de, respectivement, conjonction et quantificateur existentiel . Cependant, une remarque : il n’est pas possible de contourner cette exigence par l’usage de doubles négations, car (et justement pour cette raison) en logique intuitionniste, n’est pas équivalent à .

Les interprétations des expressions ne se font pas dans le sens de et , mais dans le sens de Prouvable et Contradictoire. C’est ce qui explique que nous ne disposons pas de tables de calcul, comme avec l’algèbre de Boole, ce qui ensuite, explique pourquoi les opérations ne puissent pas être redéfinies dans les termes d’une autre.


Inclusion de la logique classique dans la logique intuitionniste[modifier | modifier le code]

Si l’on admet la démonstration faite par Kurt Gödel, que l’insertion de double-négations placées selon des règles définies, nommée « non-non traduction (en) de Gödel-Kolmogorov » (voir ci-après), permet de rendre démontrable en logique intuitionniste toute formule démontrable en logique classique ; et si l’on considère qu’en logique intuitionniste, est une forme affaiblie de , alors il est possible d’assimiler la logique classique à une forme affaiblie de la logique intuitionniste et de voir la logique classique comme incluse dans la logique intuitionniste. Remarque : si l’on admet cela, on peut également faire remarquer que la logique intuitionniste n’est pas « moins capable » que la logique classique (voir les exposés qui suivent).

De manière plus économe que la saturation des formules et sous-formules par des doubles négations, Gödel a remarqué que si on considère une fonction de l'ensemble des formules dans l'ensemble des formules définie par :

  1. , pour une formule atomique différente de ⊥

et sont des formules quelconques et est une formule ayant comme paramètre.

Alors on a le théorème suivant :

  • .

est la déduction classique et est la déduction intuitionniste.

La Non-non traduction[modifier | modifier le code]

Ce modèle est-il pertinent ? Cliquez pour en voir d'autres.
Cette section semble contenir un travail inédit ou des déclarations non vérifiées (15 avril 2016).

Vous pouvez aider en ajoutant des références. Voir la page de discussion pour plus de détails.

Ce qui amena Brouwer à concevoir l’intuitionnisme étant une remise en cause de la qualité des preuves de la logique classique[15], une question peut venir : quelle est donc la valeur d’une preuve de la logique classique du point de vue de la logique intuitionniste ? Dans le cas de la preuve de l’hypothèse qu’il existe des a et b irrationnels tels que ab soit rationnel (voir plus haut), la preuve de cette affirmation par le tiers-exclus est-elle fausse ? Il serait contradictoire de l’affirmer, puisque le théorème de Gelfond-Schneider indique que effectivement, l’une des deux hypothèses utilisées est concrètement vraie, et qu’il existe des solutions qui permettent d’en donner des exemples à l’œuvre. Cependant, comme vu précédemment, elle apporte une réponse… incomplète (elle ne réalise pas de solution). On pourra dire assez honnêtement, que la preuve par le tiers-exclus, montre au moins que l’affirmation de l’hypothèse qu’elle « démontre », n’est pas une contradiction. La preuve de la non-contradiction d’une hypothèse selon la logique intuitionniste étant la preuve de , c’est finalement la preuve de (qui signifie que peut éventuellement être démontré) qu’a effectuée la démonstration par la logique classique. Cette constatation est le fondement de la non-non traduction, qui permet d’exprimer une formule de la logique classique en logique intuitionniste (voir Liens externes). Ce principe a été formalisé par Kurt Gödel et Andreï Kolmogorov.

Attention : la non-non traduction est une traduction dans un seul sens. Bien qu’elle permette de traduire une expression de la logique classique en termes de la logique intuitionniste, elle ne garantit par l’inverse (mais l’inverse reste possible dans certains cas, comme il peut l’être trivialement pour une formule traduite de la logique classique). De plus et ne serait-ce que pour la raison que, par exemple en logique classique ou encore qu’en logique classique les opérateurs peuvent être exprimés les uns par rapport aux autres, la non-non traduction ne peut pas être bijective : plusieurs expressions de la logique classique peuvent correspondre à une même expression de la logique intuitionniste.

Traduction en logique modale classique[modifier | modifier le code]

La logique intutionniste peut être traduite dans la logique modale classique S4[16] munie d'une modalité . La construction se lit " est prouvable"[7] La traduction est définie par ː

pour toute variable propositionnelle ,

Une formule est valide en logique intuitionniste si et seulement si est valide dans la logique modale S4 classique (c'est-à-dire valide sur les modèles de Kripke réflexif et transitif).

Complexité algorithmique des problèmes de décision en logique intuitionniste[modifier | modifier le code]

Le problème de la décision de la satisfiabilité et le problème de la décision de la validité en logique propositionnelle intuitionniste sont PSPACE-complets[17]. D'ailleurs, ils restent PSPACE-complets même si on restrait les formules à deux variables[18].

Références[modifier | modifier le code]

  1. Stanford Encyclopedia of Philosophy: "Intuitionistic Logic"—by Joan Moschovakis.
  2. Glivenko, V., 1928, “Sur la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 14: 225–228.
  3. Kurt Godel, K. Collected Works, Vol. III , Oxford: Oxford University Press (1995)
  4. Andreï Kolmogorov, "On the principle of the excluded middle" (1925) in Jean van Heijenoort, 1967. A Source Book in Mathematical Logic, 1879–1931. Harvard Univ. Press: 414–37.
  5. Ceci est dû au fait qu'une formule de logique intuitionniste qui représente une formule de logique classique est plus complexe.
  6. Gerhard Gentzen (trad. R. Feys et J. Ladrière), Recherches sur la déduction logique [« Untersuchungen über das logische schließen »], Presses Universitaires de France, , p. 4-5.
    Traduit et commenté
  7. a et b (en) « Kurt Gödel, 2.5.3 Intuitionistic Propositional Logic is Interpretable in S4 »
  8. Les Métamorphoses du calcul. Une étonnante histoire de mathématiques, Paris, Édition Le Pommier, coll. « Essais », , 223 p. (ISBN 978-2-7465-0324-3)
  9. a et b Joseph Vidal-Rosset, « Intuitionnisme », Université de Nancy 2,‎ (sur l’interprétation des expressions et la philosophie).
  10. Autrement dit, on ne peut pas définir, comme en logique classique, tous les connecteurs à partir d'un ou deux connecteurs de base.
  11. a, b, c et d Saul A. Kripke, Semantical Analysis of Intuitionistic Logic I, Elsevier, coll. « Formal Systems and Recursive Functions », (lire en ligne), p. 92–130
  12. a et b R.David, K.Nour, C.Raffalli, Introduction à la logique : Théorie de la démonstration - Cours et exercices corrigés, Dunod, , p. 159 "l'ordre sur le temps"
  13. Structure and Logic, Springer Universitext, 1980. ISBN 3-540-20879-8
  14. Structure and Logic, Springer Universitext, 1980. ISBN 3-540-20879-8
  15. Franck Wynen, « La logique intuitionniste », CNAM,‎ 2000-2001 (sur l’épistémologie et l’histoire de la logique intuitionniste de Platon au XXe siècle).
  16. Michel Lévy, « Traduction de la logique intuitioniste en logique modele », sur LIG,‎ .
  17. Richard Statman, « Intuitionistic propositional logic is polynomial-space complete », Theoretical Computer Science, vol. 9,‎ , p. 67–72 (DOI 10.1016/0304-3975(79)90006-9, lire en ligne)
  18. (en) M. Rybakov, « Complexity of intuitionistic and Visser's basic and formal logics in finitely many variables », Proceedings of Advances in Modal logic,‎

Annexes[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

Ouvrages[modifier | modifier le code]

Liens externes[modifier | modifier le code]

Articles connexes[modifier | modifier le code]