De quelques logiciens pré-modernes

Il était une fois, en des temps lointains, un monde où les gens avaient (et ont toujours, heureusement !) des opinions différentes. Il y avait deux sortes d’humains, ceux qui parlaient et ceux qui écoutaient. Ceux qui parlaient voulaient convaincre ceux qui écoutaient, et ceux qui écoutaient voulaient savoir qui parmi eux disait la vérité.

En des temps encore plus lointains, c’était beaucoup plus facile. Si un de ceux qui écoutaient n’était pas d’accord avec un de ceux qui parlaient, ce dernier tapait celui qui écoutait jusqu’à ce que celui-ci soit d’accord. Et si deux personnes qui parlaient n’étaient pas d’accord, alors ils se tapaient dessus et le plus fort avait raison. Mais bon, que voulez-vous, depuis la civilisation ce n’est plus possible.

Au fil du temps, ceux qui écoutaient ont choisi de se réunir pour discuter de la façon de reconnaître les choses vraies des choses fausses. Ils se sont d’abord aperçus qu’il y avait des vérités indéniables, comme « le ciel est bleu », « l’eau mouille », « si je lâche une pierre du haut d’une falaise, elle tombe », « recevoir une pierre sur la tête ça fait mal » ... Et là quelqu’un s’est écrié : « Si je lâche une pierre du haut d’une falaise et que quelqu’un se trouve en bas de la falaise à ce moment-là, il aura très mal !!! J’invite ceux qui ne sont pas d’accord à faire l’expérience ». C’est alors qu’ils ont pris conscience qu’à partir de vérités indéniables, on pouvait construire d’autres vérités indéniables. Ils se sont mis alors à discuter des règles qui permettent de faire cela. C’est comme ça qu’est apparue ce qu’on appelle la logique.

Et ceux qui parlaient ont trouvé qu’avec la logique il était plus facile de convaincre ceux qui écoutaient. Car en partant de vérités indéniables et en appliquant des règles de logique on ne pouvait arriver qu’à une autre vérité indéniable. Mais malheureusement il y avait des gens qui n’étaient pas d’accord sur les règles de logique à utiliser ; et d’autres qui n’étaient pas d’accord sur les vérités indéniables. Ceci a marqué le début de l’ère Argumentaire (et la fin de l’ère Bastonnaire). Il y a donc des personnes qui cherchent à savoir quelles propositions sont des vérités indéniables, on les appelle « les philosophes ». Il y a aussi ceux qui cherchent à savoir quelles règles peuvent légitimement être appliquées, on les appelle « les logiciens ». Et enfin il y a ceux qui, étant données certaines règles, et étant données certaines vérités indéniables (parfois appelées plus communément « axiomes »), cherchent à savoir quelles sont toutes les vérités que l’on peut en déduire, on les appelle « les mathématiciens ».

Où la logique s’introduit comme une mécanique de pensée

Les logiciens considèrent une proposition comme une phrase à laquelle on peut donner une valeur de vérité. Par exemple « le ciel est rouge » est une proposition car on peut dire « oui, c’est vrai » ou alors « ah non, c’est absolument faux ». Voir aussi « qui sait ? ». Mais pas toutes les phrases : les phrases interrogatives ou impératives, par exemple, ne sont pas considérées comme des propositions. En effet, à quelqu’un qui demande « pourquoi les poules n’ont pas de dents ? », ça n’a aucun sens de lui répondre « ce que tu viens de dire est complètement faux », ou à quelqu’un qui nous dit « passe-moi le sel ! » une réponse du genre « mais c’est parfaitement vrai ce que tu me dis là » n’a aucun sens.

En fait, les logiciens ne s’occupent pas du sens des propositions, ils les considèrent comme des objets abstraits nommés généralement A, B, ... Autant dire qu’ils se moquent bien de ce qu’elles peuvent vouloir dire. Et pour construire de nouvelles propositions à partir de propositions qui existent déjà, les logiciens utilisent des opérateurs logiques :

• L’opérateur et : Si on a deux propositions A, B, alors on peut construire une troisième proposition A et B, et ça se note $A \wedge B$.
• L’opérateur ou : il fonctionne comme l’ opérateur et, le ou du logicien est inclusif, ça veut dire que A ou B signifie soit A, soit B, ou les deux, et ça se note $A\vee B$.
• L’opérateur non permet de construire la négation d’une proposition A, on le note $\neg A$.
• L’opérateur implique : de même avec deux propositions A et B, on peut faire la proposition A implique B, ce qui signifie que Si on a A alors on a B. Et ça se note $A\rightarrow B$.

Maintenant il faut se mettre d’accord sur ce que signifie pour une proposition d’être Vraie ou Fausse. Une proposition est Fausse si sa négation est Vraie, c’est-à-dire que A est Fausse si $\neg A$ est Vraie. Et une proposition est Vraie si on peut la démontrer, c’est-à-dire la prouver en utilisant un certain nombre de règles et d’axiomes à établir.

On attribue alors à chaque opérateur des règles qui permettent de dire comment prouver les propositions qui utilisent ces opérateurs, et comment en déduire certaines propositions. Par exemple, si à chaque fois que « je fais une omelette », alors « je casse des œufs » on a la proposition « je fais une omelette implique je casse des œufs » qui est Vraie. Ce qui correspond à la règle « Si on admet A comme étant Vraie et qu’on a alors B, alors on a A implique B ». Et si « je fais une omelette implique je casse des œufs » est Vraie et que je fais effectivement une omelette alors il est vrai que je casse des œufs. Ce qui fait une deuxième règle pour l’opérateur implique : « Si on a A, et A implique B alors on a B ».

Chacun des opérateurs logiques a ainsi des règles qui permettent de déduire certaines propositions à partir d’autres.

Notons qu’à partir d’une proposition Fausse, on peut démontrer n’importe quoi !
Par exemple, si je suppose que 2 + 2 = 5 alors je peux montrer des trucs vrais : comme 2 + 2 = 4 (en effet, si 2 + 2 = 5, on a 2 = 3 en enlevant 2 de chaque côté, donc 4 = 5 en ajoutant 2 fois 2 de chaque côté, donc 2 + 2 = 4), mais aussi des trucs faux (de 2 = 3 on déduit 0 = 1 en enlevant 2 de chaque côté), à partir de là je peux aussi montrer que tous les nombres sont égaux entre eux, en effet, en multipliant par N de chaque côté de l’égalité 0 = 1 on obtient pour tout N, 0 = N. Et là c’est une hécatombe, c’est la fin de l’humanité car s’il y a 7 milliards d’êtres humains sur Terre, comme 7 milliards est égal à zéro alors il n’y a plus d’être humain sur Terre, et en faisant le même raisonnement avec le nombre d’atomes dans l’univers alors c’est aussi la fin de tout. Mais ne soyons pas tellement sinistres, je peux montrer aussi des choses bien comme par exemple que je suis Zeus ; en effet, Zeus et moi sommes deux entités différentes, mais comme 2 = 1 alors nous sommes une seule et même entité et donc à partir de là je peux décréter que toutes les propositions sont Vraies ... Euh, j’espère que cela a convaincu les plus réticents sur le fait que si on suppose une chose Fausse alors on peut vraiment démontrer n’importe quoi.

À partir de là, on peut se donner une proposition toujours Fausse que l’on va appeler « FAUX ». Une telle proposition existe, on peut prendre par exemple la proposition « Vrai = Faux ». Le lecteur attentif aura astucieusement remarqué que l’on n’a pas donné de règle pour l’opérateur non. Voyons donc quand non A est Vraie. Dire que non A est Vraie, c’est dire que si on arrive à prouver A on a alors une contradiction (car A serait à la fois Vraie et Fausse). Autrement dit, non A est Vraie, ça veut dire que $A\rightarrow \hbox{FAUX}$.

Surgissent alors deux logiques selon le paradigme choisi

Voilà donc les fournitures scolaires de la majorité des logiciens. Parmi cette majorité on va s’intéresser à deux écoles particulières. Il y a l’école dite classique (plutôt des mathématiciens) et l’école dite intuitionniste (plutôt des informaticiens). Ce qui les différencie principalement est une proposition appelée principe du tiers exclu qui dit que si A est une proposition alors soit A est Vraie, soit A est Fausse (et donc $\neg A$ est Vraie) autrement dit on a la proposition $A\vee \neg A$. On parle de tiers exclu car cela revient à dire qu’une proposition ne peut avoir que deux valeurs de vérité : Vrai ou Faux, et qu’il n’existe pas de tierce possibilité.

Comme vous n’avez pas manqué de le remarquer, cette proposition ne peut être démontrée en utilisant les règles des opérateurs définis plus haut. Pour les logiciens classiques, c’est une proposition évidente qui peut donc se passer de démonstration, ils la posent donc comme axiome. Par contre, les logiciens intuitionnistes considèrent comme Vraies uniquement les propositions dont on peut construire la preuve à partir des règles définies pour les opérateurs ; et ce n’est pas le cas du principe du tiers exclu. Il n’est donc pas considéré comme Vrai. Il n’est pas non plus considéré comme Faux. Pour les intuitionnistes, une proposition peut donc aussi être indécidable, c’est-à-dire qu’on ne peut pas montrer qu’elle est Vraie, et on ne peut pas montrer non plus qu’elle est Fausse.

En fait en logique classique on a aussi des propositions indécidables mais à un niveau différent, c’est-à-dire si on utilise la logique classique pour faire de l’arithmétique, on aura quand même des propositions d’arithmétique indécidables, c’est le célèbre théorème de Gödel qui a bouleversé le monde des mathématiques . . . mais c’est une autre histoire !

Pour illustrer cela on pourrait imaginer que les valeurs de vérité d’une proposition sont décidées par référendum (seuls les votes accompagnés de démonstrations sont comptabilisés). Les logiciens classiques n’ont que deux bulletins de vote possibles : un bulletin Vrai et un bulletin Faux, alors que les logiciens intuitionnistes, eux ont en plus le droit au vote blanc.

Il se trouve que le tiers exclu est indécidable, mais on peut prouver (non non le tiers exclu), ce qui signifie que celui-ci n’est pas faux. J’entends déjà quelques réflexes d’école, « mais une double négation, c’est une affirmation ! Donc non non le tiers exclu c’est la même chose que le tiers exclu ! ». Que nenni, car le fait que pour une proposition A on ait non non A implique A est une conséquence . . . du principe du tiers exclu (amusez-vous à déduire du tiers exclu que $\neg\neg A\rightarrow A$, mais aussi que si cela est vrai pour toute proposition A alors cela entraine le tiers exclu).

Le logicien intuitionniste interprèterait la double négation plutôt de la manière suivante. Si on se rappelle que $\neg A$ signifie $A\rightarrow \hbox{ FAUX}$, alors $\neg\neg A$ signifie que le fait que « A implique une contradiction » implique lui-même une contradiction. Autrement dit, s’il existait une preuve de A, elle n’apporterait aucune contradiction. Mais cela ne signifie pas qu’il existe effectivement une preuve de A. Dans ce cas A n’est pas Vraie (ni Fausse).

Pour reprendre notre histoire de scrutin, si le logicien classique prouve $\neg\neg A$ alors il a éliminé le bulletin Faux, et il vote donc Vrai.
Alors que si le logicien intuitionniste a éliminé le bulletin Faux, il lui reste deux choix : voter blanc ou voter Vrai. Pour voter Vrai il est obligé de trouver une preuve de la proposition A pour que son vote soit pris en compte. S’il n’en existe pas, alors il votera blanc. Donc une preuve de $\neg\neg A$ n’est pas une preuve de A, ça nous permet seulement de supprimer le bulletin Faux pour le vote de la valeur de vérité de la proposition A.

De l’utilisation et de quelques conséquences du tiers exclu

L’axiome du tiers exclu permet de faire des raisonnements qui facilitent parfois les démonstrations de certaines propositions. Ces raisonnements ne sont pas valides en logique intuitionniste car ils ne permettent pas de construire des preuves à partir des règles. Voici quelques exemples :

• Le raisonnement par l’absurde :
  Pour montrer qu’une proposition A est Vraie, on peut supposer que $\neg A$ est Vraie et en déduire une proposition B dont on sait qu’elle est Fausse. Ainsi en supposant $\neg A$ et en prouvant FAUX, on a prouvé que $\neg A\rightarrow \hbox{FAUX}$, autrement écrit, on a prouvé $\neg\neg A$ et donc A.
  • Exemple : J’ai mangé une omelette ce midi, et je veux montrer que j’ai moins d’œufs dans mon armoire que ce matin. Supposons par l’absurde que ce n’est pas le cas, c’est-à-dire que j’ai autant ou plus d’œufs que ce matin. Comme je n’ai pas été faire de courses aujourd’hui, il est impossible que j’en aie plus, j’en ai donc autant. Cela signifie que j’ai fait mon omelette ce midi sans casser d’œufs, ce qui est absurde ! La supposition selon laquelle j’ai plus ou autant d’œufs que ce matin est donc erronée, j’ai donc moins d’œufs que ce matin.

• L’implication :
  Dire que l’on a $A\rightarrow B$, c’est la même chose que dire que l’on a $\neg A\vee B$. En effet, si on a $A\rightarrow B$ alors, d’après l’axiome du tiers exclu, soit on a A et alors comme on a aussi $A\rightarrow B$, on a B et donc on a $\neg A\vee B$, soit on a $\neg A$ et donc on a $\neg A\vee B$. Et si on a $\neg A\vee B$ alors soit on a $\neg A$, et cela signifie que si l’on suppose que A est Vraie alors on a une contradiction et donc on a B qui est Vraie. Si on lit ce qui est en gras cela veut dire que $A\rightarrow B$. Soit on a B et alors on a forcément $A\rightarrow B$.
  • Exemple : Eh oui, dans la vie soit on ne fait pas d’omelettes, soit on casse des œufs !

• Le raisonnement par contraposition :
  Un autre raisonnement typique de la logique classique est le raisonnement par contraposition. Si on a la proposition $A\rightarrow B$, alors on appelle sa contraposée la proposition $\neg B\rightarrow \neg A$.
  Si on a $\neg B\rightarrow \neg A$ alors d’après le paragraphe ci-dessus on a $\neg\neg B\vee \neg A$, c’est-à-dire $B\vee \neg A$, autrement dit $\neg A\vee B$, soit $A\rightarrow B$. Cela signifie que la proposition $A\rightarrow B$ est équivalente à sa contraposée.
  Donc pour prouver que $A\rightarrow B$ est Vraie on peut prouver sa contraposée, c’est-à-dire supposer que l’on a $\neg B$, et chercher à prouver $\neg A$.
  • Exemple : Je n’ai pas cassé d’œufs, donc je n’ai pas fait d’omelettes ! [1]

• Les lois de De Morgan : Il y a deux lois de De Morgan [2] :
  • i) $\neg(A\wedge B)$ c’est la même chose que $\neg A \vee\neg B$.
  • ii) $\neg(A\vee B)$ c’est la même chose que $\neg A \wedge\neg B$.
• En effet :
  • i) Si non (A et B) est Vraie, ça veut dire que A et B est Fausse, ce qui veut dire que au moins l’une des propositions A ou B est Fausse ; autrement dit, au moins l’une des propositions $\neg A$ ou $\neg B$ est Vraie et donc $\neg A$ ou $\neg B$ est Vraie.
    • Exemple : Ce soir je ne veux pas de l’entrée et du dessert. C’est-à-dire que, comme je suis au régime, soit je ne prends pas d’entrée, soit je ne prends pas de dessert (ou même aucun des deux si je n’est pas très faim). (non (entrée et dessert) = non entrée ou non dessert)
  • ii) Si non (A ou B) est Vraie, ça veut dire que A ou B est Fausse, ce qui veut dire que ni A est Vraie et ni B est Vraie ; autrement dit $\neg A$ et $\neg B$ sont Vraies donc on a $\neg A$ et $\neg B$.
    • Exemple : Je ne veux pas de poule ou de légumes, ça veut dire que je veux ni de la poule, ni des légumes (oui, je sais, c’est difficile comme régime) [3]. (non (poule ou légumes) = non poule et non légumes).

En logique intuitionniste, comme on a un axiome en moins, on a quelque chose de moins contraint, et donc de plus général. Donc tout ce qui est vrai en logique intuitionniste, est encore plus vrai en logique classique. L’idée de la logique intuitionniste est de faire des raisonnements constructifs, c’est-à-dire qu’à partir de nos hypothèses, on construit une preuve du résultat que l’on veut démontrer en utilisant seulement les règles des opérateurs. Tandis que l’axiome du tiers exclu permet d’éviter cette construction. En mathématiques, il faut dire ce qui est Vrai, l’axiome du tiers exclu n’est pas contradictoire et n’est pas aberrant non plus, il permet au mathématicien d’accéder à certains résultats et d’avancer dans la théorie. Mais en informatique il faut construire les preuves de manière algorithmique. Pour l’informaticien un objet existe seulement si il y a un algorithme qui permet de le calculer, donc l’utilisation de la logique intuitionniste lui assure que les objets sur lesquels il faits des preuves peuvent bien être obtenus par un algorithme.

Logique classique et ordinateur : quand on calcule avec des 0 et 1

En logique classique on peut formaliser les choses avec des calculs binaires. On a vu qu’en logique classique une proposition n’avait que deux valeurs de vérité : Vrai ou Faux. On peut représenter ces valeurs de vérité par des symboles. Le plus souvent on utilise le symbole 1 pour Vrai et 0 pour Faux. Une table de vérité est un tableau qui contient toutes les valeurs possibles des propositions. Par exemple :

i) La table de vérité de $\neg$ est :

La première colonne contient toutes les valeurs possibles de A. La dernière colonne contient les valeurs de $\neg A$ selon les valeurs de A. Quand A vaut 0, $\neg A$ vaut 1 et vice-versa.

ii) La table de vérité de $\vee$ est :

Ici, quand A à la valeur 0, alors B a deux valeurs possibles, de même que lorsque A a la valeur 1. La table de vérité a donc ici quatre lignes qui correspondent aux quatre cas possibles pour les valeurs de A et de B. Et la dernière colonne contient les valeurs de $A\vee B$ selon les valeurs de A et de B.
Les plus courageux pourront aller regarder d’autres tables de vérité sur Wikipédia, à la page « Table de vérité ».

Ainsi, par exemple, si l’on veut “montrer” la proposition $A\vee\neg A$, on peut faire sa table de vérité. Pour ça on commence par la première colonne qui va donner toutes les valeurs possibles de A, ensuite on peut donner une deuxième colonne pour donner les valeurs de $\neg A$ correspondantes, comme ci-dessus. Maintenant on peut ajouter la dernière colonne (celle qui nous intéresse) qui va contenir les valeurs de vérité de $A\vee\neg A$. Dans la première ligne on voit que A vaut 0 et $\neg A$ vaut 1. La deuxième ligne de la table de vérité de $\vee$ nous dit qu’alors $A\vee\neg A$ vaut 1. Si on fait pareil pour la deuxième ligne, on obtient la table de vérité suivante :

On voit ici que la dernière colonne ne contient que des 1 et donc que la proposition est toujours Vraie quelles que soient les valeurs de la proposition A.

Nous avons donc un ensemble de symboles pour lesquels on a défini des tables de vérité à l’aide des symboles 0 et 1. Maintenant, oubliez le sens de ces symboles, et relisez la phrase précédente (repassez alors à la phrase suivante sans relire cette phrase). Vous pouvez alors vous poser la question : Quels sens pouvons nous donner à ces symboles ?

Ce qu’on a vu ci-dessus est une interprétation possible des symboles, et ce qui nous intéresse dans ce cas ce sont les propositions dont la table de vérité ne contient que des 1, ce qui correspond aux propositions Vraies de la logique classique.

Les Portes Logiques

Une autre interprétation courante de ces symboles est une interprétation physique. Le 0 et le 1 peuvent-être interprétés comme étant un état d’un fil conducteur (Par exemple 1 : le courant passe, 0 : le courant ne passe pas). Les autres symboles peuvent alors être interprétés comme ce qu’on appelle des portes logiques.

Une porte logique est un petit composant électronique qui possède en général un ou deux fils en entrée, et un fil en sortie. L’état du fil en sortie dépend de l’état des fils en entrée. Le comportement d’une porte logique est entièrement déterminé par sa table de vérité. Les portes logiques ont les mêmes noms que les opérateurs logiques. Ils ne seront pas tous présentés ici. Vous pouvez les trouver dans Wikipédia, à la page « Fonction logique ».

Pour les représenter, il existe plusieurs normes, j’ai choisi ici la norme européenne.

i) La porte et :

Ici l’état de la sortie est 1 si l’état de l’entrée A est 1 et l’état de l’entrée B est 1.

ii) La porte non :

Si l’entrée A est à l’état 0 alors la sortie est à l’état 1 (c’est-à-dire $\neg A$). Et inversement, si l’entrée A est à l’état 1 alors la sortie est à l’état 0. En fait ici c’est le petit rond après le rectangle qui désigne la négation. De manière générale au lieu de dessiner une porte logique suivie d’une porte non, on ajoute simplement un petit rond pour indiquer la négation. Par exemple la porte qui a comme entrées A et B et qui rend en sortie $\neg(A\wedge B)$ s’appelle la porte non-et, et est représentée par la porte et suivie d’un petit rond.

On peut faire une porte logique qui correspond à la table de vérité de $\rightarrow$, à l’aide de portes non et ou, en remarquant que $A \rightarrow B$ est la même chose que $\neg A\vee B$.

On peut assembler plusieurs portes logiques pour faire ce qu’on appelle un circuit logique. Ces circuits peuvent définir de nouvelles portes logiques. Par exemple, vous connaissez pour l’instant la porte logique et. On a vu que A∨B signifie soit A, soit B ou les deux. Il existe un autre opérateur que l’on appelle ou exclusif qui veut dire soit A, soit B mais pas les deux. On peut définir cet opérateur comme $(A\vee B)\wedge\neg(A\wedge B)$, et à partir d’une formule comme ça il est facile de trouver le circuit correspondant (le $\ge 1$ désigne la porte logique ou) :

Sur le schéma, le croisement n’est pas un vrai croisement, il y a un fil qui passe par dessus l’autre. Vous pouvez facilement trouver la table de vérité de cet opérateur. Pour vérifier sur un exemple, imaginons que A et B sont à l’état 1, que le courant se propage dans tous les fils jusqu’à ce qu’il rencontre des portes logiques. Les deux entrées de la porte logique du bas sont à 1, donc la porte et rend en sortie 1, mais il y a le petit rond (porte non) qui transforme ce 1 en 0. La porte ou reçoit également deux 1 en entrée, elle retourne alors 1 en sortie. Donc la dernière porte et a d’une part une entrée à l’état 0 et d’autre part une entrée à l’état 1, sa sortie est donc à l’état 0.

Il y a plein de propriétés très simples et amusantes qui relient ces calculs logiques et l’électronique. Par exemple, en s’amusant un peu avec les lois de De Morgan (ou en faisant des tables de vérité) on peut remarquer que :

• $A\vee B$ est équivalent à $\neg(\neg A\wedge\neg B)$.
• $A\wedge B$ est équivalent à $\neg(\neg A\vee\neg B)$.

Et donc la porte ou peut être obtenue à partir de portes non et de portes et. En fait avec seulement la porte non et l’une des deux portes et - ou on peut faire n’importe quel circuit logique voulu.

Mais avec des circuits logiques on peut faire aussi des choses un peu plus intéressantes. Si on se rappelle, par exemple, que 0 et 1 peuvent être simplement des chiffres en base deux, on peut par exemple faire un circuit qui pour les entrées prend comme états les chiffres d’un nombre en base deux et qui en sortie donne les chiffres en base deux du nombre suivant (autrement dit un circuit qui prend un nombre et qui lui ajoute un) :

La porte logique avec un =1 est un ou exclusif. Ici on ne considère que les nombres à deux chiffres. L’entrée A représente le chiffre des « deuzaines » et l’entrée B le chiffre des unités du nombre de départ. La sortie en haut représente le chiffre des deuzaines et la sortie en bas le chiffre des unités du résultat.

Les nombres à deux chiffres en base deux sont dans l’ordre 00, 01, 10, 11. Comme le résultat a aussi deux chiffres il retourne 00 pour 11 (Un peu comme un compteur kilométrique qui ne contient que des 9 et qui se remet à zero au kilomètre suivant).

Vous pouvez remarquer que le chiffre des unités alterne d’un nombre à l’autre, c’est-à-dire que si le chiffre des unité d’un nombre est 0 alors le chiffre des unité du nombre suivant est 1 et vice-versa. Donc le rôle de la porte non en bas est d’avoir cette alternance du chiffre des unités. La porte logique du haut est un ou exclusif et nous donne en sortie le chiffre des « deuzaines ».

Mais on peut faire des circuits un peu plus compliqués qui permettent d’additionner deux nombres, de les soustraires, de les multiplier, etc. Et si on se rappelle qu’une suite de 0 et de 1 peut aussi représenter un texte, une couleur, une image, un son, ... (voir ici) alors avec les circuits logiques on peut faire des machines qui permettent de traiter ces informations. C’est cette idée géniale de la multi-interprétation de 0 et 1 qui fait que les portes logiques nous donnent accès au monde de l’informatique.

Les règles formelles de la logique.

Pour décrire plus formellement une logique, on utilise des règles qui ressemblent au truc ci-dessous :

Sur ce dessin on a une barre horizontale qui sépare les hypothèses de la conclusion. Si tout ce qu’il y a au-dessus de la barre est vérifié alors ce qui est en dessous l’est aussi. Bref, si on a C_1, C_2, ... , C_n, alors on en déduit C_0. Mais il y a une subtilité de plus. Toutes les expressions sont de la forme $\Gamma\vdash C$. Ce qu’il y a à gauche du $\vdash$ est un environnement. C’est le contexte dans lequel la proposition de droite est exprimée. Un environnement est une liste de propositions qui détermine le contexte dans lequel la propositon $C$ est Vraie. Autrement dit $\Gamma$ est une sorte de boîte à outils qui contient toutes les propositions que l’on peut utiliser pour prouver la proposition de droite.

On a déjà vu plus haut les règles des opérateurs logiques. Ici ce sont les mêmes règles, mais exprimées de manière formelle comme décrit ci-dessus. Je vais donc en montrer ici seulement quelques-unes, le lecteur courageux pourra essayer d’écrire lui-même celles qui manquent, et le lecteur moins courageux pourra aller les regarder dans Wikipédia aux pages « Calcul des propositions » ou « Logique intuitionniste ».

• Voici une des règles de l’implication : Cette règle dit que pour prouver $A\rightarrow B$ avec une boîte à outils $\Gamma$ , il suffit de pouvoir prouver B en rajoutant une preuve de A dans la boîte à outils.

• Les règles de l’opérateur et :

La première règle dit que si avec une boîte à outils $\Gamma$, je peux prouver A et qu’avec cette même boîte à outils je peux prouver B alors avec ces mêmes outils je peux prouver $A\wedge B$. Toutes les autres règles peuvent se lire de la même manière.

• La règle de FAUX : On a vu plus haut que FAUX est une proposition toujours fausse. Cette proposition est souvent notée $\bot$, et d’après ce qu’on a vu sur FAUX, on a la règle

On utilise ces règles pour faire des preuves, comme illustré sur l’exemple suivant (pour ceux qui sont encore debout) :

Une preuve consiste à construire petit à petit ce qu’on appelle un arbre de preuve.
Un arbre de preuve est une trace de toutes les règles que l’on a utilisées pour faire une preuve. Vérifier qu’un arbre de preuve est correct est quelque chose de très facile à faire. On n’a même pas besoin de connaître le sens des symboles $\wedge$, $\vee$ ou $\rightarrow$ pour faire cela. Il suffit simplement de vérifier que les règles sont appliquées correctement, autrement dit il suffit de vérifier si toutes les règles utilisées ont la bonne forme. Ce que l’on vient de voir ici est une formalisation de la logique que l’on a présentée avant. Le fait que l’on n’ait pas besoin de connaître le sens des symboles pour vérifier ou même pour faire des preuves facilite l’automatisation de ces procédures. La formalisation est le premier pas vers l’automatisation de l’acte de démonstration et de vérification de preuve.

La vérification de preuves mathématiques est une question de recherche et développement de logiciels de haut vol, par exemple le logiciel Coq sert à prouver/vérifier des théorèmes, mais c’est aussi utile pour prouver que des programmes sont valides. La belle épopée narrée ici donne une idée de ce que l’on fait avec ce genre de logiciel.

En savoir plus :

Un logiciel qui utilise la logique intuitionniste pour la déduction naturelle : Panda

Sur Interstices, l’article « La vérité et la machine » qui donne un exemple de preuve par ordinateur et explique la différence avec les raisonnements mathématiques standards ; l’article « Preuves formelles, preuves calculatoires » qui présente les méthodes formelles issues de la logique de type intuitionniste ; l’article « Alan Turing du calculable à l’indécidable » qui explique plus en détail les notions d’indécidabilité.