Logique minimale

La logique minimale, amputée du traitement de la négation, n'est pas si éloignée de la logique classique ou de la logique intuitionniste. On montre en effet que pour toute formule A, il existe une formule A' équivalente à A en logique classique, telle que A est prouvable en logique classique si et seulement si A' est prouvable en logique minimale. A' est obtenue au moyen de la traduction de Gödel, définie inductivement comme suit :

${\displaystyle \bot '=\bot }$

${\displaystyle p'=\lnot \lnot p}$ pour toute formule atomique différente de ${\displaystyle \bot }$

${\displaystyle (\lnot A)'=\lnot A'}$

${\displaystyle (A\land B)'=A'\land B'}$

${\displaystyle (A\to B)'=A'\to B'}$

${\displaystyle (A\lor B)'=\lnot \lnot (A'\lor B')}$

${\displaystyle (\forall x\;A)'=\forall x\;A'}$

${\displaystyle (\exists x\;A)'=\lnot \lnot \exists x\;A'}$

Autrement dit, la traduction de Gödel d'une formule consiste à ajouter des doubles négations devant les formules atomiques, les disjonctions et les quantificateurs existentiels. Cela signifie qu'en logique classique, il suffit de faire appel à des raisonnements par l'absurde seulement devant des formules atomiques, des disjonctions ou des quantificateurs existentiels.

Par exemple, le tiers exclu ${\displaystyle A\lor \lnot A}$ est un théorème de la logique classique, mais pas de la logique minimale. Par contre, la formule ${\displaystyle \lnot \lnot (\lnot \lnot A\lor \lnot \lnot \lnot A)}$ est démontrable en logique minimale. En effet, celle-ci est équivalente, en logique minimale, à ${\displaystyle \lnot \lnot (\lnot \lnot A\lor \lnot A)}$ ou à ${\displaystyle \lnot (\lnot \lnot \lnot A\land \lnot \lnot A)}$ ou encore à ${\displaystyle \lnot \bot }$, c'est-à-dire à ${\displaystyle \bot \to \bot }$ qui est une formule valide.

Dans les trois logiques (minimale, intuitionniste, classique), on dispose des deux règles suivantes, relatives à la négation :

• La règle d'élimination de la négation : si on a à la fois une proposition ${\displaystyle A}$ et sa négation ${\displaystyle \lnot A}$, alors on a une contradiction, que l'on notera ${\displaystyle \bot }$;

${\displaystyle {\frac {A\qquad \neg A}{\bot }}}$

• La règle d'introduction de la négation : si une proposition ${\displaystyle A}$ conduit à une contradiction, alors c'est que ${\displaystyle \lnot A}$ est un théorème[2]. Cette règle peut d'ailleurs être prise comme définition de la négation : ${\displaystyle \lnot A}$ est un synonyme de ${\displaystyle A\to \bot }$.

${\displaystyle {\frac {\neg A}{A\to \bot }}}$

en effet ${\displaystyle A}$ conduit à une contradiction est ${\displaystyle A\to \bot }$ et ${\displaystyle \neg A}$ est ${\displaystyle A\to \bot }$.

Les trois logiques diffèrent sur les conséquences à tirer d'une contradiction.

• La logique classique utilise le raisonnement par l'absurde et déduit de ${\displaystyle \lnot A\to \bot }$ le fait que ${\displaystyle A}$ est valide. C'est en fait une règle d'élimination de la double négation, puisque ${\displaystyle \lnot A\to \bot }$ est un synonyme de ${\displaystyle \lnot \lnot A}$.
• La logique intuitionniste déduit d'une contradiction n'importe quelle proposition : ${\displaystyle \bot \to B}$, ce qu'on résume par le principe d'explosion: ex falso sequitur quodlibet (d'une contradiction, on en déduit ce que l'on veut).
• La logique minimale ne prévoit aucun traitement lié à ${\displaystyle \bot }$ : lorsque l'on arrive à une contradiction ou à un résultat absurde, on ne peut rien en déduire.

Il en résulte que la logique minimale n'établit pas de différence entre la formule ${\displaystyle \bot }$ et n'importe quelle autre formule. Considérons par exemple une formule quelconque ${\displaystyle C}$. Définissons ${\displaystyle \sim A}$ comme synonyme de ${\displaystyle A\to C}$. On a alors :

• Si on a à la fois ${\displaystyle A}$ et ${\displaystyle \sim A}$, alors on a ${\displaystyle C}$. En effet, de ${\displaystyle A}$ et de ${\displaystyle A\to C}$, on peut déduire ${\displaystyle C}$. C'est la règle du modus ponens ;
• Si une proposition ${\displaystyle A}$ conduit à ${\displaystyle C}$, alors on a ${\displaystyle A\to C}$ et donc ${\displaystyle \sim A}$.

On voit donc que, si on n'attribue aucun rôle particulier à la contradiction, on peut faire jouer le rôle de cette contradiction à n'importe quelle formule ${\displaystyle C}$, en définissant la négation comme étant ${\displaystyle A\to C}$, et qu'inversement, on peut supprimer toute référence à la négation en logique minimale.

Par souci de comparaison avec les autres logiques, nous continuerons néanmoins à utiliser les symboles ${\displaystyle \lnot }$ et ${\displaystyle \bot }$.

Exemple 1 : ${\displaystyle (\lnot A\land \lnot B)\leftrightarrow \lnot (A\lor B)}$

En effet, supposons qu'on ait ${\displaystyle \lnot A\land \lnot B}$ (autrement dit, on a à la fois ${\displaystyle \lnot A}$ et ${\displaystyle \lnot B}$). Montrons que l'on a ${\displaystyle \lnot (A\lor B)}$, autrement dit, montrons que l'hypothèse ${\displaystyle A\lor B}$ conduit à une contradiction. Distinguons les cas : soit on a ${\displaystyle A}$ qui est bien contradictoire avec l'hypothèse ${\displaystyle \lnot A}$, ou bien on a ${\displaystyle B}$ qui est contradictoire avec ${\displaystyle \lnot B}$. Dans tous les cas, on a une contradiction, CQFD.

Réciproquement, supposons que l'on ait ${\displaystyle \lnot (A\lor B)}$ et montrons que l'on a ${\displaystyle \lnot A}$, autrement dit que ${\displaystyle A}$ conduit à une contradiction. Mais ${\displaystyle A}$ entraîne ${\displaystyle A\lor B}$ qui est contradictoire avec l'hypothèse. CQFD. On procède de même pour montrer ${\displaystyle \lnot B}$.

Par contre, on a seulement ${\displaystyle (\lnot A\lor \lnot B)\to \lnot (A\land B)}$, la réciproque étant seulement vraie en logique classique.

Exemple 2 : ${\displaystyle A\to \lnot \lnot A}$

Supposons qu'on ait ${\displaystyle A}$. Alors l'hypothèse supplémentaire ${\displaystyle \lnot A}$ conduit à une contradiction. On a donc ${\displaystyle \lnot \lnot A}$. CQFD

La réciproque n'est pas démontrable en logique minimale et en logique intuitionniste. On dispose cependant de ${\displaystyle \lnot \lnot \lnot A\to \lnot A}$. En effet, supposons que ${\displaystyle \lnot \lnot \lnot A}$. L'hypothèse supplémentaire ${\displaystyle A}$ entraîne ${\displaystyle \lnot \lnot A}$ qui est contradictoire avec ${\displaystyle \lnot \lnot \lnot A}$, donc on a ${\displaystyle \lnot A}$.

Exemple 3 : On peut montrer la démonstrabilité en logique minimale de ${\displaystyle \lnot \lnot (A\to B)\to (\lnot \lnot A\to \lnot \lnot B)}$. Mais la réciproque est seulement démontrable en logique intuitionniste ou en logique classique.

Exemple 4 : En ce qui concerne la contraposition, on peut montrer qu'en logique minimale, on a ${\displaystyle (A\to B)\to (\lnot B\to \lnot A)}$, ainsi que ${\displaystyle (A\to \lnot B)\to (B\to \lnot A)}$ et ${\displaystyle (\lnot A\to \lnot B)\to (B\to \lnot \lnot A)}$, mais on ne dispose pas de ${\displaystyle (\lnot A\to \lnot B)\to (B\to A)}$ qui est une variante du raisonnement par l'absurde.

Exemple 1 : La formule ${\displaystyle \lnot \lnot A\to A}$ n'est pas démontrable en logique minimale. En effet, si elle était prouvable, alors on pourrait prouver également, en remplaçant ${\displaystyle \bot }$ par une proposition quelconque ${\displaystyle C}$ que ${\displaystyle ((A\to C)\to C)\to A}$, or cette dernière formule n'est pas même prouvable en logique classique, sans hypothèse supplémentaire sur ${\displaystyle C}$.

Exemple 2 : La formule ${\displaystyle (\lnot A\lor B)\to (A\to B)}$ est démontrable en logique intuitionniste et en logique classique, mais pas en logique minimale. En effet, une preuve demanderait de supposer ${\displaystyle \lnot A\lor B}$ et d'en déduire ${\displaystyle A\to B}$, et donc de supposer ${\displaystyle A}$ et d'en déduire ${\displaystyle B}$. L'utilisation de ${\displaystyle \lnot A\lor B}$ par disjonction des cas et de ${\displaystyle A}$ pour prouver ${\displaystyle B}$ demanderait de prouver que ${\displaystyle \lnot A}$ et ${\displaystyle A}$ prouvent ${\displaystyle B}$, et que ${\displaystyle B}$ et ${\displaystyle A}$ prouvent ${\displaystyle B}$. Mais la preuve de ${\displaystyle B}$ à partir de ${\displaystyle \lnot A}$ et ${\displaystyle A}$ n'existe pas en logique minimale. Elle existe en logique intuitionniste, puisque, de la contradiction ${\displaystyle A\land \lnot A}$, on peut déduire ${\displaystyle B}$.