LOGIQUE DU 1`” ORDRE DANS LES TOPOS ELEMENTAIRES
Contents
1. Soit p c n De par sa construction p Li un l ment de Hintikka et on PDT V gt UA Fin de la d monstration du sous lemme 2 Voici maintenant la deuxi me tape Sous lenme 3 d Si p U r est un l ment de Hintikka il existe un e F i collection de Hintikka C U telle que pe C et v U p On suppose ici que l on dispose d une double suite de variables libres qui ne sont pas dans UT On suppose a ssi que l ensemble des sous formules des formules de p est totalement num r On appelle F formule une formule sign e F d une des trois formes F 406 F 6 V F x9 GO Si d est un ensemble de formules sign es on nose ds l ensemble des formules de sign es T On construit la collection de Hintikka petit petit 1 us Vs Up Etape O On pose p P pr Etape 1 Si p ne contient aucune F formule on pose 1 T Ve x U Sinon on consid re la premi re F formuie de Pr gt d v Si c est F b P U Te est V p consistant Si F 9 P V i est d montrable ra l est aussi On pose EET Vp UD Si c est F Y on pose P1 P QU T FO Ve Vo T i Si c est FAx x p Y Fb a est PDU a consistant Vu a E Si TY sa o ve Ut et 9 c T gt TO E P est d montrable Als x i l est aussi On pose mol F 9 p pu Geb UV Ve T P Dans tous les cas on tend p d en un l ment de H2. Si V fa seers est un ensemble fini de variables libres m V h suppos es rang es dans l ordre croissant om fotera X le produit X X Si V est vide XV 1 Er r b Li Soit t un terme de lt e V un ensemble fini de variables libres contenant c t Au couple t V on associe une fl che ev x X tit de la mani re suivant i i v SI ta a f af y est la projection canonique X gt X i 5i t e est une constante de type i lev est la compos e de lel et de la fl che X 1 le vl x gt el x i Si t f t t ev itl o euis IE sv t Narre VD MT TT n T i On remarque que si NW et V sont des ensembles finis de variables libres tels que VWoVoo t le diagramme Ww t W zu Xite x Pd EV im fm Ww v x ou la fi che X gt X est la projection canonique commute Scit une formule de d V un ensemble fini de variables libres contenant o Au couple d V on associe une fl che V CE o v X gt R de la mani re suivante Si r t t est atomique vl rlo EV loss eslE VD dia DR eav v v n Ix Si 6 WYAS9 respectivement Vv Y 80 9 V o diy wl lo vp v v VI lg y A le vi X vis ovi GAD gt Q resp vl v o jv vl 16 vb le vl so dyi lo vl Si 1 9 9 eo v vl je vl x LAIR d uis Notation Dans la suite
3. Si on remplace d montrable par d montrable sans coupure on aboutit au m me r sultat Une s quence F HAY qui n est pas d montrable dans T L J ou TLJE resp TLE ou T LKE sans coupure n est pas valide resp valide classiquement Ceci montre l analogue du Hauptsatz de Gentzen 4 Th or me xs v 2 RE 7 Si T est d montrable dans TL J resp TL JE TLK d 7 T HT LKE Te A est d montrable dans le m me calcul sans coupure Corollaire Si Tr A est d montrable dans T L J resp TL J E TEKS T LKE il existe une d monstration de T pe A dans ce m me calcul o toutes les formules qui figurent sont des sous formules des formuies de T et A et toutes les r gles employ es concernent des op rateurs logiques qui apparaissent dans les formules de let A Le corollaire d coule imm diatement du th or me par la consid ration des r gles de d duction autres due 1a r gle de coupure Remarque i Ce corollaire montre que ie calcul TL JE est un bon calcul pour les cat gories d ductives de B nabou Ces cat gories permettent A Vk Les P i d a s quences consid rer ici sont du type T f o la suite de l interpr tation des symboles v pour vrai droite a pour longueur i et o les formules qui apparaissent sont 3 crites uniquement avec A V Les axiomes de TL JE ainsi que les r gles pour A et V crits avec des s quences du genre a a r E F v ci des
4. er a Le but de ce papier est de pr ciser la logique du ordre qul fonctionne dans les topos ce qui sera fait par la description d un syst me de d duction ad quat Les id es principales sont les suivantes Le langage interne d un topos est li un topos particulier et m me aux situations particuli res l int rieur de ce topos particulier J entends par 1 que tout type de variable tout symbole de relation ou de fonction est li de facon immuable un objet ou une fl che donn du topos ce qui ne laisse aucune latitude l interpr tation du langage Le point de vue du lan gage interne apparait ici comme peu commode pour noncer des pro pri t s g n rales C est pourquoi le point de vue adopt dans la suite est celui de la logique ordinaire Le langage est donn priori ensuite on consid re les r alisations de ce langage dans les topos Ce sont les propri t s de cette nouvelle s man A tique qui sont 3 tudier 2 En logique ordinaire on est quelquefois amen consid rer qu une formule a plus de variables libres qu elle n en a r eile ment Souvent l criture Pa sees sa signifie que les variables libres de sont parmi does sd et non que As s8 sont l toutes des variables libres de amp Cela n introduit aucune compli cation Dans les topos il en va tout autrement Soit une formule avec une seule variable libre 23 de type X Sa v
5. l ment de Hintikka ar s ay IF p 2 tel que Ts P et Vel On suppose que l on dispose d une suite ET NE see de variables Qr libres qui ne sont pa dans vo p A 2 i On va raisonner sur les sous formules des formules de o Etro sous formule de est la plus petite reia ion r flexive et transitive contenant la relation 4 d finie par 1 Si 5 9 A 9 9 v 0 Y s 9 4 alors se et El i 2 Si alors y x P 3 si amp Vx Y Cx Ax V x pour tout terme t de Pf VOE L ensemble des sous formules des formules de g est d nombrable oupposons le totalement num r 6 o p 1 ges On construit une suite TR Us qu V o s ue U avec d us J el C ada sek Vele e as Et pour tout t cf y Fi M B V consistant Supposons D 3 U connu Posons n t f So q v n n id n n P i 09 0 1 On construit alors une suite finie v d UD PX nti ni Td o pi nt ie p TS ND don avec cP c od et Va e pad et pour tout K gf V consistant Supposons v d QU 2 connu Puisque d est U consistant trois possibilit s qui s excluent l une l autre peuvent se pr senter 1 Sd ne contient ni T6 ni F5 Alors d F 2 s ju as n K K n n n n 2 q contient T n K a dg YA O T U TY T est consistant Sinon on aurait un lisli d montrable avec Sc 4 i U TY TO et ve On peut sup poser que S contient T et TO Mais si D V O M es
6. t ER i i 3 i n TTE Les formules atcmiques dea sont les expressions rc o r est un symbole de relation de signature dees sd Pour l galit om derit eO uL COD 1 D Les formules de amp sont construites 3 partir des formules atomiques de ol par l application des r gles suivantes Si et Y sont des formules BAY bv 46 sont aussi des formules i i Si sas E est une formule a etant une variable libre qui Low m i LE n appara t pas forc ment dans soit d une variable li e qui n appara t pas dans et d signons par o x 09 le r sultat de la substitution de x toutes les occurences de a dans Alors y x G jc et Ax BOE sont des formules On notera oc 9 l ensemble des variables libres d une formale 4 d E r amp aiisations de amp E rF E Soit E un topos Imne E r alisation de ab est la donn e des l ments suivants Pour chaque type i un objet X de E objet de base de type i Pour chaque symbole de relation r de signature sees i une fl che jr TT AE TE E n Si oU est avec galit sera interpr t par la fl amp che 1 EER i X x our 4 fonction caract ristique de la diagonale Pour chaque symbole de fonction f de signature iji 1 n une fl che If Xx X x X ne constante GO i n J sera interpr t e par une fl che 1 NUS Notation i ij i
7. 7 3 1 To A et T EF A v 17 sont valides Tvl ja v vio v et Ir vL las v rov D Irvi sela vlv 0yh ter 4 5 6 7 8 9 10 et Pour Pour Si et Si et Si et Si et Si dans r ER SANT est valide V gauche VY droite T Irvi s fava v iev T T Inv a devis f T T eap et MV A est valide gt Ir v A als vi Lavia TO est valide F 6 p est valide E x WT n FO est valide uo Po AT sont valides Ivi lt LA V v 9 V 1 et Tvl A Twv slavia J P 6 Y te A A gt rvi aday vD as VI ACTA VE iv ERAD Ww C Pe HY est valide DANS avi lt ly v ra est valide rea 2 HA Vu a est valide amp LAN LA est valide c TV o v v vl ag V et a ne figure ni dans YT ni TV o P e 2 Vo tatz C vi p gt 192 V vadledlr vl A v De P Wx 0 v vlr lavha TV Ox 8 GOV lt av X et i n VER ste H est valide 44 i d LI E est valide soit une variable libre qui V ax x n est pas dans V la projection canonique p X X 2 11 Si T e A t V R et la fi che A x donnent une fl che r t p EV x ay got a je vi ub ded gsx aa EA Eea DE od amor ma mi mL s lavia daa oa o lt VD et 16 2 o 9 GOD si NOOD o Yx8 GT o p entr
8. BP est un sous objet du pr faisceau final Par Yoneda tout a de P p on peut associer de fa on bijective une fl che h P que l on notera encore a Soit 9 a 8 une formule de Pip On lui associe la fi che jrs n oie pue EES PESO 3 T 62 MIK h et si est close sans param tre i l D ai ed Q Le th or me s nonce alors t s i Pour toute formuie de P p ph lt gt isl y h Le th or me se d montre par induction sux la complexit de la formule en utilisant les propri t s logiques de Ens qu il est bon de rappeler l i Tout d abord i oblet classifiant R et sa structure On a Q p v Hom h 9 sous foncteurs de h Un sous foncteur u de h est caract ris par l ensemble D q C u q une Partie D n de C est associ e un sous foncteur de si et seulement si qe D sy qQ p et Vr re D Appelons parties satur es au dessus de p les parties de C dui v rifient cette propri t On peut poser Q p parties satur es au dessus de p ER avec comme morphismes de transition pour g p UB ssec ci Di Vas D Hire x gt a la La relation d ordre sur 1 est repr sent e par le sous objet gt 7 xE avec c p D D O DEP La fl che 1 2 5 Q choisit pour chaque p l ensemble Ig q gt pl dans Q p C est la partie as soci e h i P Scit X un objet de fus U un sous cobjet de X Si xe
9. gles de d duction qui vont tre nonc es sont directement copi es de celles du calcul s guentiel de Gentzen cf 4 Les s quences P Y utilis es sont du type TA o F et sont des suites finies de formules de ee On note T l ensemble des formules qui apparaissent dans la suite F V est un ensemble fini de variables libres contenant les varia bles libres des formules de T et A Definition ID v Fi Une s quence TrA sera valide pour une E r alisation donn e si pour cette E r alisation AN O W v be r avt lt Vel A yv dans Hom X 9 Si rT le terme de gauche est v yo Si A celui de X i droite est f i A vo uL v T A sera valide si pour tout topos E TA est va lide pour toute E r alisation de Ad v LI Enfin HA sera valide classiquement si pour tout topos P oom We NE bool en E THA est valide pour toute E r alisation de X Voici le syst me de d duction Axiomes EB pour toute formule et tout V fini contenant o d R gle structurale pour PTjc r i TA ETA dd B 13 Fu ui 4 di R gles gauches R gles droites C Af Ww T HA EG T FA 9 PRA PQOSAVFAY r AYPA TEA SAY v v Le CD rA T YEA FA PHA Y v revy pa Y taau PrA 9vV WO lEA 6 Uo EA v T 10 EA AT v x Nx PDEA 9 DO Ya D RA X XC Pr bY HAAN rr ew ji Vu al i
10. ie AE CE o e qs Proposition lisi vV est satisfaisable v est cit La compl tude par ia r ciproque x HL UP LU Th or amp me i si Si est rm n d est EE D monstration du th or me de compl tude La d monstration fait appel aux collections de Hintikka Une collection de Hintikka est une collection ordonn e C d ensembles p de for mules sign es de 4 munie d une application pie Ut valeur dans les ensembies de variables libres de ak On note U y l ensemble des termes de Construite avec les variables de LAS C et bad v rifier les conditions suivantes 1 Pour tout p Les contient les variables libres des formules de p et p est U p consistant MK 2 v 4 q eu D oue Ut 3 p 4 q mos TOEP THE da DY u e 7 4 4 4 T A Vcep Tep et TYEp 5 Fa cp Fbep ou FYep 6 TO vYEp gt TOEp ou TYep 7 Fv Yep sy F cp et FYep 8 Ttep F Ep 9 F 49cp sm Jjasp Teq 10 ThrVep gt Fep ou TYep 11 Fe ep x d qzp T eq et FYeq 12 TVx6 x ep 2 dac Vo To a Ep 15 FVx x ep Yre Ctp F t sp 14 TAX x ep Vte p TOE Ep 15 FAxe x lop dqzp Fae Vta Ff a stq L int r t des collections de Hintikka est 1a propri t suivante Lemme rout p de C est EE RR Le th or me est alors une cons quence imm diate du Lemme 2 p F est V consistant il existe une collection de Hintikka Kc ar 975 et un pe C tel que J c p et M us V p D monstration du lemme i d abord dans
11. Ens qui v rifie pour p qccC p lt q gt P p Pig et tel que pour tout p de C P p 6 On notera P p l ensemble des formules closes de Je param tres dans P p ds Une relation H entre l ments de C et formules closes de o param tres dans ko P p v rifiant o Si pe bsp et Vasp afr D pH ay sr pli et plitv 2 pvi Er p ou plitY 3 p Has EE 16e P p ec Vqzp que 4 pasy SEP gt YeP et Vazp af s qv 5 pk OG s da ec Pi p F8 a 6 pit x x z Yap Va c P q q H a EOT i E ET A une r alisation de Kripke on associe canoniquement une Ens r alisation de ja mani re suivante L objet de base est le pr faisceau P Si r est un symbole relationnel n aire de Jo Ir sera la p i it E i fonction caract ristique du sous foncteur R de P d fini par R p a TEER p ria ens a R est bien un pr faisceau vu la condition 0 Voici le th or me qui exprime que la s mantique de Kripke est un cas par ticulier de la s mantique introduite dans ce papier Th or me Soit une formule dad n variables libres Val 9 c 9 calcul dans la AT associ e ia wt i n j de Kripke est un sous foncteur de P et on 4 si n 0 Ya pa P p a seresa eVal o 9 PER PRO se es va Val 6 0 p J ensemble un seul l ment 4 gt p F6 Ceci peut s exprimer de facon plus agr able Soit h 1e foncteur Hom p
12. X p et Si q gt p on notera x l image de x dans X q La fonction carac r d t ristique X u y E R Mi o x i f 1 est donn e par u CP i x ba ig gt 9 i Ufqir g Le diagramme Es est bien un produit fibre i je AT de sF X gt O La structure d alg bre de Heyting de Q est donn e par r La fleche y La fleche f 1 A aui pour chaque p choisit dans Sp i La fl che A 9 xf amp avec a AX X ED DO ens ss DAD La fl che Ve pes nt avec B v p D D ps DUD Le La fl che Qa Q a fonction caract ristique de Y p D D i s a p DRE pt N d d La fl che Rm X qui vaut gt e 1 y f 6 7 p D pet gt p DR 4 d it dd Et maintenant des propri t s que l on pourra rapprocher des propri t s de ia relation H page 8 C Soit X un objet de Ens U et V deux sous objets de X i MAW p U p n V p 2 UV p UCp u V p R 3 5 gt V p x e Xp Yq gt p x g ula ou XKt V q i q Fa x e Xp Va gt p xp f U a q 4 4U p C 1 Soit Y un autre objet de Ens R un sous objet de XxY Puisque U gt V R Ed Uxtz gt R Y 5 M m ph x e Xp Ty e Yp x y R p Y Puisque NR U dr R gt Ux Y 6 AR p xe Xp IVasp VyesY Gu y RO Y d EF Th orie de la d monstration aal Les r gles de d duction Les r
13. et T p d o pH e et pr ce qui entra ne Alors par exemple F p donc p We 5 6 7 8 9 10 S1 11 12 Si 13 Vte EU Cp F Y t ep Vt e TUG 3 Si 2656 6 ii LANE LM T p Alors par exemple T 9 ep donc pH et i Fe Ep Alors F p et F T 4 P d o p F4 ce qui entra ne pr Si 4V per 7 Hi On utilise la propri t ThepVazp T eq Va gt zp FYeq Va gt p zx D pH Ft amp pq gt TYcdq iq HY ly Ep sedig 2 p eq dq p qg 2i pt TE p 3Va 3 D TE ap Y qp Fe F6 cpzdia p T eqet F9 e q da 2 gt p q 9 et qo gt ps 6 Vx Y x T tep ag TR T Y a p p H Y a Comme MOIN lt el on a pro F cp On utilise la propri t 5 page 12 a n variables libres PETERET Val Vv Tu On utilise la propri t pu a que Y On utilise la propri t cq ou TE ea Y qp q MA ou q pr VO Donc si PIN Tas a HEY Y E n et ainsi Val 6 YY p n Las a DI ce qui entra ne p 6 i A x Y x i bep Vaz gt ps T6cq la p Ve e UG qi t k Nt v Y vun i 2 4 Si a n variables libres 83 8 On a valt gr IMAA a eoa P DS A Ti a i m et ainsi Valla LU TOFMERT ce aui entraine p Ie 14 F0 cp lap da e Ula F v a qq da e Uta af Y a Comme v a 2 l l gt a
14. le cas La amm sans galit d FARNE i On consid re la Ens r alisation de c suivante e Le pr faisceau de base est EU 0n a Ep Po pour p q Si f est un symbole de fonction n aire f est d fini par Flo gy EVE t sou j Ed ft ges jt Si r est un symbole de relation n aire r est la fonction n mi caract ristique du sous foncteur R de TY d fini par Rp TE sees Uto TOE vere sp n Soit une formule dont toutes les variables libres sont dans Ve toute variable de U et plus g n ralement tout terme de OU 9 SAU que l on d signera par la m me lettre Ainsi comme la page 9 on associe la fl che on associe de fa on bijective par Yoneda une fl che h pi E rd P anl apt On remarque que si on remplace c par un ensemble V plus grand la fl che reste toujours la m me la correspondance entre fl ches de l ments de Q p q gt p gr Sous lemme i ET zz p irt La d monstration se fait par induction sur la complexit de Eus des pages 10 et 11 utilisant les propri t s logiques de 3 4 Si RR est atomique on a En effet ai pour variables libres Yu ness ev le diagramme Ese ee t R p et pit p t cela veut dire que tyret Rp p D T F p n est pas oa EN Finalement pe els Itl a On utilise ia propri t amp m Alors fT p
15. m qR e pha Fin de ia d monstration du sousrlemme Soit maintenant S une partie finie de pet V une partie finie de VU to contenant les variables libres des formules de S D apr s le sous lemme 1 Tes lt ph F YES pH v S l i V Ainsi A Le gt M N ce qui montre que list n est pas valide p est bien U p satisfaisable P f Il reste examiner le cas o est avec galit Dans la Ene rea lisation de F considexce plus haut L interpr tation de l galit fonction caract ristique de A gt VI TY d fini par t t e AIT t t p n est pas l galit standawd Soit n es PUR EV 1a plus petite relation d quivalence contenant et stable par les symboles de fonction tt sees t Ep E t eret E tisset v p On remarque cf page t4 que t t e p si et seulement si il existe une cha ne d galit E t t teile que V ce fE t t TOEP t C r E rg On considere alors la nouvelle Ens r alisation de Le pr faisceau de base est P qu L interpr tation d un symbole de fonction se d duit de l inter pr tation dans TU par passage au quotient grace la stabilit L interpr tation d un symbole de relation est l image par quotient de l interpr tation dans U A une fl che de hP dans P ne correspond plus maintenant un seul terme de TES mais une classe de termes de ET sy pour p Ceci pr cis on d montre pour cette nouvelle ns
16. on crira Y VlA 9 V plut t que A v vl lo vl A d signant alors une op ration bin ire sur Hom X SES ei De m me pour V et op ration unaire Si y x ve resp A x G y x Oy Soit a D une variable libre qui n est pas dans V Soit P la projection V canonique AE LL NEN NER Alors 2 vl V dya zo uta 3 resp A Ita y uta j Pa On remarque que si V et W sont des ensembles finis de variables tels que W tV 50 9 4 le diagramme MIER R M T d o v commute Notation Val V d signera le sous objet d fini isomorphisme pr s de X de fonction caract ristique 9 V Comparaison avec les s mantiques ordinaires La s mantique qui vient d tre d finie est plus g n rale que la s mantique classique Une r alisation au sens classique de est une Ens r alisation o les ensembles de base ne sont pas vides et Val la a n est autre que lasse sa gCa a 7 Ce qui est plus int ressant c est qu elle englobe aussi la s mantique de Kripke ER Pr sentation de la s mantique de Kripke cf 3 On se limite ici un langage G sans symbole de fonction sans galit et avec un seui type Une r alisation de Kripke de dy est la donn e des l ments suivants Un ensemble ordonn C lt s pi d signera le topos des pr faisceaux sur C consid r comme cat gorie valeur dans Ens C ie RR x Un pr faisceau P de
17. ER rs SEMINAIRE DE MONSIEUR BENABOU 1973 74 EXPOSE DE M COSTE LOGIQUE DU 1 ORDRE DANS LES TOPOS ELEMENTATRES ne L i M it LOGIQUE DU 1 T ORDRE DANS LES TOPOS ELEMENTATRES Ce papier suppose connues les notions de base sur les topos l mentaires que l on peut trouver dans 1 Pour des raisons de commodit les notations sont l g rement diff rentes en ce qui concerne les op rateurs logiques des topos gt J V sont remplac s par V A De plus il est pr f rable d avoir une id e des langages internes des topos de B nabou dont on trouvera une pr sentation succincte dans 2 Introduction R F le me DE Les exemples font appel au langage interne des topos Depuis que l on manie les langages internes des topos on se demande quelles sont les formules vraies dans les topos On sait de tacon empirique que les topos poss dent une logique qui ressemble l intuitionnisme Ainsi i objet classificateur d un topos est muni d une structure d aig bre de Heyting Cependant certaines choses ne se passent pas comme dans l intui tionnisme ordinaire Par exemple la formule Ax rx Vx rx qui est un th or me intuitionniste n est pas en g n ral vraie dans un topos Si x est de type X et r Vy i X 9 la valeur de Ax rx gt Vx rx est la fonction caract ristique du support de X image de la fl che X 1 Il n y a aucune raison pour que ce soit v XQ
18. ET ER VIS v droite o TES ek T Pl i a Une d monstration de FA x r x Vxr x dans T LJ et dans T L K qui ne peut pas se modifier en d monstration de a H x Ex Vx rx ratre la A ne Ax x vt a 24 Bi rd EE P V droite X r xrVx Y Xx an PPP EY ct droite F x rx Vx rz 16 ER Les calculs sont corrects La premi re close v rifier c est le Th or me Fi Ca las um qu BERE Pure Cas A sans galit I Si T A est d montrable dans TLJ resp T LK L4 n 3 YT HA est valide resp valide classiquement cas 4 avec galit a 1 51 T AV put d montrabie dans T L JE resp T L K E v TH 4 est valide resp valide classiquement On raisonne par induction sur la longueur de la d monstration tn note RE EE ivan v eei D abord le cas des calculs T LJ et TLIE u 1 Tr est un axiome p 8 est valide e oO N vf v uet Si FE est avec galit ECC te t et 1 V F t j ti HAE Eit A 2 OE gasse t FEEL se eet sont valides 11 suffit de remarquer que r ge a i G QD LG V C H a i p 1 i amp g b 555 a m b I Fases sa JTE b i it 1 n I n 4p G y 0 2i E bi ets Ai i Pn Y asenna HEC sese b sont valides v 2 Si T FA est valide in vla le OVE lt d v om Inv a fev AET Inv jv et T AY F est valide Fi
19. NV F b a tt I 2 LE 5 ETENE Nen EED AA AE e RE NE KS EE I Tq T Via Vita u 0 v mE Da EER e EE uo PNE y b d e Ax eO ra b rea Ax aq TE rt spa S Regie de coupure M PF 4 At Quand on ne consid re que les topos bool ens on utilise ce syst me tel quei sans restriction On notera TIK ce calcul s quentiel Par contre si l on veut travailler dans n importe quel topos il faut apporter la restriction suivante Dans les r gles droites pour N les suites qui apparaissent droite ont une longueur qui ne d passe pas Elles peuvent donc s crire Vua T0 p Ev re o a 0 a V Iden M regsvV peA xD aV 1 d I i On notera T LJ ce calcul s quentiel Si Y est avec galit ii faut introduire des axiomes suppl men taires Tout d abord quelques d finitions Un maillon d galit e t t entre deux termes t et t de mene type est une suite finie de formules telle qu il existe des termes i i i i uU V y vt y P avec t uv V 4 AV ST mor nem D id 1 n t u v pst v et que pour tout k Ig kzn Ou bien e t t contient V E MI Du bien 11 contient v EN Vo e t t ne contient pas d autre formule Une chaine d galit E t t entre deux termes de m me type est une juxtaposition d un nombre fini de maillons d galit e t t 3 e t t ees e t t Tout ceci sera plus clair si l on remarque
20. a nent vlg l v v Vx x c Vx x o p et ainsi EA As D EV est valide 12 Pour A gauche se traite comme 11 13 Si DE pla O9 Y vla o a g V et a ne figure pas dans I est valide Ivi o pP a Vy tall gt T I lt x GO VI et r Age Ro est valide V l4 Si lr CAN et To r A sont valides I E t jav y le vl et Ir v A CRIE latvia entra nent maypa ovi avis Je v D A IT VI Is VI v JA Yla et P AAN est valide Maintenant le cas des calculs T LK et TLKE TI faut re prendre les tapes V i 79 Si TT HA est valide classiquement dans un topos bool en VE A ovi g A v ravia davi valovi g ERAPR le vi la EL TV g fav v hov Yn et Ft A 8 est valide classiquement 9 Si Ts e AP est valide classiquement dans tout topos bool en VE a fev IA via v IPV lt lA Vi v DE vlv Ine v avt le v vl et Te AS gt y est valide classiquement 13 Si F A 8 ati 3 v tal ou af V et a ne figure ni dans T ni dans est valide classiquement dans tout topos bool en TV ep pelda VI on vleta vufal gt Tvl AO as vl pep Elala Vut E VERA RAY X A xb x V Inv lt LOAF v Ace x V et Fra BY e a OV est valide classiquement Les calculis sont complets Ii faut maintenant s assurer que toute s quence valide est d mon trable dans l calcul appropri On va suivre la d monstration de compie tude que l on peut trouve
21. aleur est une fl che eta Xens Si b est une variable de type Y et si on consid re t cotume formule en les variables libres a et b on peut lui attribuer la valeur b a b XxY 9 qui est la compos e de i a avec la projection canonique K Y X L ennui c est que l a b peut tr s bien tre le vrai de X xY sans que a soit le vrai de X Ceci emp che d appliquer tel quel le modus ponens Si l v b est le vrai de Y et V b gt a est le vrai de X Y il se peut que a ne soit pas le vrai de Y bien que 2 551 soit le vrai de XAT a La cause de cette difficult est que dans les topos les projections ne sont pas des pimorphismes autrement dit que tous les objets ne sont pas de support 1 Ceci est aussi vrai pour le topos Ens dans lequel on fait la logique classique ordinaire mais dans ce cas on s en tire en re fusant les r alisations vides EE L id e qui peut venir piur tourner la difficult est Ja suivante pr ciser chaque fois l ensemble des variables que l on veut consid rer Ceci am nera remplacer les s quences de Gentzen rA o T et A sont des suites finies de formules par les s quences Hn ou V est un enr semble fini de variables comprenant les variables libres qui apparaissent dans Fet ER S mantique Dans la suite d signera un langage du 1 ordre S coren Un ensembie d nombrable de types d sign s par 1 Pour chaque t
22. intikka dis M Pod Pa p au moyen des variables de ia suite 4 85 s qui ne sont as dans Ur et on poe P amp Po On d t que la premi re F formule i P si elle existe a t utilis e Supposons qu l tape n on ait construit une suite P V o P U Qo esu 8 AJ o D d l ments de Hintikka 4 2 2 2 avec p p U c De U o pour 2 gt K 2 k 2 K Tl m LE Etape n l Pour chaque k tel que 1 amp k 2 on consid re la premi re F formule de p non utilis e si elle existe et on proc de comme dans 1 tape 1 pour construire un nouvel l ment de Hintikka p id On pose Pr PL et on 2 K 2 K 2 K dit que la F formule consid r e est utilis e Soit C la collection de tous les Pa ainsi obtenus L ordre sur C est le plus petit ordre contenant lt on le note encore lt De par sa cons truction C e 0 est une collection de Hintikka Fin de la d monstration du sous lemme 3 du lemme 2 et du th or me vas 30 mes Wi 4 On a bien entendu un th or me de compl tud aussi pour les catculs TEK et T LKE La demoustration utilise la meme d marche que la d monstration ci dessus mais elle est beaucoup plus simple car elle se passe plat tous les contre mod les tant construits dans Ens Le Hauptsatz om Henn TEE On peut remarquer dans la d monstration du th or me de compl tude que la r gle de coupure n intervient jamais
23. que ce qu on a fait revient d crire 1a plus petite relation d quivalence contenant une relation donn e et compatible avec un certain uombre de fonctions Maintenant les axiomes pour l galit s crivent pcc s trO Ft t pour toute chaine d amp galit et tout V fini contenant les va riables libres qui apparaissent i i V A noter F tl i eG comme cas particulier xw E t t reali K t ti r t seses t DT TOE ses est pour tout symbole de relation r toutes chaines d galit E t sty et tout V TLK resp TL J muni de ces axiomes suppl mentaires sera not T LKE resp TL IE Quel est le mode d emploi de ces calculs s quentiels Quelques exemples de d monstration le feront comprendre Une d monstration de Vx rx Ay ry dans TLJ et donc dans TLK 15 ge Pe a axiome VX rx Vyxrx P al n EE axicne eeu fa rat bra Vx rx Muro Sie Bauc e NORRALE al 2 structure li rapVxrx Vx rx Q4Vx r xt coupure a ta 1WX r x i Ta structurale na Vxrx rar droite Yx r xhar a ue g A droite Va r x AyaQr y RA EE MG droite x I aVx r x Ayar y On sautera souvent l emploi d une r gle structurale dans une d monstration d Une d monstration de I pope daus T LK qui n en est pas une dans T LJ deg ro PT TC Ai droite pas valable dans TLJ e 3 EE OO OE EE 4 droite G F e BI
24. r alisation le sous lem me i comme pr c demment Le seul pas qui n cessite une nouvelle v rification est celui o est atomique et F 6 p ait p AU Si est r t psrsst et si pit cela veut dire qu il existe i n des cha nes d galit ECt t see ECE t avec IN 1 3 1 VK Y c E ESE TY Ep et Tr t itn t ED s V Mais puisque E t stus E t ERGER se ee tt ATR est un axiome si Fr tsere t p p n est a8 EE erant Si est t t et si pi o c est qu il existe une cha ne d galit E t t avec V V e fg t t TYE p Puisque E t t br tz TA est un axiome si Ft t ep p n est pas Vo consistant Dans les deux Cas F AE p p He Une fois le sous lemme i d montr on conclut comme pr cedemment Fin de la d monstration du iemme D monstration du lemme 2 b di d bs a C3 Li 4 y Pour plonger un consistant dans une collection de Hintikka on proc de en deux tapes D finition CI Li ger Un l ment de Hintikka est un couple p UD O p est un q 9 ensemble de formules sign es de et L 5 un ensemble de va riables libres contenant toutes les variables libres des formules mu de p tel que p est p consistant et que les conditions ACTI 4 94 SEG AB ECTS V D TES v0 BT 8 IO TS 9 120 Vx 6 x 13 F Vx x 16 TAX 6 x des collections de Hintikka sont v rifi es Sous lemme 2 Si si o est U consistant il existe un
25. r dans 3 e LE On ne consid rera qu un langage un seul type ce qui rend les choses plus faciles dire sans pour cela enlever quelque chose d essentiel D a bord quelques d finitions D finition HORE v Une formule sign e de 4 est une expression de la forme Y ou F2 O est une formule de T ou F sera la signature de la formule Soit S e Ta riseg 19 a EE FY i un ensemble fini de formules ni i sign es On pose ist TOTE ti FT ee iom I s n est d fini qu l ordre des suites de formules pr s mais cela importe peu gr3ce la r gle structurale P P re l PA x a i a CI Lr sm Soit F un ensemble fini ou infini de formules sign es LF un ensemble fini ou infini de variables iibres contenant toutes les variables libres des formules de E D finition Sest V U consistant si pour toute partie finie 8 de yY et toute mum partie finie V de p contenant les variables libres des formules EN 60S la de S iisi n est pas d montrable dans TLJ TLJE si L ect i avec galit Si ost V satisfaisable si pour toute partie finie S de oa toute partie finie V de EG en les variables libres des formules de ELEM n est pas valide Remarque Si dc VeU M fr est Leona MERHE ar i Pi GE j resp NONSE entraine est He ratont F 4 E 4 resp D satisfaisable Le fait que les calculs sont corrects s exprime par la
26. sus fonctionnent dans les cat gories d ductives Bi T H est d montrable dans T L JE il existe une d monstration de r Fe qui n utilise que les r gles pour A et V et ou toutes les s quences sont du bon genre Pt o est alors valide pour les cat gories d ductives D autre part puisque T LJE est complet pour les topos il l est pour les cat gories d ductives TLJE est un calcul correct et complet pour les cat gories d ductives i 2 3 4 REFERENCES G n ralit s sur les topos de Lawvere et Tierney expos s de J BENABOU et J CELEYRETTE au S minaire BENABOU 1970 71 Expos de M COSTE au S minaire BENABOU 1972 73 Intuitdonistic Logic Model Theory and Forcing M C FITTING North Holland The collected papers of Gerhard GENTZEN Investigations into logical deduction North Hoiland
27. t d montrabie dans T L J ou s K T LJE T Ya9 En l est aussi et d ne bd K serait pas trs H OS AE b c d e f 3 g m zx V x a k E vog Y 0 Vx V x y K 1 n On pose 4 iui Ey TY TO 1j Kr D i n n n n tdi U TY ou J U TO est ta consistant Si T V HAT et T 0 HA sont d montrables K TV v OF A l est aussi Si par exemple U TY est U consistant on pose f ijs U TY q9 Kel DK n n K 1 K Kel K 2 Sure VE sU di f U FO ou d U TY suivant le cas il Ur t n Soit a la premi re variable de la suite qui n est K pas dans DR Alors op U fTY a astu s U a n T L n 1 K k Vu a i K k avec veu consistant Si T Y a J k K K oet a Toc 5 oc A S Foe Y est d montrable jM Vx V x AY l est aussi On pose Sol ed U TY a VEL fa n n i n n i k k 4 U rv c t c VU est U consistant Si P Y t seses Y t F AY est d montrable T xY H 4 l est aussi On pose vi im wq Utrv ce IE c ev d 1y K i 17 5 n n contient Fe Yao K d i U FY ou of U FO suivant le cas UB ups n n or 3 K 1 QUK m a KK 2TK h amp Yv0 2 fi FY F0 U s U DO Ee os EDE a n n n n E qp Kl OX qrKEH TER D ds m3 53 rM B t UC P KEY K K K 29K k t Vx V x U FY t t e EU 1 i e UE D dssdo 1 t9 249 DEN nce i K n n Ti Et aai ed
28. ype i un ensemble d nombrable de variables qui seront employ es comme variables libres d sign es par les lettres du d but de l alphabet et un ensemble d nombrable de variables qui seront employ es comme variables li es d sign es par des lettres de la fin de l alphabet On sp cifiera le type d une variable par un OD exposant entre parenth ses ou x On supposera l ensemble des variables libres de tous les types totalement ordonn Un ensemble d nombrable de symboles de relations d sign es par r 5 chacun muni d une signature qui est une tuite finie de types i i T sera avec galit si on a pour chaque type i le symbole T qui est un symboie relationnel distingu de signature i i a Un ensemble d nombrable de symboles de fonction d sign s par f g chacun muni d une signature qui est un couple form d une suite peut etre vide de types et d un type i i Une cons tante de type i aura comme signature i Les termes de Pd sont form s l aide des r gies sulvantes Les variables libres et les constantes sont des termes Si une constante a pour signature i Son type est i 84 SETET sont des termes de types ied et si f est u Symbole de fonction de signature isa s j alors Elt se ses est un terme de type 1 On notera c t l ensemble des variables libres d un terme t et t t son type On pourra sp cifier ce type par un exposant entre parenth se
Download Pdf Manuals
Related Search