A C T A U N I V E R S I T A T I S L O D Z I E N S I S FOLIA PHILOSOPHICA 7. 1990
P a t r ic e B e ilh a c h e
PERSPECTIVES ONTIQUfS ET TEMPORELLES POUR LA LOGIQUE OffONTIQUE
(AXIÜMATIQUE, SÉMANTIQUE ET COMPLETUOE)
In tr o d u c tio n
Pour con tou rn er le s nomhreux paradoxeg qui l u i sont p ro p re s , la lo g iq u e des normos a b esoin do prendre en campte non seulem ent la dim ension d Jo n tiq u e , b ie n s ú r , mais a u s s i des dim ensions comrae c e l ie des m od alittis o r d in a ir e s (u n tiq u e s ou a lé t h iq u e s ), c e l i e du temps, c e l i e de ľ a c t io n , c e l i e du s a v o ir , e t c . On S tu d ie i c i , t ie s sommalrement, au sim p le n ive a u du c a lc u l des p r o p o s it io n s , la com- b in a is o n des t r o ie dim ensions o n tiq u e , d eon tiq u e e t te m p o re lle . L'a- n a ly s e sém antique permet d '" e x p llq u e r " avuc un bon riegre' de vraisem- b la n ce lo s d iv e r s axiomee q u 'i l corivten t de p o ser. On donne pour f i n i r la s tr u c t u r e (je n e ra le des preuves de com plétude qui d o iverit é t r e m ises ел oeu vre. Ces preuves sont e s s e n t ie lle s , c a r ce sont e l l e e , b ie n souvorit, qui perm ettent do tro u v e r le s éle'ments axio- m atiquus e t s^m antiques prop res aux systÄm es; e t , du f a i t du málange ties t r o i s dim ensions, e l l e s sont d 'u n e d i f f i c u l t ^ а зэе г grande, qui m cirite e x p lic a t io n .
N otre but e s t i c i de donner un riombre minimum ď in d ic a t io n s sur un systéme o n t i q u e , d e o n t i q u e et t e m p o r e l que nous a p p e lle ro n s B Si- D S S, e t qui, dans son genre du moins, fo rm a lis e le s in t u it i o n s le s p lu s fondam entales en m a tié re ď é t r e , de d e v o ir - é tr e e t du te m p o r a lité . A fln de re m p lir ce b u t, nous prendroits comme modéles de dópart le s system es o n tiq u e s T, S 4 , S5, b ie n connus*, que nous c o n s id e re rc n s du double p o in t de vue
tiq u o e t sém antique. Noua v a rie ro n a e t e n r ic h lro n e progress!vem ent ces systém es, pour p a rv e n tr fin a le m e n t au systéme trid im e n a io n n e l d é s ir é .
I . D e s c rip tio n sommatre des systém es
Systémes puremant o n tiq u e s T. S » , SS
Axlomat lq u e . Comme le a axiom atiques de tous le s systém es dont i l va é tr e q u estio n i c i , c e l i e de T c o n tle n t un ensemble d'axiom es p rop res au pur c a lc u l p ro p o s itio n n e l non modal. E l l e у a jo u te le a élém ents s u iv a n ts , dont nous n oterons 1 'ensemble AxT:
O é f.e ■p * i l e s t n é c e a s a ire que p, A*l e (p э q) э (*p 3 * q ) ,
A®2 *p э р ,
R * H f —* H ® /•
Pour S4 et 35, s' a jo u te resp e ctive m e n t 1 'un des deux axiomes (ď ú ú le s ensembles axiom atiques Ax54 e t 4x SS):
A*S4 «p э M p , APS5 - Ш р э « * р .
Séman tiq u e . Noua c o n sid é re ro n e le a sém antiques "é la m aniére de K r ip k e ", p lu s p récisém ent aous la forme que le u r ont donnée Hughes e t C re a s w e ll. "An In tr o d u c tio n to Modal L o g ic " , 196Ü. Passant sur le d é t a il dea mécanismes d 'é v a lu a t io n de3 fo rm u le s, nous ne conaerverons que 1 'e s s e n t i e l , á s a v o ir le a deux ré g le a m odales, qui aont ä la base de la c o n s tr u c tio n des diagrammes sém antiques:
M. 5 i dans un monde w, fig u r e und fo rm u le * / de v a la u r 0, a lo r s i l d o i t у a v o i r a u m a i n s u n monde Wj t e l que RwjWj dans le q u e l f ig u r e У avec la v a le u r 0.
N. S i dans un monde Wj f ig u r e une f o r m u le * / de v a le u r I , a lo r s e n t o u t monde w. t e l que Rwt Wj d o it f ig u r e r / avec la v a le u r I .
,
’’
•
.
*
•
’
>«
.,? •
-La ré g le M (comme "m ö g lich " * p o s s ib le ) exprime qu'une form ule e s t p o s s ib le dans un monde, s i e l l e e s t v r a ie dans au moins un monde a c c e s s i b l e au monde co n a id é ré . La r e la t io n Rwt Wj exprime 1* a c c e s s i b i l i t y du monde wj pour le mondeC e tte r e la t io n poseéde au moins la p r o p r id té de la r é í 1 e x i- v i t é , ce qui e s t la tra d u c tio n sém antique de l* axiómu A*2 ( l e n é c e s s a ir e lm p liq ue le v r a i ) . £ l l e e s t en o u tre t r o n з i t i v e pour SA , e t t r a n s i t i v e et a y m á t r i q u e (done un« r e la t io n ď á q u i v a 1 e n c e ) pour S5. La re g le H (comme " n é c e s s a ir e “ ) , sem blablem ent, exprime qu'une form ule e s t n é c e s s a ir e dans un monde, s i e l l e e s t v r a ie en to u t monde а с с е ззД Ы е au monde c o n s id é ré . Nous noteron3 le s ensembles 3Ómantique3 corresp on d ents Smi, SmS4, SmSS.
Syetŕm ea pureirent rtéon t iq uHs D, DT, OSA. DS3
A x iom atiq u e. t l i e e s t tró s v o is in e de ľ axiom atique des oyütemea p n tiq u e s j pour П (ensemble АхО):
n é í.O O p « i i e s t o b liq a t o ir e que p, АО 1 0(p э q) э (Op э 0q)
A02 Op э -0-p,
«О h - * -+ h - 0 / *
On cemaiquo quo ľ axiom« A02 n 'a pas la s tr u c t u r e Op э p, c e l i e qui c o rre s p tjn d ra it exaotemont 6 1' axióme u n tiq u e # 2 , c a r un é t a t do chores o b lif ja t o u e n 'o s t p as, par lá moine, vra x . tn revan ch e, puisquc -0-p veut d ir e q u 'i l t?st pe.riai3 quo p, A02 exprime ce tru ism « n o rm a tif, que ľ o b lig a t io n lm p liq ue logiqunment la p e rm issio n .
La r ô y le HO peut choquer n o tro i n t u i t i o n . E l l e n 'e n e s t pas moins a d m is s ib le , aprés une réform e du concept ď o b 1 д. g a t i o n, réform e qui s ' Impose i c í pour s i m p l i f i e r au maximum 1' e d i f i c a t i o n des syatémee logxques. On comprendra b ien le sens de c e t t e réío rrae, lo rsq u e nous aurons préseritd le a modal it é s d tion tiq u es, llé e s aux w o d a lité s a n tiq u e s dans un môme syst&me sém antique.
A jou tan t des axiumea du genre Q(0p 5 p ) , Op з () Op, -Op э O-Op, on peut encore d iS fin ir des sy3temes O f, OSA, 035, sur le s q u e ls nous r/ in s is t e r o n s pas pour le moment.
Sriman t iq u e . Les deux r é g le s M et N que nous avons vues c i- desaus á propos des system es ontxques d o iv e n t é t r e rem placées par le s s u iv a n te s :
В. S i dana un monde w( fig u ro une formule 0 / dn va le u r 0, a lo rs 1 1 d o i t у a v o i r a u m о 1 n s u n monde W; tel que Sw( Wj dans leq u el fig u re / avec la v a le u r 0.
A. S i dans un monde fig u re une formule 0 / de v a le u r I , alore e n t o u t monde w. t e l que S w i d o i t fio u r e r / avec la va~
le u r I . 1 1
E lie s ont apparemont tout к f a i t la mfime s tru c tu re que le a rrgles И e t N, mals m aintenant, outre q u 'i l eat question de 1' E v a lu a tio n de ľ o b 1 i u a t o i r e , la r e la t io n condidáräe n 'e tit p lu s ľ a c c e s s i b i l i t y Rw( Wj , male ce que noue appol- le ro n s la p e r m i e s i b l l l t é , notée Šw, . Pour ľ instant, sans a u tre p r e c is io n , noue d irons que le monde wj eet p e r m i s s i b l e pour le monde Uj , s i toutes le s o b lig a tio n s du second sont r é a lis é e s dans le prem ier, Contrairem ent au cas de K, la r e la t io n S n 'a aucune raiso n ď é t r e r é f le x iv e . T o u te fo is, la v a lid a tio n de ľ axióme A02 Op э -0-p exlge une n o u v e lle p ro p rié té do la r e la t io n S:
Op э -0-p l 0 01
Pour v a lid e r ľ axióme, nous proccidons par ľ absurde en le supposant in itia le m e n t faux (v a le u r 0 ). Cecl conduit á a tt r ib u e r la v a le u r v r a i ( t ) k chaque o b lig a tio n Op e t 0-p. On v o it a lo r s , que le s ré g le s A e t B cl-dessus ne s u f f ir a ie n t pas, á e lle s s e u le s , k parachever la dem o nstration . Mala s i l' on suppose en o u tre , que p o u r t o u t m o n d e 1 1 e x i s t e a u и o i n s u n m o n d e p e r m i s s i b l e , a lo r s la preuve sémantique de la v a lid it d de A02 a' achôve comme s u it :
wi Op d -0-p, 1 0 01 " i P -P.
1 10
le monde Wj, dans le q u e l la p ro p o s itio n p d e v ra it é tre a la fois v r a ie e t fau sse, e s t e x p l l c i t e m e n t i n c o n s i s t e n t e t la fau sse té de ľ axióme e st im p ossib le. A in s i aux deux ré g le s A e t B doit-on en a jo u te r une tro is ié m e , qui s'exprim o par:
C. Pour tout monde Wj 11 d o i t y a v o i r a u m o i n s u n monde Wj t e l que Sw^wy
Ľ' oat la s é r i a l i t é de la r e la t io n S . Les systém es (IT, 0S4, 0S5 a jo u te n t á c e t t e p r o p r ié t é , do m aniére c u m u la tiv e , e t r e s p e c tiv e m e n t, le s p r o p r ié t é s de p o s t - r é f l e x i v i t é (un monde e s t en r e la t io n avec lui-raeroe, s i du moins i l e s t d é jä p e rm is s ib le pour un a u t r e ) , de t r a n s i t i v i t é et de p o s t - s y m é t ŕ i e ( d e f i n i t i o n s e m b la b le ). Les ensembles sém antiques qui en r é s u lt e n t se ro n t n otes SmU, Sm lil, SmBS4, SmDSS.
S y s téme purement t emporel R
I I y a p rin c ip a le m e n t t r u i s m aniéres ď exp nm er . le temps en lo g iq u e des p r o p o s itio n s : en employant s o lt des temps verbaux (p r e s e n t , p assé, f u t u r ) , s o it des " la p s de temps O r ie n t e s " ( a u jo u r ď h u i , h ie r , d e m a in . . .) , 901t e n f in des d a t e з . C e tte d e rn ié re m ariiére e s t évidemment la p lu s r ic h e de p o s s i b i l i t é s ď e x p re s s io n , p a r t ic u lié r e m e n t lo rs q u 'o n a a u s s i a f f a i r e ä des m o o a lité ä o n tíq u e s e t d é o n tiq u e s. I ' uxiomat íque e s t la s u iv a n te
(ensem ble AxRh
O é f.R Rtp » i l e s t r é a liu é 5 la d a te t que p, A tl R t(p э q ) 3 (R tp o R t q ) , At2 Rtp • -Rt -p, At J R ť Rtp • R tp , R t l j— / —* j _ R t / , Rt2 j— Rt / —* ł ( t '»on 1 ib r e dans / ) ,
*~а sémantÍq u e , quant á e l l e , met en oeuvre un ensemble de m ond es-liés e n tre eux par une r e la t io n ď a c c e s s i b i l i t é te m p o re lle (w e s t post^neur k W j), d on t, pour des r a is o n s de b r ié v e t é , nous p re fé ro n s ne pas p a r i e r . Nous a llo n s v o i r , en re v a n ch e , comment c e t t e sém antique s ' a r t i c u l e avec c e l i e des m o ä a lité s o n tiq u e s e t d é o n tiq u e s.
S y s témes o n tiq u e s e t tempore is RT, R S 4 , RS5
Ou p o in t de vue ax^om atique, ces systém es sont d é f in is p ar la xéunion des ensembles AxT, AxSA, AxS5 e t de 1*ensemble AxR, c i- d e ss tis , a q u o i 1' o n d o i t a j o u t e r d e s
J e s d i m e n s i o n s o n t i q u c e t t e m p o r e l l e , le tout formant 1' ensemble axiom atique AxKT, AxKS4 ou A xltSi. Ces axiomes sont le s s u iv a n ts :
A®11 Rt«p * R t* l!tp ,
ft*t2 t* < t --- ► Rť«R-tp => R-t*Rtp.
Mais с ' e st i c i que le double tra ite m e n t axiom atique e t siím anti- que s 'a v é r e in d is p e n s a b le e t fru c tu e u x . C a r, sans ľ a n a ly s e sóm antique, on p e r c e v r a it mal la s i g n i f i c a t i o n de ces nouveaux axiom cs. Or la sem antique, lo in de com pliquer le s ch o ses, le s é c i a i r e tré s sim plem ent.
Sem antique. Pour exprim er sémantiquement la te in p o ra lis a tio rt des m o d a lite s o n tiq u e s , í l s u f f i t de rep re n d re la sdmantique des system es o n tiq u e s , e t d 'y rem placer le s m o n d e s par des r o u t e s . Les ro u te s sont des ensembles de mondes ordonnes chronologiquem ent. Assurém ent, c e c i p a r a lt tou t sim p le ; en f a i t , touto la q u estio n e s t de d é f i n i r correctem en t la s tr u c t u r e de ľ ensemble des ro u te s . C e tte s tr u c t u r e e s t a lo r s d é f in le de la m aniere s u i va ň te .
On a des r e g ie s И e t N analogues ä c e l i e š des systém es purement o n tiq u e s :
M. S i sur une ro u te cfj f ig u r e á la d ate t une form ule • / de v a le u r 0, a lo r s 1 1 d o i t у a v o i r a u m o i n s u n e route cr. t e l l e que Rt<r,o., sur la q u e lle J f ig u r e a la date t avec la v a le u r 0.
N. S i sur une ro u te cr, f ig u r e ä la d ate t une form ule ■ / de v a le u r I , a lo r s s u r t o u t e ro u te a t e l l e que Rto a, d o it f i g u r e r / ä la date t avec la v a le u r I .
La m o d ific a tio n e s s e n t ie ll e e s t qu' i l fa u t c o n a id é re r maintenant une r e la t io n t e r n a ir e R tffjO j, exprim ant que la ro u te or• e s t a c c e s s ib le pour la ro u te a. á la date t . C o n sid é ra n t to u t de s u it e R5>, le systéme phénoménologiquement le p lu s com p let, le s p r o p r ié t é s de la r e la t io n s 'e x p rim e n t comme s u it (p o ur to u t in s t a n t t et to u te s ro u te s cr. , cr e t a. ): 1 J К - r é f l e x i v i t é (p a r ra p p o rt aux r o u t e s ) —» R t o ^ . , - s y m é trie R t c r o r . --- * R t o ^ - t r a n s i t i v i t y (Rto^cTj e t Rta^cxk ) — ► R t o ^ , - r a m if ic a t io n ( ť < t e t R t o ^ ) ---► R t ' ^ O j .
A p rem iére vue, ces p r o p n é t é s peuvent p a r a lt c e compliquóee; en r é a l i t é , e l l e s t o im a lis e n t des in t u it i o n s extcémement s im p le s . Car en i d e n t i f i a n t la r e la t io n Kto^o^ avec le f a i t que le s deux ro u te s a Ł ont tous lu u rs é t a t s du monde en commun au moins duns to u t le passé e t le p rä s e n t de la date t , ces p r o p r ié t é s corresp on d ent to u t stmplement a la s t r u c t u r e r a m ifié e v e rs ľ a v e n i r , i l l u s t r é e par le schéma r.u ivan t e t p a rfa item ent conform s k nos in t u it i o n s le s p lu s o r ü in a ir e s en m a tié re de tem poral i té ( l e f u t u r e s t v e rš la d r o i t e ) .
Une p r o p o s itio n f u t u r e , rtó c e s s a ire a un in s t a n t donrié, est une p r o p o s itio n v r a le sur to u te s le s ro u te s qui d iv e rg e n t ä c e t in s t a n t . B ie n entendu, dane иез c o n d it io n s , une p r o p o s itio n passée e s t par la-méme n é c e g s a ire ; merne une p r o p o s itio n s tr ic te m e rit p ré s e n te ľ e s t a u s s i, ce qui n 'a r ie n de p a ra d o x a l.
Ľ axióme c i- d e s s u s A®t2 t r a d u it , on le d e vin e ( e t c e la se démontre assez f a c ile m e n t ), p recisém ont la p r o p r ié t é sém antique de la r a m i f i c a t i o n .
Sy*táaes ontiques ę t déontiques í-Df. S4-0S4. S5-OS5
Four s i m p l i f i e r , ne raiso nn on s que sur le p rem ier de cea
ьувЧемеа.
Ои p o in t ое vue a x j oma 11que, cumrne to u t a ľ heure , on d o it combiner des élém ents is s u s de deux dim ensions d if f é r e n t e s . On r e u n it done le s ensembles Axl e t AxUT, e t la q u e s tio n e s t do s a v o ir ce que ľ on d o it a jo u te r comme axiome p rop re au rapprochement des deux o rd re s o n tiq u e e t d é o n tiq u e . Or i c i e n co re , la c o n s id e ra tio n de la sém antique nous permet de c l a n f i e r nos i n t u i t i o n s . (.'axiom e qui c o n v ie n t s ' e c r i t :
A*0 * p Э Op
c .- ä - d . que le n é c e s s a i r e im p liq u e 1' o b 1 i g a- t o i r e . I I y a évidemment une p a re rité de s i g n i f i c a t i o n e n tre c e t axiome e t la r e g ie purement o n tiq u e RO, qui pose que pour tou te
these sa n écessix e e s t également th é se . Ľ a n a ly se sémantique ex- p liq u e c e tt e p aren té e t le c a r a c té re assez étran g e de ces fo r- m ules,
Se'mantique. Les s tr u c tu r e s Smi e t SrnOT sont r e p r is e s . La s e u le q u estio n d é lic a t e e s t de déterm in er le s rap p o rts e n tre le s r e la t io n s R et S, resp ectivem en t ď a c c e s s i b i l i t y e t d e p e r m i s s i b i l i t é e n tre le s inondes. Or nous avons vu qu'un monde p e rm is s ib le e s t un monde dans le q u e l to u te s le s ob lig a t io n s sont re m p lie s . Hormia c e c i, u n t e l m o n d e n* a a u c u n e r a i s o n d e d i f f é r e r ď u n m o n d e a c c e s s i b l e o r d i n a i r e . Mais c e la veut précisém ent d ir e que la r e la t io n S i m p l i q u e la r e la t io n R. Les théses - qui sont v r a ie s dans tous le s mondes absolument -, de merne que les p ro p o s itio n s n e 'ce ssa ire s - qui sont v r a ie s dans tous le s mondes a c c e s s ib le s au monde donné -, sont done également v r a ie s dans tous le s mondes p e rm is s ib le s . C 'e s t done q u 'e lle s sont o b lig a - t o i r e s , ce q u 'exp rim ent axiomatiquement la re g le RD e t 1 'axióme A*Ü.
Sy3ténies on tiq u e s , déon tiq u e s et te m poreis RT-OT, RS4-0S», RS5-0S5
Nous pouvons íin a le m e n t e ff e c tu e r la fu s io n des t r o i s ord res de dim ensions. Commenęant par RT-OT, nous co n s ta te ro n s que, axiomat i q uement, c e t t e fu s io n se t r a d u it par la reunion des p reced en ts ensembles AxT, AxUI e t AxR, ä quoi on a jo u te ra le s axiomes propres aux fu s io n s p a r t i e l l e s re n co n tré e s c i- d e s s u s , A*0, A * t l, A#t2, p lu s deux axiomes prop res ä la fu s io n des moda- l i t é s déontiques e t te m p o re lle s , qui sont analogues ä A * t l et A*t2:
AOtl RtOp a RtO R tp ,
AOt 2 ť < t --- * R ť 0 (R ť ORtp О RtO Rtp)
(rem arquer la s tr u c t u r e légérem ent d if f e r e n t e de A0t2 par rap p o rt ä c e l i e de A * t2 ).
Mais i i fa u t encore a jo u te r un axióme p r o p r e a l a f u s i o n s i m u l t a n é e d e s m o d a l i t é s o h- t i q u e s , d é o n t i q u e s e t t e m p o r e l l e s . I I s ' é c r i t :
e t son in t e r p r é t a t io n , ä nouveau, e x ig e 1' a n a ly s e sém antique. A c e c i, le systéme RS5-OS5 - pour ne p a r ie r que de l u i - a jo u te ľ axióme propre de S 5 , p lu s :
A*054 Op О «Op.
Sem antique. C e lle de RT-BT combine le s sém antiques des systém es RT e t U I. P lu s p récisé m en t, e i l e comporte deux r e la t io n s :
- Rtffjff. ď a c c e s s i b i l i t y s i m p l e e n tre ro u te s , eu egard á une d ate donnée t ;
- S tcT tfj de p e r m i s s i b i l i t y e n tre ro u te s , eu ćgard ä une date donnée t .
La seconde de Des r e la t io n s se comprend de la m aniere s u iv a n te . S i la ro u te cr e s t o r d in a ir e , c .- á - d . non p e r m is s ib le pour une a u tr e , la ro u te l u i e s t confondue ju sq u ' k la d ate t . E n s u it e , la seconde ro u te d iv e rg e de la p re m ié re , en devenant "bonne" á p a r t i r de c e t t e d a te . A in s i, to u te ro u te p e rm is s ib le e s t p arta g é e en deux b ran ch es, l'u n e o r d in a t r e , ľ a u tre "bo n n e", á une d ate que nous a p p e lle ro n s d a t e c a r a c t é r i s t i q u e ( l e terme de "bon" d o it b ien súr é t r e p r ls en un sens t r é s g e n e ra l, au máme t i t r e que c e lu i d* " o b i i g a t o i r e " ) . S i la ro u te e s t d é já p e rm is s ib le e t s i la date t e s t p o s te r ie u r e á sa d ate c a r a c t y r i s t i q u e , le s ro u te s ff. e t ff^ peuvent 6 tre confondues au d e lá de t dans l ' a v e n i r , la p a r t ie bonne de ff^ é ta h t p e rm is s ib le pour elle-méme ä p a r t i r de sa d ate сагат c t é r i s t i q u e .
Les r é g le s ď e v a lu a tio n s des o p é ra te u rs • e t 0 é ta n t le s mémes que ci-deseuB (r é g le s M, H e t A, B ) , on re tro u v e le s p r o p r ié t y s de la r e la t io n R p ropre au systéme R7 ( r é f l e x i v i t e e t r a m if ic a t i o n ) , e t l 'o n d o it a jo u te r le s s u iv a n te s : -
sy ria lité
de S ( V t X V c r ,) ( Эо*> S to jo r., - p o s t - r é f le x iv it é de S - p o s t- ra m ific a t io n de S - in c lu s io n R-S i - p o s t- in c lu s io n S-RLes deux p rem iéres p r o p r ié t y s ne p ré s e n te n t aucune d i f f i c u l t y . La tro is ié m e e s t une p o s t - r a m i f i. c a t . i o ň. et non
Stff^ffj - Stffj ffj , ( V < t et S ť ď jf f . e t S t j r f f . ) — * Sťffjďk» J J ^ Sto^tfj —— ► ( ť < t e t S ť c^ ff^ e t R t d j ) — ► S t ^ f f k .
pas une sim ple rami I ic a t io n , c a r la dato c a r a c t e ŕ i s t i q u e ä l3q u e lle une routo p e rm is s ib le d e v ia n t bonne jo iie un r o le essen- t i e l . Pour r e c u le r dans le passé la date de p e r m is s ib ilit é ď u n e route par rap p o rt й une a u tre , i l fa u t que la prem iére s o it tiien d éjá p e rm is s ib le ä la date a n té rie u re ä la q u e lle on veut зе r é f é r e r . S in n n , e i l e n 'a u r a i t , pour le v o is in a g e ď une t e l l e d a te , qu'un c a r e c te re simplement o n tiq u e , e t r ie n ne p e rm e ttra it d 'in - f é r e r la v é r it é de la r e la t io n de p e r m is s i b ilit é . On re tro u v e , i c l tem p o ralis é e , une s it u a t io n analogue ä c e l i e que d é c r it ia propriété de p o s t - r é f l e x i v i té .
11 c o n v ie n t d’ a u tre p a rt de ne pan confondre 1* in c lu s io n R-5 avec la p o s t- in c lu s io n S-R. La prem iére de ces deux r e la t io n s e st tou t ä f a i t sem bluble ä c e l i e qui a é té mentíonnáe pour le s systém es mélangeant le s m o d a lité s on tiq u es e t d éo n tiq u e s, á c e c l pres que le temps e s t m aintenant p r is en compte. E l l e correspond í» 1*axiome A*0. ta seconde, en revanche, e s t de nouveau une p r o p r ié té du type "p o s t- ", c.-b - d . qu' e l l e expriine une con d it io n qui n ' a lie u que lo rsq u e ť e n tre e dans le s mondes permis- s ib le s e s t d é ja f a i t e (dans 1' énonce de la p r o p r ié t é , c e t t e e n tré e se f a i t ä la d ate ť , e t la c o n d it io n 'd 'in c lu s io n S-R est r é a lis á e ä la d ate s tric te m e n t p o s té r ie u r e , t ) . Ľ axiome cor respondent e s t A *0 t. La sém antique permet m aintenant H'en comprendre le sen s. Toutes le s ro u te s a c c e s s ib le s ou p e rm is s ib le s pour une route elle-roéme d é já p e rm is s ib le , et é une dato об c e tt e ro u te e st bonne, to u te s ces ro u te s ne peuvent é tr e que bonnes, car la sem sntique suppose que le s v a r ia t io n s p o s s ib le s du bon ni? peuvent que r é s t e r bonnes. S i ce n 'é t a i t pas le c a s , le s é t a t s d é c la ré s antérieu rem erit bons a u ra ie n t co n d u it ä des é ta t s "m au vais" e t n * a u ra ie n t done pas é té réelem ent p a r f a i t s . 11 fau t bien comprendre que c e c i n 'im p liq u e aucun determ inism e n o rm a tif, c a r l ' in t e r p r e t a t io n de la sém antique sous-entend que le monde r e e l n 'e s t jam ais bon. le s é t a t s p e rm is s ib le s ne jo u en t qu'un rôle de parangon, de modéle a s u iv r e dans l ' a c tio n , q u 'i l s e r a it tout ä f a i t i l l u s o i r e ď im ag an er a v o ir a t t e i n t un j o u r . . .
Quant on a jo u te aux p r o p r ié té s m entionnées, c e lie š qui con vienn ent pour d é c r ir e le systéme R W -O Si ( l a t r a n s i t i v i t é de R , * la sym é trie de R e t ce qu'on peut a p p e ler la t r a n s i t i v i t é RtS, exprimée par (R tc^ o . e t S t c r ^ ) --- *» S tc ^ a ^ ), la sémantique s ' i l l u s t r e tré s simplement par des schémas du genre s u iv a n t:
le s p a r t ie s p o i n t i l l é e s re p ré s e n te n t le a branches bonnes des ro u te s . Conformément ä ce qui a é té e x p liq u é , dés q u'une ro u te d e v ie n t bonne, e i l e le r e s te e t e l l e ne se r a m if ie , au d e lá de sa d ate c a r a c t é r is t iq u e , q u 'en ro u te s dont le s branches du fu tu r sont égalem ent bonnes. On v o it que la s im p lic it é du schema o n tico - -déon tico-tem p orel se t r a d u it par des elem ents sém antiques re la tiv e m e n t com plexes, e t par des élém ents axiom atiq u es a u ssi complexes et moins i n t u i t i f s . Le rapprochement de ces deux typ es d 'é lé m e n ts permet de r e n fo r c e r la com préhension que nous en avons. Or ce rapprochement e s t mis en oeuvre par deux groupes de m é t a t h é o r é m e s : d'un e p a rt seux de la s o l i d i t é (a n g la is ‘'so u n d n ess") des systém es, ď a u t r e p a rt ceux de le u r c o m p l é t u d e . Dans le p rem ier qroupe on é t a b l i t que to u te thése e s t v a lid e , dans le second c 'e s t ľ in v e r s e qui e s t prouvé, c.- ô - tí. que tou te e x p ressio n v a lid e e s t th e se . Les dém o nstration s du prem ier groupe ne sont pas t r é s d i f f i c i l e s . I I s u f f i t de m ontrer, pour chaque systém e, que le s p r o p r ié t é s sém antiques v a l i dent b ien le s axiomes e t co n serve n t le s r é g le s ď in fe r e n c e . Les p reuves du second groupe, au c o n t r a ir e , sont autrem ent é p in e u se s. Nous voudrions en d ir e quelques mots i c i .
2. S tr u c t u r e pé n é ra le j le s pre z v eš de complétude
Puisq ue l c systéme que nous co n sid é ro n s солше le m e ille u r (du moins dans le cad re de c e t t e é tu d e ) s 'a p p a re n te á S5, on p o u r r a it e sp é re r que la preuve de com plétude par f o r m e n o r m a l e c o n j o n c t i v e m o d a l e , q u i c o n s is t e é r é d u ir e au p rem ier degré modal n 'im p o rte q u e lle e x p re s s io n , p u iss e s 'é te n d r e au p rése n t c a s . M alheureusem ent, on se rend fa c ile m e n t compte q u 'il n ’ en e s t r ie n . Car ce genre de preuve repose sur des théorémes de ré d u c tio n , comme * (p v * q ) s (* p v * q ) , q u i, d é jä dans un systéme simplement a n tiq u e e t tem p orel, ne se la is s e n t pas géné- r a l i s e r . A i n s i , p. e x .,
R t* (p v R ť * q ) a (R tB p v R ť * q )
e st val telo pour ť ^ t , ma i s in v a lid e pour ť > t . et le s re d u c tio n s ne sont pas p o s s ib le s . Au passage, on touche lá du d n ig t, en quelque s o r te , le f a i t que le temps e s t s u s c e p tib le de c o n fé ť e r h chaque m oríalité une s ig n if ic a t io n p rop re.
I I fa u t done employer un a u tre type de dém onstration de com plétude. l e p lu s d ir e c t e s t p e u t- é tre c e lu i qui c o n s is te ä b a t i r la preuve ď u n e form ule v a lid e d 'a p ré s la s tr u c t u r e mSme de son diagramme de v a lid a t io n . C 'e a t ce que nous avoris f a i t , en c h o is is s a n t le s t y le de Hughes et C re s sw e ll 1968.
Pour prouver que:
*= f * (— f
on a s s o c ie ä chaque monde w- (a chaque route o^, pour le s systemos te m p o ra lis é s ) du diagramme de v a lid a t io n de У une c e r t a in e form ule w | (ou orj), c a r a c t é r i s t i q u e des contenus v e rifo n - c t io n n e ls de ce monde (ou de c e t t e r o u t e ). On c h o ia it c e tt B f o r mule de t e l l e s o rte que le s t r o is c o n d itio n s s u iv a n te s se tro u ve n t re m p lie s :
C l. S i Wj ( f f . ) e s t e x p íic ite m e n t in c o n s is t e n t, c .- á - d . s ’ i l e x is te une p a r t ie b ien formée (P flF ) de (tí^ ) á la q u e lle le s v a le u r3 v r a i et f a u x ont é té a t t n b u é e s h la f o is , a lo r s
(ь * y
-C2. S i í ° u Sw-Wj ou Rtw^w- ou S .tw .w j), si^-w ^ (ou|_d ^) a lo r s . [ . и ' ^ о и l-rf j ) .
C J. Uans le саз du monde ou de la route . i n i t i a l e , w j ou tf'j n e s t a u tre que la form ule У elle-méme.
La c o n d itio n Cl amorce la p reu ve, C2 la transm et de monde en monde (ou de ro u te en r o u t e ), e t C3 l'a c h é v e . C e c i, t o u t e f o is , n 'e s t que le schéma t r é s g én éral des dem onstrations de com plétude.
En e f f e t , la d e f in it io n de la form ule c a r a c t é r is t iq u e d o it é tr e m od ifiée se lo n le s monde3 ou ro u te s auxquels on a a f f a i r e . C e s t p . e x . :
a v -ôj v . . . v -0k pour un monde simplement a c c e s s ib le du systéme I ou p e rm is s ib le de Ü, dans le q u e l cc e s t la form ule issue de 1 ' a p p lic a t io n de la re g ie H ou U qui a " c r é é “ le monde, e t dans le q u e l le s (3 sont le s form ules is su e s de 1 'a p p lic a t io n de la re g le К ou A;
a v -Pj v .. de № 4 e t O S);
v -/3k v Opj v -0/3k pour un monde perm issible
Rto,otv v . . . v -Rt^ök pour une ro u te simplement a c c e s s ib le de КТ ou И1 -01, oil t- e s t la d ate de d iv e rg e n c e des ro u te s en r e la t io n , e t t ; ^ t«, j
. , v - R t.O ^ ) pour une ro u te p e rm is s ib le R T jO (R t« otv - R tjO l v .
ou le s t ; ont la méme s i g n i f i c a t i o n e t ou e s t la de R I -01, w« * vw » j, Ull l АУ ШЫ1ИЙ J i^ llillb O U U I I Ь I. UU I ^
d a t e c a r a c t é r i s t i q u e de la route cr..
D'un systéme ä l ' a u t r e , la r e a l is a t io n de la c o n d itio n C3 ne change guére; c e l l e de C l change assez peu; mais c e l l e de C2 v a r ie beaucoup e t reclam e de sé rie u x e f f o r t s . Cependant, ces e f f o r t s sont recompenses, c a r c 'e s t la r e a l i s a t i o n de C2 qui f a i t vraim ent tro u v e r et comprendre le s s tr u c t u r e s axiom atiques e t sém antiques corivenab les. P a r e x ., dans le cas de RI-U T, í l у a c in q cas p o s s ib le s de r e la t io n e n tre ro u te s ; donnent une i l l u s t r a t i o n : le s f ig u r e s s u iv a n te s en cos I cus II ‘ Г l T ) C Q SIII
___ О
cas IV # cas IV"
cf.
T, ■
En o u tre , le s systém es de type S5 (0 S5 , R S5 , RS5-0S5) ex ig e n t une demarche p a r t i c u l i é r e pour la p r is e en compte des p r o p r ié té s de s y m e trie ou de p o st- sym é tri e . On p e u t, comme nous ť avons montré (B a ilh a c h e , "Normes e t m o d a lité s ", 1983) c o n s io e re r un diagramme d 'un t e l type comme un diagramme de type S4 e n r ic h i p r o g r e s s i v e m e n t par ľ a d d itio n de la s y m é trie , e t done par c e l l e des nouveaux mondes e t des rio u v e lle s form ules qui en r é s u lt e n t . Le souci d 'e t r e b re f nous empéche i c i d 'e n t r e r dans p lu s de d e t a i l s . De 0 á R I -ОТ, en p assan t par tous le s systém es
in t e r m é d ia ir e s , le s dém onstrations prennent p lu s de 80 pages. Pour p lu s d 'in fo r m a t io n s , nous renvoyons b ľ ouvrage que nous venons de m eritionner.
U n iv e r s it é de Nantes fra n c e
P a t r ic e B a ilh a c h e
AKSJOMATYKA A LOGIKA 0E0NTYCZNA
Zagad nienie aksjom atyki w lo g ic e d eon tycznej analizow ane j ? 3* przez au to ra z dwu punktów w id z e n ia . Pierw szy z n ich jest. b a rd z ie j f ilo z o f ic z n y . Bada s ię na jego g ru n c ie z a le t y i wady aksjomatów c z y s to d e o n tycz n ych . A n a liz a ta wskazuje na konieczność wprowadze n ia do l o g i k i d e o n tycz n e j p r z e s tr z e n i w stosunku do n i e j zew n ętrz n e j, t j . p r z e s tr z e n i m odalności k la s y c z n y c h . Drugi punkt w id zen ia j e s t n a tu ry b a r d z ie j te c h n ic z n e j. Chodzi w nim głów nie o dowody z u p e łn o śc i wymagane na g ru n cie l o g ik i d e o n ty c z n e j. Z r a c j i tru d n o ś c i pom ija s ię cz ę sto ic h p r e z e n ta c ję . Autor wykazuje w p racy n ie zbędność dowodów tego ro d z a ju .
