Avant d’aborder l’étude des systèmes modaux, nous allons dire un mot des systèmes logiques proches de la logique classique, qui dérivent d’une interprétation plus faible de la notion de négation ou d’implication. Nous reprenons ici la présentation faite dans [Gri67].
Plutôt que de choisir un nombre minimal de schémas d’axiomes n’utilisant que les symboles → et ¬ puis de définir tous les connecteurs à partir de ces deux-là comme nous l’avions fait lors de la présentation de la logique classique propositionnelle, il est possible de partir d’un système définissant chacun des connecteurs logiques séparément. Ceci est même nécessaire, dans la mesure où ces connecteurs ne sont plus inter-définissables dans les logiques considérées dans cette section.
Les schémas d’axiomes de A sont :
| P→ (Q → P) |
| (P → (Q → M)) → ((P → Q) → (P → M)) |
| (P ∧ Q) → P |
| (P ∧ Q) → Q |
| (P → Q) → ((P→ M)→ (P→ (Q ∧ M))) |
| P → (P∨ Q) |
| Q → (P∨ Q) |
| (P → M) → ((Q → M) → ((P ∨ Q) → M)) |
Le signe ¬ n’apparaît nulle part dans les schémas d’axiomes de A. La négation n’existe pas dans ce système.
Le système A est un système extrêmement faible. Non seulement la négation n’existe pas dans A, mais certains théorèmes de la logique classique, comme p ∨ (p→ q) qui ne contient pourtant pas de signe de négation, ne sont pas des théorèmes de A. Si l’on rajoute l’axiome1 : [A9]
| A ∨ (A → B) |
le système ainsi défini contient bien l’ensemble des théorèmes de la logique classique ne contenant aucune négation. On l’appelle logique positive.
Si l’on étend le système A par les deux axiomes suivants : [A10]
| ¬ A → (A → ¬ B) |
[A11]
| (A → ¬ A) → ¬ A |
on obtient la logique minimale M. Dans ce système, le symbole de négation a pour interprétation << est réfutable >>2. Dans M, on a le théorème : [Négation et implication]
| p→ ¬ ¬ p |
En revanche, la réciproque est fausse.
Si l’on considère le système M, qu’on lui retranche l’axiome A10 et qu’on le remplace par : [A12]
| ¬ A → (A → B) |
on obtient la logique intuitionniste. Tout théorème de M est évidemment un théorème de J (A10 est une conséquence triviale de A12). Dans cette logique, le symbole de négation peut se comprendre comme << est absurde >>.
La logique classique se retrouve en adjoignant à la logique intuitionniste le schéma d’axiome A9.
Les problèmes concernant la notion de devoir et de nécessité sont apparus très tôt. Husserl résumera le problème :
<< Les énoncés négatifs du devoir ne doivent pas être interprétés comme des négations des énoncés positifs correspondants. >>
Le logicien anglais Lewis s’intéressera aux notions de nécessité et de possibilité à travers un des problèmes intuitifs lié à la logique classique, la formule :
| ¬ A → (A → B) |
Cette formule, qui se déduit aisément des axiomes de la logique classique, se lit : << si A est faux, je peux déduire n’importe quoi de A >>.
D’autres formules, comme A → (B → A)3, ont posé très rapidement des problèmes aux logiciens. Pour tenter de résoudre ces << paradoxes >>, Lewis proposa au début du siècle une nouvelle implication, dite implication stricte, qu’il nota : >.
Pour cela, il définit la notion de possibilité logique qu’il nota ◇ et posa par définition :
| (A>B) =def ¬ ◇ (A ∧ ¬ B) |
Ceci peut se lire : << il est impossible que A soit vrai et B faux lorsque A implique strictement B >>.
Il définit également la notion (duale) de nécessité, notée □ par :
| □ A =def ¬ ◇ ¬ A |
On peut le lire : << A est nécessaire si non-A est impossible >>.
Muni de ces définitions et de ces deux nouveaux opérateurs, dits opérateurs modaux, Lewis définit deux systèmes, S4 et S5, que nous allons examiner brièvement. Dans chacun de ces systèmes, l’implication stricte définie précédemment n’est plus paradoxale. En effet, les formules ¬ A > (A>B) et A > (B>A) ne sont pas toujours des théorèmes de ces systèmes.
Les notions de possibilité et de nécessité sont des instances particulières de la notion plus générale de modalité. [Modalité] On appelle modalité toute suite d’opérateurs ¬ , □ , ◇ . Par exemple ¬ □ □ ¬ ◇ est une modalité.
On voit bien intuitivement que des modalités syntaxiquement distinctes peuvent avoir la même signification. Ainsi les modalités ¬ ◇ et □ ¬ sont équivalentes dans tous les systèmes présentés ici. [Modalités équivalentes] Deux modalités α et β sont équivalentes si, pour toute formule A, on a : ⊢ (α A ↔ β A) Une logique modale peut être caractérisée par l’ensemble de ses modalités non-équivalentes. Pour établir la liste des modalités non-équivalentes, on tente d’établir l’ensemble des théorèmes de réduction syntaxique démontrables dans la logique dont on se préoccupe. Nous démontrerons un tel théorème dans S4.
On appelle logique aléthique toute logique dont les modes sont la possibilité et la nécessité. Les logiques définies par Lewis sont des logiques aléthiques. Le langage des premiers systèmes que nous allons étudier est construit comme celui du calcul propositionnel en y adjoignant la règle : Si A est une formule, alors ◇ A et □ A sont des formules. La construction faite par Lewis est un peu différente de celle que nous allons donner. Les systèmes de logique aléthique sont représentés dans la figure 0.1.
Dans cette figure (due à Prior), tous les systèmes qui sont à gauche des flèches sont des sous-systèmes des systèmes situés à droite, c’est-à-dire que tout théorème valable dans le système de gauche est aussi un théorème du système de droite.
Les systèmes S1 à S5 sont les systèmes définis par Lewis. Le système T est dû à Freys (1950) et Wright (1951), et est donc bien plus tardif. Cependant, il est formellement plus agréable d’arriver à S4 et S5 à partir de T qu’à partir de S1 et S2.
Le système T est défini par les axiomes de la logique classique et les axiomes supplémentaires suivants : [K]
| □ (A → B) → (□ A → □ B) |
| □ A → A |
On adjoint à la règle d’inférence de la logique classique la règle : [Règle de nécessitation]
|
T contient une infinité de modalités non-équivalentes. Il est consistant et il existe une procédure de décision.
Les règles d’inférence de S4 sont les mêmes que celles de T. On ajoute simplement l’axiome : [4] □ A → □ □ A Nous allons démontrer rapidement un théorème de réduction dans S4. [Réduction de □ □ en □]
| ⊢ □ □ A ↔ □ A |
On peut ainsi démontrer que dans S4 toute modalité ne contenant pas ¬ peut être réduite à une suite contenant au plus 3 opérateurs modaux. Notons enfin que S4 est complet et décidable.
S5 est également une extension de T. Il suffit de rajouter l’axiome suivant : [5]
| ◇ A → □ ◇ A |
D’autre part, tout théorème de S4 est un théorème de S5. En effet, il est aisé de montrer que l’axiome 0.4.2 est un théorème de S5. Enfin, on peut démontrer que, dans S5, toute modalité ne contenant pas de négation peut être réduite à un opérateur (théorème de réduction).
Nous nous sommes intéressés jusque-là à la théorie de la démonstration pour les logiques non-classiques. La question que nous sommes en droit de nous poser est la suivante : est-il possible de construire une théorie des modèles (semblable à la méthode des tables de vérité) dans un système comme S4 ou S5 ?
Nous devons tout d’abord constater que la méthode des tables de vérité qui consiste à associer à un opérateur une table est ici inapplicable. En effet, considérons qu’il fait beau aujourd’hui ; alors l’énoncé : << Le ciel est bleu >> est vrai, ainsi que l’énoncé : << Le ciel est bleu ou le ciel n’est pas bleu >>. En revanche, l’énoncé : << Le ciel est nécessairement bleu >> est faux, car il peut ne pas faire beau, alors que l’énoncé : << Nécessairement, le ciel est bleu ou le ciel n’est pas bleu >> est vrai. On voit donc que l’énoncé □ A peut être vrai ou faux, alors que l’énoncé A est vrai dans les deux cas. On voit donc mal comment la méthode des tables de vérité pourrait être appliquée.
[Modèle de Kripke] Un modèle de Kripke est défini par un triplet M=<W, R,m> où W={w1,w2,…,wi…} est un ensemble de mondes possibles4, R est une relation binaire définie sur W et m une fonction associant à chaque élément de W un sous-ensemble de Vp (ensemble des variables propositionnelles).
[Relation de satisfiabilité] Si A est une formule, M un modèle, et w un monde possible de M, alors la relation << Le monde w satisfait A >>, notée (M,w ⊨ A), est définie par :
[Formule satisfiable] Une formule A est dite satisfiable ssi il existe un modèle M et un état w de M tel que M,w ⊨ A.
[Formule valide] Une formule A est dite valide (et l’on note ⊨ A) ssi pour tout M et pour tout w de M on a M,w ⊨ A. Ainsi, en considérant une interprétation comme un couple (M,w), une formule valide est une formule vraie pour toute interprétation, ce qui est bien compatible avec la définition que nous avions utilisée en logique propositionnelle et en calcul des prédicats.
Que cherchons-nous à exprimer par les définitions précédentes ? Nous avons vu que la vérité d’une proposition du type □ A semblait être liée à une notion d’universalité de la vérité de l’énoncé A. Nous allons donc définir un ensemble de mondes contenant chacun des formules, puis nous les relierons entre eux par une relation d’accessibilité de la connaissance ; si par exemple w1 R w2 et w1 R w1 alors pour que M,w1 ⊨ □ p il faudra que p ∈ m(w1) et p ∈ m(w2). Pour avoir M,w1 ⊨ p, il suffit que p ∈ m(w1) et pour que M,w1 ⊨ ◇ p il suffit que p ∈ m(w1) ou p ∈ m(w2).
On voit donc qu’il est possible par ce moyen de construire un modèle pour tester la validité d’une formule. Cependant, ce modèle n’est pas quelconque. En fait les axiomes de la logique déterminent le type de la relation d’accessibilité R.
[Modèle de S4] Un modèle de Kripke pour S4 est un modèle M=<W, R,m> où R est une relation réflexive et transitive. Nous allons essayer de donner une idée intuitive de la démonstration pour la propriété de réflexivité.
En fait, la réflexivité est rendue nécessaire par l’axiome T ( □ A → A). Examinons la figure 0.2. Nous devons aisément comprendre à partir de cette figure pourquoi l’axiome T est vrai dans une structure réflexive.
On peut démontrer que la relation d’accessibilité de S5 doit être une relation d’équivalence.
Comme en logique classique, on peut s’intéresser en logique modale aux propriétés de consistance et de complétude.
Le but de cet ouvrage n’étant pas de développer une théorie générale des logiques modales, nous nous contenterons de citer les principaux résultats. Les lecteurs intéressés pourront se reporter à [HC72].
S4 et S5 sont syntaxiquement consistants, adéquats et complets vis-à-vis de l’interprétation sémantique définie par les modèles de Kripke.
Il faut noter que, pour chacun de ces systèmes, on peut rajouter certaines formules qui ne sont pas des théorèmes de ces systèmes en tant que schémas d’axiomes sans aboutir à des systèmes syntaxiquement inconsistants5. En effet, nous avons vu que T peut-être étendu à S4, que S4 peut être étendu à S5. D’autre part, il est toujours possible de rajouter à S5 le schéma :
| A → □ A |
Ce schéma ne rend pas le système inconsistant, et n’est pas non plus un théorème de S56.
Comme nous l’avons fait pour le calcul propositionnel, il est possible de définir une logique modale opérant sur des prédicats. La définition du langage est la même que pour la logique des prédicats avec l’adjonction de la définition suivante : Si A est une formule alors □ A et ◇ A sont des formules. On peut ainsi définir des systèmes S4 et S5 du premier ordre en adjoignant à l’axiomatique propositionnelle de S4 et S5, les axiomes de la logique des prédicats (voir [HC72]).
Les logiques épistémiques sont des logiques ayant pour but de représenter la notion de connaissance ou de croyance. Elles ont été introduites par J. Hintikka en 1963.
La logique de la connaissance est basée sur S5. Les opérateurs modaux rencontrés prennent alors une autre signification ; ainsi □ devient << SAVOIR >> et ◇ devient << COMPATIBLE AVEC MES CONNAISSANCES >>.
Examinons les axiomes et les règles d’inférence de S5 à la lumière de ces nouvelles définitions.
La règle d’inférence :
|
peut alors se lire : << si A est démontrable, (je sais A) est démontrable7 >>.
L’axiome □ (A → B) → (□ A → □ B) peut se lire : << si je sais que A → B est vrai, alors, si je sais que A est vrai, je sais que B est vrai >>.
L’axiome □ A → A devient : << si je sais que A est vrai, alors A est vrai >>.
L’axiome ◇ A → □ ◇ A devient : << si A est compatible avec mes connaissances, alors je sais que A est compatible avec mes connaissances >>. Cet axiome est un axiome dit d’introspection négative.
On remarquera que la propriété de S5 : □ A → □ □ A, est également une propriété d’introspection, mais positive8.
Cette logique est appelée logique de la connaissance en raison de l’axiome □ A → A, qui exprime que si l’on connaît une propriété alors cette propriété est vraie.
La logique de la croyance est obtenue à partir des axiomes de S5, en supprimant l’axiome □ A → A et en rajoutant dans le jeu des axiomes la propriété : □ A → □ □ A.
La suppression de □ A → A reflète le fait que le concept de croyance admet que l’on peut croire des choses qui sont fausses dans la réalité.
Une extension classique valable pour toutes les logiques épistémiques est l’introduction d’arguments dans les opérateurs modaux. Ainsi, on peut écrire □ [Pierre] A, qui se lira << Pierre sait que A est vrai >>. Ces systèmes permettent de représenter des environnements où les connaissances sont disjointes. On peut par exemple écrire : □ [Pierre] A → □ [Paul] A, que l’on peut traduire par : << Paul sait tout ce que sait Pierre >>. De telles logiques sont appelées multi-modales.
L’extension au premier ordre permet, elle, d’exprimer des propositions de la forme :
| ∃ x □ espion(x) |
qui signifie : << il existe une personne x dont je sais que c’est un espion >> à ne pas confondre avec cette autre proposition également exprimable :
| □ ∃ x espion(x) |
qui signifie, elle : << je sais qu’il existe un espion (mais je ne sais pas qui c’est) >>.
Nous nous contenterons dans ce chapitre de donner un aperçu des logiques temporelles. Les lecteurs intéressés peuvent se reporter pour plus de précisions à [AEC90], dont nous nous sommes largement inspirés.
Le but de la logique temporelle est d’enrichir (comme le fait la logique modale) la capacité d’interprétation de la logique classique.
Ainsi l’énoncé << Robespierre est mort >>, s’il est vrai aujourd’hui, était faux en 1789. Or, ce type d’évaluation est impossible en logique classique. Là où la logique modale a introduit des notions de nécessité et de possibilité, la logique temporelle va introduire les notions de futur et de passé.
Il existe deux façons de définir une logique temporelle. L’une d’entre elles est basée sur les dates. On introduit un opérateur binaire de datation, généralement noté R. L’expression Rtp signifiant << p est réalisé à l’instant t >>. De cette façon , on peut aisément en fixant une échelle et une origine des temps, exprimer des propriétés comme << Hitler est mort en 1945 >>. En revanche, cette méthode ne nous permet pas de représenter simplement des énoncés comme << le temps sera beau >>. Pour représenter ce type d’énoncé, nous avons besoin d’un opérateur dit opérateur d’ultériorité, noté généralement U. Ainsi on écrira : Rt ( Utt′ ∧ pt′) avec Utt′ signifiant << t′ est ultérieur à t >> et p étant << le temps est beau >>. Il faut remarquer que cette seconde méthode repose sur ce que l’on appelle des pseudo-dates. En effet, nous utilisons comme éléments de référence des termes comme << aujourd’hui >> ou << demain >> qui ne sont pas à proprement parler des dates (c’est-à-dire des éléments fixes). Les premiers travaux de la logique temporelle furent en grande partie consacrés à établir que le calcul fondé sur les pseudo-dates pouvait se dériver du calcul sur les dates.
Les premiers opérateurs que nous allons définir seront les opérateurs F et P, opérateurs futur et passé. La définition de ces opérateurs en langage des pseudo-dates est9 :
On peut donner comme interprétation de Fp : << p sera vrai >> et comme interprétation de Pp : << p a été vrai >>.
On peut, à l’aide de ces opérateurs, exprimer les notions d’ultériorité. Ainsi si on veut exprimer que p est postérieur à q, on peut écrire :
| (p ∧ (¬ q ∧ Pq)) ∨ P(p ∧ (¬ q ∧ Pq)) ∨ F(p ∧ (¬ q ∧ Pq)) |
On peut remarquer les trois parties de cette formule. La première (p ∧ (¬ q ∧ Pq)) signifie que p est vrai, que q est faux, et que q a été vrai dans le passé. Les deux autres parties complètent la première en exprimant que ce << fait >> a été vrai dans le passé ou qu’il sera vrai dans le futur. Ainsi, la composition des trois permet de dire que p est postérieur à q aujourd’hui ou qu’il le sera ou qu’il l’a été (informellement).
On voit immédiatement que, comme en logique modale, la méthode des tables de vérité n’est pas applicable en logique temporelle.
En fait, il existe une forte similitude entre logique modale et logique temporelle. En théorie des modèles de la logique modale, nous avons vu qu’un modèle était un ensemble de mondes, et que la relation d’accessibilité des connaissances entre ces mondes déterminait le type de la logique.
En logique temporelle, les mondes possibles deviennent les mondes datés et la relation d’accessibilité devient la relation d’ultériorité entre les dates. Suivant la façon dont on conçoit le temps (linéaire ou ramifié, continu ou discret…), on modifiera la relation d’accessibilité, ce qui à son tour modifiera les axiomes de la logique.
Par analogie avec la logique modale, on définit également les opérateurs duaux de F et P :
Les définitions formelles du langage de la logique temporelle, ainsi que les définitions de satisfiabilité et de validité sont très semblables à celles de la logique modale, nous ne les reprendrons pas. Nous allons plutôt nous intéresser à l’influence des diverses interprétations du temps sur l’axiomatique (théorie de la démonstration) et les relations de satisfiabilité (théorie des modèles).
Notons tout de suite que deux axiomes seront valables dans toute la suite ; il s’agit de :
Ces axiomes, sont semblables à ◇ (A → B) → (◇ A → ◇ B) et □ (A → B) → (□ A → □ B) en logique modale.
Il s’agit là de la notion de base dans la représentation intuitive que nous avons du temps. Elle impose (évidemment) à la relation entre les mondes d’être anti-symétrique. Les axiomes logiques de tout système temporel doivent donc avoir des modèles dont la relation d’accessibilité est anti-symétrique. Cependant, il n’existe pas d’axiomes caractérisant l’anti-symétrie. Les axiomes suivants, qui expriment l’ultériorité, correspondent bien à une relation anti-symétrique, mais ne correspondent pas seulement à une telle relation :
Comme nous le voyons ces axiomes se << lisent >> bien en terme d’ultériorité comme nous le disions en tête de ce paragraphe. Avec les deux axiomes du paragraphe précédent, ils forment l’axiomatique de la logique temporelle de base.
Si nous supposons que nous pouvons ordonner, tout au moins partiellement, nos dates, notre relation devient une relation d’ordre partiel i.e., elle devient transitive en plus de son anti-symétrie.
La transitivité exprime des propriétés comme : << si A est vrai dans le futur, alors il sera toujours vrai que A sera vrai >>.
Il nous faut donc adjoindre des axiomes exprimant la transitivité. La transitivité est associée à l’axiome □ A → □ □ A. Cet axiome devient en logique temporelle GA → GGA.
Nous conservons les propriétés (anti-symétrie et transitivité) précédentes, ainsi que les axiomes qui en découlent, mais nous devons de plus exprimer que deux dates sont toujours comparables : ∀ wi ∀ wj (wi < wj) ∨ (wj < wi) ∨ (wi = wj).
Les axiomes correspondants à cette propriété sont :
L’axiome FA ∧ FB → F(A ∧ FB) ∨ F(FA ∧ B) exprime que si à un instant donné nous avons dans le futur deux événements A et B, alors soit A se produit et B sera dans le futur de A, soit B se produit et A sera dans le futur de B. Ceci nous donne le schéma de la figure 0.3. Pour plus de détails, on pourra se reporter à [RU71].
Il est également possible de représenter nombre d’autres propriétés en logique temporelle, dont la notion de temps discret, ou de temps ramifié…Pour plus de détails, on pourra se reporter à [RU71].
Dans ce chapitre, nous allons montrer sur un exemple simple comment la logique temporelle peut être utilisée pour coder un programme et démontrer sa correction.
Le programme auquel nous allons nous intéresser est extrêmement simple :
y1:=n; y2:=m;
while (y2>0) do
begin
y1:=y1+1; y2:=y2-1;
end;
Ce programme calcule évidemment la somme de deux nombres n et m qu’il retourne dans y1.
La première étape à réaliser est de coder le programme sous forme d’un graphe d’exécution, ou graphe de contrôle.
Chacun des sommets du graphe représente une étape du contrôle. À chaque arc est associé une condition et un ensemble d’opérations à effectuer :
| (li,lj) : Cij( |
| ) → fij( |
| ) |
Ceci peut se lire intuitivement : si le programme est dans l’état li alors il passera dans l’état lj ssi toutes les conditions Cij portant sur les variables y du problème est vérifié. Lors de la transition, on appliquera aux variables y, la transformation fij(y).
Les programmes séquentiels déterministes garantissent que pour chaque sommet li, une et une seule condition Cij est vraie à un instant donné.
Appliquons cette méthode de codage sur notre exemple. Les trois sommets seront :
Les arcs seront :
| (l0,l1):(true) → (y1:=n,y2:=m) |
| (l1,l1):(y2>0) → (y1:=y1+1,y2:=y2-1) |
| (l1,lf):(y2=0) → (nul) |
L’ensemble de ces éléments est représenté dans la figure 0.4.
Notre programme est déterministe, séquentiel et discret, donc les états seront une suite discrète w0,w1,…,wn. Nous posons wk=(li,yk). L’état w est donc entièrement déterminé par le sommet courant du graphe et l’état des variables du problème à l’instant k.
La relation d’accessibilité est très simple. Dans ce modèle temporel linéaire non ramifié, on pose wi R wj ssi i ≤ j.
Nous utiliserons comme variables propositionnelles des expressions at lj qui seront vraies dans l’état wk=(li,yk) ssi i=j.
Un prédicat atomique portant sur les variables, de la forme p(y), sera vrai dans l’état wk=(li,yk) ssi p(yk) est vrai.
Enfin nous utiliserons comme opérateurs temporels ◇ et □. Ils pourront se lire :
À chacune des relations de transition sur les arcs du graphe nous associons une formule de la logique temporelle de la façon suivante.
Soit la condition :
| (li,lj) : Cij( |
| ) → fij( |
| ) |
nous lui associons la formule :
| □ ((at li ∧ Cij( |
| ) ∧ ( |
| = |
| )) → ◇(at lj ∧ ( |
| = fij( |
| )))) |
Ainsi, le programme qui nous intéresse se code en trois formules, correspondant aux trois relations vues plus haut :
| □ ((at l0 ∧ (y1=v1) ∧ (y2=v2)) → ◇(at l1 ∧ (y1=n) ∧ (y2=m))) (0.1) |
Cette formule exprime que si nous sommes dans l’état initial, alors il existe un état accessible où le contrôle est en l1 et y1=n,y2=m.
Codons la seconde relation :
| □ ((at l1 ∧ (y1=v1) ∧ (y2=v2) ∧ (y2>0)) → ◇(at l1 ∧ (y1=v1+1) ∧ (y2=v2−1))) (0.2) |
Cette formule exprime que si nous sommes dans l’état l1 et que y2>0, alors il existe un état accessible où le contrôle reste en l1 et où les variables sont devenues y2:=y2−1,y1:=y1+1.
Codons la troisième relation :
| □ ((at l1 ∧ (y1=v1) ∧ (y2=v2) ∧ (y2=0)) → ◇(at lf ∧ (y1=v1) ∧ (y2=v2))) (0.3) |
Cette relation exprime que nous passons dans l’état final sans changer la valeur de nos variables si y2=0.
Nous avons maintenant terminé de coder nos hypothèses de calcul.
Il nous reste maintenant à coder nos conclusions, ou plus clairement à coder le résultat que nous voulons que notre programme obtienne. Comment peut-on exprimer en logique temporelle le fait qu’un programme va calculer correctement une valeur ?
En fait, il existe deux types de correction possible, l’exactitude partielle et l’exactitude totale.
| (at l0 ∧ P) → □ (at lf → Q) |
| (at l0 ∧ P) → ◇(at lf ∧ Q) |
Pour en revenir à l’exemple qui nous intéresse, l’exactitude partielle sera codée par :
| at l0 → □ (at lf → (y1=n+m)) |
et l’exactitude totale sera codée par :
| at l0 → ◇(at lf ∧ (y1=n+m)) (0.4) |
Nous allons voir que nous sommes dans un cas où la logique temporelle est assez simple.
En fait, une logique temporelle minimale basée sur les axiomes de S4 nous suffit pour travailler sur les propriétés temporelles du système. Rappelons que les axiomes de ce système sont 0.4.1, 0.4.1, 0.4.2, et la règle d’inférence 0.4.1 plus les axiomes et les règles d’inférence de la logique classique. Cependant, nous avons aussi besoin d’exprimer des propriétés du premier ordre. C’est donc en fait le système S4 du premier ordre que nous adoptons.
Mais nous devons également enrichir S4 d’un certain nombre d’axiomes et de règles d’inférence exprimant les propriétés des données manipulées. Comme nous travaillons sur des nombres entiers en utilisant des règles d’arithmétique, nous devons utiliser l’équivalent des axiomes de ℕ en logique temporelle.
Ainsi nous pouvons récupérer l’axiome d’induction :
| A(0) ∧ ∀ x (A(x) → A(x+1)) → A(x) |
et le transformer en une règle d’induction en logique temporelle :
|
En fait, nous n’utiliserons pas cette règle mais une règle dérivée :
| (0.5) |
On peut lire cette règle de la façon suivante : si chaque fois que l’on a A(0), alors on aura B, et si chaque fois que l’on A(n+1), alors on aura soit A(n) soit B, alors s’il existe une valeur k telle que A(k), on aura B.
Il nous faut d’autre part quelques propriétés supplémentaires sur les entiers. Nous utiliserons :
| □ (x ≥ 0) (0.6) |
et
| □ ((0 ≤ x ≤ n+1) → (0 ≤ x−1 ≤ n)) (0.7) |
Le problème est maintenant complètement formalisé dans un système logique, et il ne s’agit plus que de construire une preuve : il faudrait démontrer en utilisant les hypothèses 0.1,0.2,0.3, les axiomes et règles d’inférence de S4 et les règles et propriétés 0.5, 0.6, 0.7 que la formule 0.4 est vraie.
La preuve complète est longue et technique, nous ne la développerons pas ici. Nous renvoyons le lecteur intéressé à [AEC90].
Nous allons terminer en disant un mot des logiques multi-valuées. Les logiques multi-valuées sont construites intuitivement à partir de la technique des tables de vérité de la logique classique. Simplement, au lieu de ne considérer que deux valeurs possibles t ou f, ou encore en logique binaire 0 et 1, on construit une table où chacun des atomes peut prendre plusieurs valeurs pour les logiques admettant seulement un nombre fini de valeurs. Pour les logiques acceptant une infinité de valeurs, on donne des règles générales de construction.
A B A → B ¬ A 0 0 1 1 0 1/2 1 1 0 1 1 1 1/2 0 1/2 1/2 1/2 1/2 1 1/2 1/2 1 1 1/2 1 0 0 0 1 1/2 1/2 0 1 1 1 0
Dans la logique trivaluée de Lukasiewicz, un atome peut prendre trois valeurs 0, 1/2, ou 1. Les connecteurs sont définis à partir des tables de vérité. Le tableau 0.1 définit l’ensemble des connecteurs.
On définit les connecteurs manquants par :
| p∨ q =def (p → q) → q |
| p∧ q =def ¬ (¬ p ∨ ¬ q) |
| p ↔ q =def (p → q) ∧ (q → p) |
Nous avons donc ici un modèle sémantique de notre logique. La construction d’une théorie syntaxique dans le cas des logiques multi-valuées est chose difficile.
logiques non classiques|)
Le téléchargement ou la reproduction des documents et photographies
présents sur ce site sont autorisés à condition que leur origine soit
explicitement mentionnée et que leur utilisation
se limite à des fins non commerciales, notamment de recherche,
d'éducation et d'enseignement.
Tous droits réservés.
Dernière modification: 09:48, 22/02/2024
