Line

Accueil
CV

Sites IA

LC
Introduction
Langage
Sémantique
Applications

LP

 La logique propositionnelle
Il n'y a qu'une méthode pour inventer, qui est d'imiter.
Alain
A la plus belle les premiers honneurs. Ancêtre de la logique, la logique propositionnelle Lp est à la base de tous les systèmes formels. Simple et pure, elle est d'une richesse suffisante pour exprimer de nombreux raisonnements non triviaux.

Le langage de la logique propositionnelle est composé :
  • de propositions atomiques (notée classiquement a,b,c...) formant l'ensemble PLP,
  • du connecteur monadique de négation, noté ¬,
  • du connecteur diadique d'implication matérielle, noté ->,
  • des symboles de parenthèses "(" et ")".
Les règles de formation d'une formule bien formée sont :
{Base} Toute proposition atomique est une formule bien formée.

{Induction} Si a et b sont des formules bien formées, alors les expressions (a), ¬a et a->b sont des formules bien formées.

{Clôture} Une formule bien formée s'obtient exclusivement en appliquant un nombre fini de fois les règles de base et d'induction.
L'ensemble des formules bien formées est noté WLP. Pour toutes formules bien formées a et b, un axiome est une formule de la forme :
[A1] : {Unicité} a->(b->a)
Une proposition vraie l'est indépendamment de toute autre proposition. Cet axiome permet d'exprimer le concept leibnitzien du monde et du tiers exclu : a est strictement vrai ou faux.
[A2] : {Auto-distributivité} (a->(b->c))->((a->b)->(a->c))
Une proposition infère les propositions inférées par les propositions qu'elle infére - faut suivre !
[A3] : {Raisonnement par l'absurde} (¬a->¬b)->((¬a->b)->a)
Une proposition n'infère pas de propositions contradictoires. Cet axiome permet d'exprimer le principe de non contradiction : a n'est pas à la fois vrai et faux.
Les règles de formation d'un théorème sont :
{Base} Tout axiome est un théorème,

{MP} Pour tous a et b de WLP, si a et a ->b sont des théorèmes, alors b est un théorème (cette règle est appelée le modus ponens),

{Clôture} Un théorème ne peut être obtenu qu'en appliquant un nombre fini de fois la règle de base et MP.
L'affirmation "a est un théorème" est noté |-LP a. Montrons, par exemple, que, pour tout a de WLP,  a->a est un théorème :
  1. |-LP a->(a->a) par application de [A1] pour b=a
  2. |-LP a->((a->a)->a) par application de [A1] pour b=a->a
  3. |-LP (a->((a->a)->a))->((a->(a->a))->(a->a)) par application de [A2] pour c=a et b=a->a
  4. |-LP (a->(a->a))->(a->a) par application de MP sur 2 et 3
  5. |-LP a->a par application de MP sur 1 et 4
Une théorie F est un ensemble de formules de WLP. Les formules de F représentent les hypothèses de F. Une formule a est dite prouvable dans F (et est notée F |-LP a, soit : a est un théorème de F) si, et seulement si, elle peut être produite de F en appliquant les règles de formation des théorèmes, pour toutes les hypothèses de F se comportant comme des théorèmes.

F est dit déductivement clos si :
Pour tout f de WLP, si F |-LP f, alors f appartient à F, ce qui se note : F=ThLP(F)
Montrons, par exemple, que a est prouvable dans F={¬a->b, ¬a->¬b}
  1. F |-LP ¬a->b par hypothèse
  2. F |-LP ¬a->¬b par hypothèse
  3. F |-LP (¬a->¬b)->((¬a->b)->a) par application de [A3]
  4. F |-LP (¬a->b)->a par application de MP sur 2 et 3
  5. F |-LP a par application de MP sur 1 et 4
La négation d'un théorème est, de manière générique, notée ®. F est dit inconsistant si, et seulement si : F |-LP ®. Dans le cas contraire, F est dit consistant. La logique propositionnelle vérifie le théorème de compacité ([BelMac78]), qui est :
Un ensemble F de formules bien formées est consistant si, et seulement si, tous ses sous-ensembles finis sont consistants.
Montrons, par exemple, que l'ensemble F={a, ¬a} est inconsistant :
  1. F |-LP a$ par hypothèse
  2. F |-LP ¬a$ par hypothèse
  3. F |-LP a->(¬®->a) par application de  [A1]
  4. F |-LP ¬a->(¬®->¬a) par application de [A1]
  5. F |-LP ¬®->a par application de MP sur 1 et 3
  6. F |-LP ¬®->¬a par application de MP sur 2 et 4
  7. F |-LP (¬®->¬a)->((¬®->a)->®) par application de [A3]
  8. F |-LP (¬®->a)->® par application de MP sur 6 et 7
  9. F |-LP ® par application de MP sur 5 et 8
Cet exemple montre bien combien la moindre démonstration peut être fastidieuse ! Aussi, afin de simplifier l'expression des formules, le langage est communément étendu aux connecteurs diadiques de disjonction (noté |), de conjonction (noté ^) et d'équivalence (noté <->). Ils sont définis par :
  • a | b est équivalent à (¬A->B),
  • a^b est équivalent à ¬(A->¬B),
  • a<->B est équivalent à (a->b)^(b->a)
Un littéral est une proposition atomique ou la négation d'une proposition atomique.
Une clause est une disjonction de littéraux.
Une formule est dite sous forme normale si elle est une conjonction de clauses. Nous sommes, à partir de ces définitions, en mesure d'énoncer le résultat suivant ([Tha90]) :
Toute formule admet une réécriture logiquement équivalente sous forme normale.
Par exemple, la formule (a->b)->c)->(f->g)] est logiquement équivalente à la formule : (¬a | b | ¬f | g)^(¬c | ¬f | g)

P. Siegel propose un processus de complexité linéaire qui réécrit une formule bien formée quelconque sous sa forme normale ([Sie87]). La conséquence importante de ce théorème est que tout ensemble de formules du langage propositionnel admet une réécriture logiquement équivalente sous la forme d'un ensemble de clauses.

Il est courant d'ajouter à chaque clause l'expression " | ®", par application du théorème :
Pour tout a de WLP, |-LP a | ® si et seulement si |-LP a
Il est alors possible de proposer une procédure de preuve plus pratique que la précédente. C'est la résolution ([ChaLee73]).

Soit F un ensemble de formules sous forme clausale. Soit a,b de WLP. F|-LP a si, et seulement si, a peut être déduit de F en appliquant les règles :
[R1] a | b est logiquement équivalent à b | a
[R2] b | b | c est logiquement équivalent à b | c
[R3] Si F|-LP b | c et F|-LP d | ¬c, alors F|-LP b | d
Montrons, par exemple, que ¬a est prouvable dans F={a->b, a->¬b} :
  1. F|-LP ¬a | b | ® par hypothèse
  2. F|-LP ¬a | ¬b | ® par hypothèse
  3. F|-LP ¬a | ® par application de [R1], [R2] et [R3] sur 1 et 2
  4. F|-LP ¬a par application du théorème.
Montrons que {a,¬a}|-LP ® :
  1. {a,¬a}|-LP a | ® par hypothèse
  2. {a,¬a}|-LP ¬a | ® par hypothèse
  3. {a,¬a}|-LP ® par application de [R2] et [R3] sur 1 et 2
Nous venons de présenter des règles de production et de transformations syntaxiques, qui permettent, à partir d'un ensemble de formules bien formées, de produire de nouvelles formules. Il est maintenant souhaitable de donner un sens à tout cela. C'est le rôle de la fonction d'interprétation.

Classiquement, l'attitude du logicien consiste à ne voir dans le langage formel que des symboles mathématiques dénués de tout contenu sémantique : seuls ont un sens (par ailleurs strictement symbolique et univoque) les connecteurs et autres signes. Est fait abstraction de toute référence à un contenu sémantique quel qu'il soit : le pertinent se trouve dans l'étude des mécanismes et des lois du raisonnement, présentés dans la partie précédente.

Considérons F un ensemble de formules, et a et b appartenant à WLP. On définit la fonction d'interprétation  ILP de la logique propositionnelle comme étant une fonction, qui associe à toute formule de F soit la valeur d'interprétation "Vrai" (notée 1), soit la valeur d'interprétation "Faux" (notée 0). Le domaine d'interprétation est noté {0,1}. Formellement, ILP(F) est définie par :
[I1] ILP(F)(a)=1 si, et seulement si, a appartient à F, sino  ILP(F)(a)=0 : a est exclusivement vrai ou faux.
[I2] ILP(F)(¬a)=1 si, et seulement si, ILP(F)(a)=1 : ¬a modélise la négation sémantique de a.
[I3] ILP(F)(a->b)= si, et seulement si, ILP(F)(a)=0 ou ILP(F)(b)=1 : a->b est vrai si, et seulement si, soit a est faux (puisqu'à partir d'une hypothèse fausse il est possible de déduire tout et n'importe quoi), soit b est vrai (puisqu'une proposition vraie l'est indépendamment de toute autre proposition).
La sémantique de la logique propositionnelle, qui indique la relation entre le monde modélisé et l'ensemble de formules F qui le représente formellement, est donnée par la proposition suivante : soit c un fait du monde réel, et a la formule qui le représente dans F. Alors :
  • c est vrai si, et seulement si, ILP(F)(a)=1
  • c est faux si, et seulement si, ILP(F)(a)=0
Remarquons que ces définitions sous-entendent une troisième valeur d'interprétation, qui traduit le fait que ni a ni ¬a ne sont des théorèmes de F : on dit alors que a est indéfini par rapport à F.

La relation |=LP d'inférence sémantique est définie par :
ILP(F)(a)=1 si, et seulement si, F |=LP a
a est alors appelé une tautologie de F (ou est dit "valide dans F"). a est une tautologie (ou formule valide) si :
Pour tout ensemble F de WLP, on a : F |=LP a
Par exemples, les axiomes A1, A2 et A3 sont des tautologies. Prouvons-le pour~: [mbox{A1 : $Ara (Bra A)$}] begin{itemize} begin{itemize}
item si $cal {I}_p^{cal {F}}(A)=0$, le résultat s'obtient par application immédiate de [I3],
item sinon, $cal {I}_p^{cal {F}}(A)=1$ et donc $cal {I}_p^{cal {F}}(Bra A)=1$ par application de [I3].
Le résultat est alors obtenu par application de [I3]
footnote{Ce petit exemple trivial cache, par sa simplicité, la difficulté à obtenir la valeur d'interprétation d'une formule. C'est ce qui rend souvent utile l'existence d'une axiomatique. Celle-ci permet de produire des théorèmes de manière automatique, par simple application des règles d'inférences.

Les propriétés d'adéquation et de complétude font le lien entre l'axiomatique (les axiomes et la procédure de production) et la sémantique (la fonction d'interprétation). Elles sont définies par :
  • un langage formel $cal {L}$ est dit {adéquat} si, et seulement si : [mbox{Si $cal {F}vdash_{cal {L}} F$ alors $cal {F}models_{cal {L}} F$}] c'est à dire : si $F$ est un théoràme de $cal {F}$, alors $F$ est une tautologie de $cal {F}$. Cette propriété assure que le processus de production de théoràmes ne produit que des tautologies : elle est donc nécessaire pour que l'on puisse faire confiance au système,
  • un langage formel $cal {L}$ est dit {complet} si, et seulement si : [mbox{Si $cal {F}models_{cal {L}} F$ alors $cal {F} vdash_{cal {L}} F$}] cést à dire : si $F$ est une tautologie de $cal {F}$, alors $F$ est un théoràme de $cal {F}$. Cette propriété assure que toutes les tautologies seront produites. Elle est donc souhaitable.
Nous terminons cette présentation de la logique propositionnelle par l'énoncé des résultats fondamentaux suivants ([Men79])~:
Le système formel que nous venons de présenter est adéquat et complet.

Soient $Fsubsetcal {W}_{cal {L}p}$, et $A,Bincal {W}_{cal {L}p}$. Alors~: [{F,A}models_{cal {L}p}B Lr Fmodels_{cal {L}p}Ara B] end{axiom}
Ce résultat est appelé le méta-théorème de déduction.