Logique intuitionniste - Définition

Approche formelle

Nous venons de voir que l'implication et la disjonction ne sont plus liées. Mais en fait cela va plus loin : une des caractéristiques de la logique intuitionniste est le fait que chaque connecteur , l’absurde et chaque quantificateur , doit être défini à partir de ses propres règles, autrement dit il n'y a pas de moyen de ramener la logique à un connecteur et à un quantificateur. C'est pourquoi nous allons donner des règles pour chaque connecteur ainsi que pour l’absurde.

La logique implicative minimale

Pour introduire la logique intuitionniste, le plus simple est de commencer par la déduction naturelle en logique implicative minimale, qui est la logique propositionnelle dans laquelle il n'y a qu'un connecteur, l'implication .

En déduction naturelle, se lit « de l'ensemble de propositions on déduit la proposition ».

Il y a alors deux règles (voir plus bas Lecture des règles) :

.

La première règle s'appelle la règle d'élimination de l'implication, tandis que la seconde règle s'appelle la règle d'introduction de l'implication. On remarque que l'élimination de l'implication est aussi le modus ponens bien connu. La méthode qui consiste à avoir pour chaque connecteur une (ou des) règle(s) d'élimination et une (ou des) règle(s) d'introduction est typique de la déduction naturelle et nous allons la retrouver par la suite.

Ce système de déduction est très simple (rasoir d'Ockham), mais il est moins puissant que la logique classique, car on ne peut y démontrer ni la loi de Peirce ni la proposition

Lecture des règles

La règle d'élimination de l'implication peut se lire 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 ψ. Nous verrons (section interprétation de la logique intuitionniste) que l'expression « je déduis » prend un sens plus fort en logique intuitionniste qu'en logique classique. La règle d'introduction de l'implication, quant à elle, peut se lire 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 .

La logique propositionnelle intuitionniste

On conserve les règles de la logique implicative minimale concernant l'implication.

L'absurde

L'absurde est la proposition, notée , qui traduit une proposition essentiellement fausse. Elle est régie par une règle:

Cela signifie que si un ensemble de propositions Γ conduit à l'absurde, alors de cet ensemble de propositions Γ, je peux déduire n'importe quelle proposition .

Cette règle est aussi la règle d'élimination de l'absurde. Il n'y a pas (heureusement!) de règle d'introduction de l'absurde. Le nom de cette règle ne doit pas la faire confondre avec la règle de raisonnement par l'absurde (reductio ad absurdum) qui n'existe pas en logique intuitionniste. En effet le raisonnement par l'absurde est étroitement lié au tiers exclu et n'est pas constructif.

Remarque: en logique classique cette règle n'est pas utile, car elle est une conséquence du raisonnement par l'absurde.

La négation

Traditionnellement, on considère la négation comme une abréviation. Plus précisément on dit que est en fait une abréviation pour . Il n'y a donc pas de règles spécifiques à la négation.

La conjonction

On introduit un nouveau connecteur binaire , representant la conjonction de deux formules. On lit  : A et B. On lui associe deux régles d'élimination, et , et une règle d'introduction.

La disjonction

On introduit un nouveau connecteur binaire , representant la disjonction de deux formules. Il est en quelque sorte symétrique du connecteur . Ainsi, on lui 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, c'est-à-dire qu'elle a trois prémisses.

Le calcul des prédicats intuitionniste

Le calcul des prédicats intuitionniste reprend toutes les règles du calcul propositionnel intuitionniste ci-dessus et lui adjoint de nouvelles règles pour les quantificateurs "quel que soit" et "il existe". Son langage et son ensemble de formules demeurent les mêmes que ceux du calcul des prédicats classique

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

• Règle d'introduction :

Gamma |- A

----------------------

Gamma |- All x A

• Règle d'élimination :

Gamma, A[t/x] |- B

------------------------------

Gamma, All x A |- B

Le quantificateur existentiel

• Règle d'introduction :

Gamma |- A[t/x]

---------------------------

Gamma |- Exists x A

• Règle d'élimination :

Gamma, A |- B

-------------------------------

Gamma, Exists x A |- B

Exemples de différences avec la logique classique

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 soit en être faites. 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érateurs.

Negation

• 

Interprétation : « Il est démontré que A est contradictoire » (et non pas « A est Faux »).

• 

Attention : il ne faut pas en conclure que est vrai. Cela ne l’est strictement pas.

Double-négation

• 

Interprétation : « Il est prouvé qu’il est contradictoire d’affirmer que A est contradictoire », c’est à dire « Il est prouvé que A n’est pas contradictoire » (et en particulier, surtout pas « A est Vrai »).

• 

C’est à dire .

Attention : la réciproque n’est pas vraie, on a pas , ce qui explique que nous n’ayons pas non-plus .

L’expression peut s’interpréter comme « Si A est vraie, alors A n’est pas contradictoire ». La précédente remarque sur la non-validité de l’implication réciproque, s’interprète donc comme « Que A ne soit pas contradictoire, n’est encore pas assez pour nous permettre de construire une preuve que A est vraie »… A restant encore à démontrer.

Remarque : la non-contradiction de A, bien qu’insuffisante pour constituer une preuve de A, reste tout de même une condition nécessaire à cette démonstration.

Conjonction

• 

Interprétation : « Preuve que A et preuve que B » (comparable à ce qu’il en est en logique classique).

• 

C’est à dire .

Contrairement à ce qu’il en serait en logique classique, n’est seulement qu’une implication de , mais n’est pas équivalent à . En effet, l’équivalence nécessiterait d’accepter l’implication réciproque , qui permettrait d’introduire un brouillage entre A et de B (par la disjonction), dont il n’est possible de rien conclure selon le principe constructiviste, car et pourraient être simultanément vrais tout autant qu’un seul des deux, sans qu’il ne soit possible de déterminer ce qu’il en est concrètement.

Disjonction

• 

Interprétation : « Preuve que A ou preuve que B » (et en particulier, surtout pas « Preuve que A ou B »).

• 

A et B s’excluent mutuellement et ne sont pas simultanément vrai.

Comparable à ce qu’il en serait dans la logique classique de Bool et Carnaug.

Quantificateur existentiel

• 

Interprétation : « Nous savons comment créer un x et pouvons prouvez que A(x) » (et non pas « Il existe théoriquement un x vérifiant A(x) »)

• 

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).

Comparable à ce qu’il en serait en logique classique.

Quantificateur universel

• 

Interprétation : « Preuve que pour chaque x appartenant à l’ensemble spécifié, nous pouvons toujours prouver A(x) » (comparable à ce qu’il en est en logique classique).

• 

C’est à dire .

Contrairement à ce qu’il en serait en logique classique, n’est seulement qu’une implication de mais n’est pas équivalent à , car l’équivalence nécessiterait d’accepter l’implication réciproque , qui présente un cas d’attention pour l’intuitionnisme. En effet, il requiert qu’en démontrant , on fournisse un moyen de montrer également un x qui vérifie cette affirmation positive de l’existence d’un x. Si cela est nécessaire, il faudra le prouver d’une autre manière, et il ne sera pas permis de l’assimiler à une conséquence de (ce qui ne « démontrerait » que son existence théorique). Cependant, l’implication présentée plus haut reste permise.

Tiers-exclus

• 

Cette relation qui n’est pas a priori valide, peut cependant être valide ! Elle n’est seulement pas automatiquement valide, et elle n’en est pas plus automatiquement invalide. Elle est valide si nous pouvons prouver A ou prouver . Par exemple, dans , l’expression est valide, car nous pouvons toujours soit prouver (x = y), soit prouver . Si nous prouvons (x = y), alors est contradictoire ( ), ce qui est une interprétation valide. Et si nous pouvons prouver la contradiction de (x = y), qui est , en prouvant , l’interprétation est valide de même. Par contre, l’expression ne serait plus valide avec , car l’égalité ou l’inégalité entre deux réels, peut être non-calculable, c’est à dire, non-décidable (hors-arrondi, mais il ne s’agirait alors plus de véritables réels au sens mathématique du terme). Elle serait valide avec (sous réserves que ces rationnels ne soient pas représentés par des expressions de longueur infinie).

Relations entre les règles

Pour mieux comprendre, on remarquera dans ce qui précède, que contrairement à ce qu’il en est dans la logique de Bool, 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 , seuls 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 A.

Les interprétations des expressions ne se font pas dans le sens de Vrai et Faux, 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éfinis dans les termes d’une autre.