L'exposé qui suit ainsi ainsi que ceux sur le calcul des prédicats et les logiques non classiques, proviennent de notes de cours que le Professeur Jean-Louis Gardies, de la Faculté des lettres de Nantes a donnés durant l'année universitaire 1979-1980 dans le cadre d'un enseignement de philosophie et constituant un des deux modules de la Licence de Logique que délivre cette Université.
La logique classique dite aussi logique des propositions ou encore logique d'ordre zéro, date de l'antiquité et est assez bien divulguée mais principalement sous sa forme sémantique des tables de vérité et rarement sous sa forme formelle contemporaine.
Ici nous exposerons le système formel syntaxique en utilisant le formalisme peu connu de Lukasiewicz et ferons quelques calculs dans ce formalisme afin de mieux saisir pourquoi il n'est pas enseigné aux débutants.
La logique classique est le système formel le plus simple qui possède les bonnes propriétés qu'on attend d'un tel système. Il est complet, décisoire et non contradictoire. Un idéal qui ne se reproduira pas pour des systèmes plus évolués et plus utiles.
Pour décrire un système formel il faut disposer d'un langage composé d'un vocabulaire terminal, appelé aussi alphabet, d'un vocabulaire auxiliaire, d'une grammaire, d'axiomes, de règles de réécriture et de règles de déduction. Le langage décrivant la logique des propositions est composécomme suit:
{C,N,a,b,c,d,.....,p,q,r,s,t,.......} les points représentant une infinité éventuellement non dénombrable de termes.Il contient les termes premiers de la théorie.
{V,E}
V ---> a|b|c|d|.....|p|q|r|s|t|...............Les mots de ce langage obtenus par cette grammaire sont appelés Expressions Bien Formées ou EBF. En anglais on dit WFF (prononcer wouf!) pour Well Formed Formulae. V représente les variables propositionnelles. E est le point d'entrée de la grammaire. Cette grammaire tès simple est définie de manière récursive ce qui permet de décrire une infinité d'expressions dans ce langage. Signalons pour mémoire qu'en 1933 on a donné une grammaire non récursive du langage, dite grammaire descriptive.
E ---> NE|CEE|V
Ce sont les trois axiomes de Lukasiewicz. On appelle thèse une EBF qui est soit un axiome, soit déduite des axiomes par les règles suivantes.
- CCpqCCqrCpr
- CCNppp
- CpCNpq
Parfois on rajoute au système d'autres termes pour condenser l'écriture des EBF et faciliter l'utilisation du système. Dans le cas de la présentation du système de Lukasiewicz on peut rajouter les quatre termes: A,K, D et E. Mais cela oblige à rajouter de nouvelles règles d'utilisation de ces termes nouveaux.
- Règle de substitution [R1]
Si dans une thèse du système on substitue à une variable, à chacune de ses occurences, une EBF, on obtient une nouvelle thèse.- Règle de modus ponens (ou de détachement) [R2]
Si on a comme thèse du système d'une part l'expression g et d'autre part l'expression Cgh, alors on peut admettre également h comme thèse du système.
C'est-à-dire qu'on est autorisé dans une EBF à remplacer la partie gauche quand on la rencontre par la partie droite des règles de réécriture.
- Règles de remplacement ou de réécriture [R3]
CNpq --> Apq NCpNq --> Kpq CpNq --> Dpq NCCpqNCqp --> Epq
Soit à montrer Cpp ( (p) ==> (p) ):
[1] CpCNpq axiome 3 de Lukasiewicz [2] CpCNpp règle [R1], p remplace q dans [1] [3] CCpqCCqrCpr axiome 1 de Lukasiewicz [4] CCpqCCqpCpp règle [R1],CCpp remplace q dans [3] [5] CCpCNppCCCNpppCpp règle [R1],CNpp remplace q dans [4] [6] CCCNpppCpp règle [R2], détachement C[2] - [6] [7] CCNppp axiome 2 de Lukasiewicz [8] Cpp règle [R2], détachement C[7] - [8]
Cette description est purement syntaxique, et n'a pas de signification en soi, c'est le principe du système formel. Cependant cette théorie peut être interprétée et c'est précisément à partir de l'interprétation que l'on a construit le formalisme afin de mieux en étudier les propriétés et les fondements.
a="Il pleut",p="5 est un nombre pair", ou q=" mars a 30 jours"
Cpq devient: Si 5 est un nombre pair Alors mars a 30 joursDans le formalisme de Russell Cpq s'écrit (p) ==> (q)
Apq devient: 5 est un nombre pair OU mars a 30 jours
Dans le formalisme de Russel Apq s'écrit: (p) v (q)
Kpq devient: 5 est un nombre pair ET mars a 30 jours Dans le formalisme de Russel Kpq s'écrit: (p) ^ (q)
- E est l'équivalence.
Dans le formalisme de Russel Epq s'écrit (p) <==> (q)
| formalisme de Lukasiewicz | formalisme de Russel |
|---|---|
| CCpqCCqrCpr | ((p) ==> (q)) ==> [((q) ==> (r)) ==> ((p) ==> (r))] |
| CCNppp | ((~p) ==> (p)) ==> (p) |
| CpCNpq | (p) ==> ((~p) ==> (q)) |
| C | 0 | 1 | N | |
|---|---|---|---|---|
| 0 | 1 | 1 | 1 | |
| 1 | 0 | 1 | 0 | |
La question réciproque de savoir si une tautologie peut être obtenue comme thèse du système est précisément l'objet de la complétude. Il peut y avoir plusieurs interprétations associées à un système formel, on dira plusieurs modèles. Citons pour le calcul des propositions les circuits électriques avec interrupteurs.
si g et Egh sont des thèses du système alors h est aussi une thèse.Lukasiewicz a montré un peu plus tard que le calcul équivalentiel pouvait être fondé à l'aide de la règle de substition et de la nouvelle règle de détachement sur l'unique axiome suivant:
- EEpqEErqEpr
La non contradiction ou la consistance
Il y a plusieurs définitions de la non contradiction d'un système formel:
En 1921 Post a donné une preuve de la consistance de ce système. A la même époque Lukasiewicz possède la même preuve.
Ce type de démonstration est assez fastidieux. Donnons-en le schéma:
On construit une propriété que doivent vérifier les thèses. La propriété utilisée ici est la validité, c'est-à-dire que la thèse est une tautologie.
Le problème de la complétude consiste à se demander si le système permet d'obtenir toutes les thèses valides quel que soit le modèle de validité choisie. Est-ce qu'une EBF dont on sait qu'elle est une tautologie peut-elle être établie comme thèse du système ?
La encore il y a plusieurs définitions de la complétude:
La complétude faible, aussi appelée complétude sémantique, nécessite une interprétation sémantique et donc la notion de validité. Elle traduit le fait que toutes les EBF valides, donc vraies, peuvent être démontrées comme thèses dans le système. Autrement dit on peut identifier le système formel à son modèle, et ne plus travailler que sur le modèle.
Comme la consistance, ces deux définitions peuvent ne pas être équivalentes suivant les systèmes. Pour le calcul des propositions elles le sont.
EXEMPLE
On peut voir comment on peut rendre contradictoire la logique des propositions
en lui ajoutant comme axiome une EBF qui n'est pas une thèse:
soit Cpq l' EBF, ce n'est pas une thèse. Forçons-la à être une thèse: alors:On obtient donc à la fois Cpp et NCpp comme thèse, contradiction.
[1] Cpq supposée thèse [2] CCppNCpp règle [R1], Cpp remplace p et NCpp remplace q [3] NCpp règle [R2], détachement C[2] - [3]
La démonstration générale de la complétude faible du calcul des propositions est assez laborieuse, citons-en le principe.
La complétude est une propriété très importante d'un système formel, car elle permet de s'affranchir de la technique très lourde de la démonstration et de travailler dans le modèle avec l'assurance d'y obtenir les mêmes résultats avec plus de facilité. Dans un système non complet où il n'y a pas équivalence entre le système et son modèle, il peut y avoir des EBF valides qui n'ont pas de démonstration formelle dans le système. C'est le cas pour les propriétés vraies indémontrables que l'on trouve en aritmétique formelle à la suite des célèbres travaux de Godel.
Le principe de la démonstration est basé sur la notion de modèle et de validité. On trouve un modèle qui réalise tous les axiomes sauf celui dont on veut montrer l'indépendance. Plus précisément on cherche une propriété qui est vérifiée par les axiomes. Cette propriété est héréditaire par les règles et elle n'est pas vérifiée par l'axiome dont on veut montrer l'indépendance. Cet axiome ne sera pas démontrable à partir des autres à cause de l'hérédité de la propriété par les règles. A titre d'exemple de notre système, montrons l'indépendance de l'axiome 3 de Lukasiewicz: CpCNpq
Comme propriété nous allons choisir des valeurs de vérité pour l'implication C et la négation N qui soient vérifiées par les axiomes 1 et 2, héréditaire par les règles, et non vérifiées par l'axiome 3. Ces valeurs sont données par les tables de vérité suivantes:
C 0 1 N 0 1 1 1 1 0 1 1 On remarque que ce modèle ne vérifie pas les valeurs traditionnelles données à la négation. Dans ce modèle la négation ne nie rien et c'est précisément pour cela que l'on a besoin des trois axiomes de Lukasiewicz pour fonder le calcul des propositions.
La propriété est héréditaire par les règles.
Elle est vérifiée pour l'axiome 1, c'est évident puisqu'il n'utilise pas la négation. Elle est vérifiée par l'axiome 2, mais il faut un petit calcul:CCN000 = CC100 = C00 = 1La propriété n' est pas vérifiée pour l'axiome 3:CCN111 = CC111 = C11 = 1
C1CN10 = C1C10 = C10 = 0L'axiome 3 ne sera jamais démontré à partir des autres.
Il existe de nombreuses autres présentations d'un tel système que nous n'avons pas abordées, comme par exemple les quatre axiomes d'Hilbert-Ackermann, les trois axiomes de Frege-Lukasiewicz. Il existe des systèmes a 9 ou 11 axiomes. On a dénombré une vingtaine de présentations axiomatiques différentes du calcul des propositions. Citons pour la performance le système à un axiome basé uniquement sur l'incompatibilité:
[p | (q | r)] | [(t | (t | t)) | ((s | q) | ((p | s) | (p | s)))]bien sur il faut modifier la règle de détachement comme suit:
Si a est une thèse et a | (b | c) est aussi une thèse alors on peut admettre c comme thèse.On peut donner cet axiome sans parenthèses en utilisant la notation de Lukasiewicz:
DDpDqrDDtDttDDsqDDpsDps