La logique classique

De
Publié par

Sequents classiques Dedou Janvier 2012

  • ordre des formules

  • formule active au bout

  • sequents classiques

  • jeu de regles

  • regle

  • regle structurelle d'affaiblissement

  • presentation correspondante


Publié le : dimanche 1 janvier 2012
Lecture(s) : 12
Source : math.unice.fr
Nombre de pages : 16
Voir plus Voir moins
S´equents
classiques
D´edou
Janvier
2012
Onrepart`aze´ro
Onavudo`usortentless´equents
etcequongagnea`lesvoirdunseul
Maintenantonde´roule la ´sentation correspondante. pre
cote. ˆ ´
Que prouve-t-on ?
Uns´equent,cestunesuiteniedeformulesclassiques dans un environnement d’atomes logiques et de variables objet.
Pourprouverunse´quent ondisposedunjeudere`glesditesdinfe´rence,quonvarevisiter.
La
r`eglestructurellede´change
Echange
` Γ , A , B , Δ ` Γ , B , A , Δ
Onpeutchangerlordredesformules.Cetter´eglepermetsurtout deformulerlesautresr`eglesenmettantlaformuleactiveaubout.
Exo Formaliserlare`glede´change.
La
regle structurelle d’affaiblissement `
Affaiblissement
` Γ ( W ) ` Γ , A
Onpeutoublierunehypothe`se.Cetter´eglepermetsurtoutde simplierlar`egledidentite´.
La
re`glestructurelledecontraction
Contraction
` A ( C )Γ , A , ` Γ , A
Onpeutdupliquerunehypoth`ese.Cettere`glepermetsurtoutde simplierlare`gledintroductionde . Lesre`glesWetCsontcellesqueLLrevisiteleplus.
Lare`glelogiquedeconjonction
Conjonction
( ) ` Γ , ` A Γ , A ` B Γ , B
Pourde´montrer A B ,onde´montre A etond´emontre B (dans le mˆemecontexte). Autrementdit:sisouscertaineshypoth`sonsaitd´emontrer A ese etonsaitde´montrer B alors,souslesmˆemeshypoth`eses,onsait d´emontrer A B .
Lar`eglelogiquedeconjonction:variante
Conjonction
0 ) ` Γ , A ` Δ , B ( ` Γ , Δ , A B
Sionsaitde´montrer A souscertaineshypothe`seset B sous dautres,alorsonsaitde´montrer A B avecleshypoth`esesquil faut pour prouver A et celles qu’il faut pour prouver B .
Exo Enquelsenslesdeuxre`glessont-elles´equivalentes?
Lesr`egleslogiquesdedisjonction
Disjonction
( g ) ` Γ ` , Γ A , A B ( d ) ` Γ , B ` Γ , A B
Pourd´emontrer A B ,onde´montre A ouonde´montre B (dans le mˆemecontexte).
Lesre`gleslogiquesdedisjonction:variante
Disjonction : variante
( 0 ) ` Γ , A , B ` Γ , A B
Pourd´emontrer A B ,onde´montre A en supposant B (ou linversecequirevientaumˆeme).
Exo Enquelsenslesdeuxre`glessont-elles´equivalentes?
Lesre`gleslogiquesdequantication
Quantification universelle
` Γ , A ( x ) ( ) ` Γ , x A ( x
` Γ , x A ( x )
La variable x n’app ˆıt s dans Γ. ara pa
Quantification existentielle
( ) `` Γ , Γ , xA ( At () x
` Γ , x A ( x )
La variable x n apparaıt pas dans Γ. ’ ˆ
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.