Home

Th`ese

1. 128 Conclusion Dans cette th se nous avons construit toute une s rie de syst mes formels propositionnels qui nous ont aid s mieux comprendre la nature et les pro pri t s m ta math matiques de la contrainte p dagogique Du calcul minimal au calculs d ordre sup rieur chaque petite alt ration montre quel point une lo gique est un difice fragile et le moindre d tail peut d truire des propri t s im portantes chaque tape nous avons tent de v rifier m ta math matiquement les attentes que nous avions face aux syst mes p dagogiques quitte exhiber des contre exemples quand elles n taient pas satisfaites Dans tous les cas nous avons tudi la non nullit des jugements des implications syntaxiquement et parfois s mantiquement nous avons galement jaug l expressivit des nouveaux syst mes par rapport aux anciens tout cela afin d obtenir des syst mes p dagogiques solides et expressifs Parmi tous les syst mes formels introduits les plus int ressants sont les sys t mes P CPM et P CP pour n 2 w ils m ritent pleinement d tre qualifi s de p dagogiques Ils admettent tous la non nullit des implications tout en restant aussi expressifs que les syst mes intuitionnistes usuels dont ils sont issus CPM et CP En cours d tude nous nous sommes rendus compte de l importance de certaines notions comme par exemple les motivations triviales en effet dans
2. l aide de la r gle Vi P AB analogue au cas P gt B Lemme 3 5 13 Soit n un l ment de 2 w Pour tout jugement d rivable T ho F gt le jugement T Hg F est d rivable avec y une variable fraiche pour FOUTFE D monstration Supposons que le jugement I Fi Fy soit d rivable donc le juge ment T F F est d rivable car P CP est un sous syst me de CCP le jugement Fe T F est d rivable par la r gle le jugement F Vy T F est d rivable par la r gle V le jugement H T F est d rivable par la r gle Ve d apr s le lemme 3 5 12 les jugements F T I1 et F F F sont d rivables ainsi le jugement H I F est d rivable l aide de la r gle Ext nous d rivons alors ais ment le jugement F F Nous pouvons alors grace aux lemmes 3 5 11 et 3 5 13 prouver la pr servation de la d rivabilit des jugements par y traduction Proposition 3 5 14 Soit n un l ment de 2 w Le jugement T F F est d ri vable si et seulement si le jugement T F5 Fy est d rivable avec y une variable fra che pour TU F D monstration D apr s les lemmes 3 5 11 et 3 5 13 La y traduction bien que tr s utile pour traduire les jugements ne permet pas de traduire les th or mes car il existe des formules F qui ne sont pas quivalentes leur y traduction F Prenons une variable a sa y traduction a y gt 7 puis suppos
3. 106 4 4 Normalisation lt imm diat par r currence sur la d rivation du jugement T Fip t Fa gt par r currence sur la d rivation de I H 4 F les cas et sont imm diats 9 N PL Se 1 4 TE Ax d apr s le lemme 4 3 1 nous pouvons d river Fip TT ainsi le jugement T Eis T est d rivable l aide de la r gle P Ax x Fer DA Zn 1 p Te F Hyp d apr s le lemme 4 3 1 nous pouvons d river Hp T ainsi le jugement TE F est d rivable l aide de la r gle P Hyp Notons que AC et P ACt typent exactement les m mes termes ils repr sentent non seulement la m me logique mais galement le m me langage de programma tion dont les programmes sont sp cifi s l identique 4 4 Normalisation En tant que programmes les A termes sont des processus ex cutables leur valuation consiste essentiellement instancier les param tres dans les abstractions par les termes qu ils repr sentent quand une application est de la forme Az t u on sait que la variable x repr sente le A terme u l valuation d une telle application produit alors le terme x u t Cette mani re d ex cuter les termes se nomme B r duction D finition 4 4 1 Pour tous les termes t et t la relation de G r duction entre t ett not e t g t est d finie par les r gles suivantes Perses Bo Fer Bxvar ea ze a A EURETAN Oet Bia Oxrea Ar4 u u
4. F est d rivable dans CCP la r gle du tiers exclu est d rivable plus pr cis ment le jugement FF y gt L gt Fy vy Fy F est d rivable 1 F y gt LHF par Hyp 2 F y LH F F d apr s la proposition 3 5 12 3 Fy LHF par Ext 1 et 2 dresser par Hyp 5 F y gt 1 1 H L par Hyp 6 F y gt L LES par Ve et 5 7T F y gt LF L gt y par gt i et 6 8 Fy 1Hy L par4et 7 9 F y gt LH F par Ext 3 et 8 10 F H y gt 1 F par gt i et 9 11 F y F ly T F d apr s le lemme 3 5 2 12 Fyyt2T par Ax 13 F y F y T par et 12 14 F y T Fey par Hyp 15 Fyy 2 T gt y par et 14 16 Fyy F y T par 13 et 15 17 F y FE F par Ext 11 et 16 18 FH y F par et 17 19 FH yo L gt F gt Q gt F gt F par la r gle du tiers exclu 20 F H y gt F gt F par gt e 19 et 10 21 FEOF par 20 et 18 22 FH F par Vi et 21 23 F F F par et 22 ainsi le jugement F F est d rivable le jugement F F F est alors d rivable 97 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur On en conclut que les calculs classiques d ordre sup rieur et les calculs p dago giques d ordre sup rieur partagent la m me expressivit via une traduction dont la pertinence par rapp
5. 8 B donc 6 d B 6 et B p ainsi Ya A y et V3 B y nous en d duisons que Va A a V3 B par la r gle avar A a par hypoth se de r currence nous avons a d A a 5 6 B et d apr s le lemme 2 2 8 nous avons a A a d A et G d B 8 5 B donc Ya A VB B par la r gle ay par d finition nous avons Ya A Ya A et VG B V6 B donc Ya A V3 B a_ par hypoth se de r currence nous avons A ay deux cas se pr sentent Le dernier lemme n cessaire la preuve par r currence concerne le cas des r gles P Ax et P Hyp en effet il nous faut garantir que la transformation substituant les occurrences de la formule L ne produit pas des formules non motivables partir de formules motivables Lemme 2 2 10 Pour toute formule F et pour toute variable y fraiche pour F si F est motivable dans F CP alors F est motivable dans F CP2 D monstration Supposons que le jugement amp F est d rivable Nous avons F y 1 F donc le jugement o 7 1 F est d rivable Ainsi Fy est motivable dans F CP par o y 1 28 2 2 Calcul propositionnel du second ordre faiblement p dagogique On montre enfin que le remplacement de L par une variable fraiche dans les for mules d une d rivation produit une d rivation valide Lemme 2 2 11 Pour tout jugement T H F d rivable le jugement T Fy est d ri
6. d rivons le jugement A B A B 1 AB AF A par Hyp 2 A B AF A At par hypoth se de r currence 3 A B t At At par gt e 1 et 2 4 A B Al A B par Hyp 5 A B t At B par gt e 3 et 4 6 A B At B B par hypoth se de r currence 7 A B AF B par gt e 5 et 6 8 A gt B tt AB par et 7 9 H A B t gt A B par gt et 8 F Va A d rivons le jugement H Va A Va A OO ND KR AED ow W 1 Va A 2 Va A Va A Va A Va A E Ya A Ore ren rw Va A rivons le jugement F 2Va A par Hyp A par V et 1 H2 A At 2 At Va At par hypoth se de r currence par gt e 2 et 3 par Vi et 4 Va A par gt i et 5 Va A Va A Va A par Hyp Va A 2 AT par V et 1 Va A Va A Va A NT NE RE SE Na NL F2 Va A 4 2 At A par hypoth se de r currence 2 A par gt e 2 et 3 2Va A par V et 4 Va A par et 5 Ainsi nous pouvons prouver la r ciproque du lemme 2 5 5 Lemme 2 5 7 Pour tout jugement T7 F FT d rivable le jugement T H F est d rivable avec y une variable fra che pour T U F 48 2 5 Traductions D monstration Le jugement I Pe FT est d rivable par hypoth se donc le ju gement 7 F7 est d rivable De 7 F
7. en substituant n importe quelle formule B la variable propositionnelle a on obtient un A terme de type B B Intuitivement pour toute formule a nous disposons d un processus construisant une preuve de a a ceci correspond une BHK interpr tation de la quantification universelle de la variable a appliqu e la formule a a c est dire la formule Va a a Au niveau des termes pour tout type a le terme Ax x est de type a a le processus d crit par la BHk interpr tation de la quantification universelle correspond l application d un A terme un type qui s value de la m me mani re d une r duction en notant Aa Ax x le terme de type Va a a on exprime la production d un A terme de type de la mani re suivante Aa Ar x A a A Az z On remarque que le symbole A joue un r le analogue au symbole En int grant cette construction aux A termes on obtient un A calcul typ par des formules pro positionnelles du second ordre ce syst me formel correspond via l isomorphisme de Curry Howard au calcul CP il a t introduit ind pendamment par Jean Yves 109 CHAPITRE 5 A calcul p dagogique du second ordre Girard et John Reynolds dans les ann es 1970 sous le nom de calcul polymorphe du second ordre Nous allons le pr senter dans cette section On commence par d finir les types D finition 5 1 1 Les types du second ordre que nous appelons types
8. est d rivable nous avons a VI T donc a VI T le jugement T Fp Vaf A est alors d rivable l aide de la r gle EEE T R Ext par hypoth se de r currence le juge T H a B F ment T Fp A B est d rivable d apr s le lemme 3 5 7 le jugement T Fy Ay B est d rivable par hypoth se de r currence le jugement Fy En a A F est d rivable d apr s le lemme 3 5 6 le jugement rT F5 a A F la A est d rivable nous d rivons alors le jugement T F a A F l aide de la r gle Ext ainsi le jugement T FP la B l F est d rivable l aide de la r gle Ext d apr s le lemme 3 5 6 le jugement T Hp a B F la B F est d rivable nous d rivons alors le jugement T Fg a B F l aide de la r gle Ext TESA A B reg a par hypoth se de r currence le jugement T F A est d rivable d apr s le lemme 3 5 8 nous avons A a B ainsi le jugement T F B est d rivable l aide de la r gle a THA A g B Te B par hypoth se de r currence le jugement T F A est d rivable d apr s le lemme 3 5 2 les formules A et B sont motivables dans P CP d apr s le lemme 3 5 10 le jugement T H A By est d rivable ainsi le jugement T B est d rivable l aide de la r gle Ext T H aA rA est d rivable nous avons 774A A gt 14 gt L et L Va a LLe par hy
9. la preuve de la proposition 3 2 8 Dans tout jugement p dagogiquement d rivable on s attend ce que les formules admettent une motivation qui associe le m me objet toutes les variables libres identiques apparaissant dans le jugement Le lemme suivant garantit que les mo tivations des hypoth ses sont galement des motivations des cons quences Lemme 3 4 4 Soit n un l ment de 2 w Pour tout jugement T Hp F d rivable et pour toute substitution o triviale dans P CP adapt e aux l ments de FU F si o est une motivation de IT dans P CP alors o est une motivation de F dans P CP D monstration La d monstration est analogue celle du lemme 3 2 5 Quelques pr cautions doivent tre prises lors de l utilisation de la r gle P V la place de la r gle Ve comme la substitution o est suppos e triviale dans P CP elle peut tre utilis e sans danger lors de l application de la r gle P V Pour tout pr dicat P P est la repr sentation de P sous la forme d une formule ainsi d montrer P et Q pour deux pr dicats P et Q garantit qu ils sont exten sionnellement gaux Lemme 3 4 5 Soit n un l ment de 2 w Soient T un contexte trivialement motivable k un genre et F K et G K deux pr dicats Si les jugements I Hg F et INE G sont d rivables alors le jugement T F5 F G est d rivable D monstration Par r currence sur kK K x les jugements I H F et IT Hg G s
10. On dit qu un L jugement I Fp F est d rivable quand il existe une d rivation dans P CPC dont la derni re r gle utilis e produit ce L jugement 13 CHAPITRE 1 Calculs propositionnels p dagogiques du premier ordre Nous allons d montrer que dans CPI et CPC les d rivations contiennent uni quement des formules c est dire des L formules ne contenant pas le symbole L On d montre d abord que pour toute formule o F F est une formule ce qui nous permettra de v rifier l absence de L dans les L formules motiv es dans les r gles P Ax et P Hyp Lemme 1 3 1 Pour toute L formule F et pour toute L substitution o si o F est une formule alors F est une formule D monstration Par r currence sur F F T T est une formule F l soit o une L substitution et supposons que g L soit une formule nous avons o L L donc L est une formule ce qui est absurde F a a est une formule F A B soit o une L substitution et supposons que o F soit une formule nous avons o F o A o B et par hypoth se de r currence A et B sont des formules donc A B est une formule Puis on d montre l absence de L dans les d rivations de CPI Lemme 1 3 2 Pour tout L jugement d rivable IT F F tous les l ments de l ensemble TU F sont des formules D monstration Par r currence sur la d rivation de F F Fior rha T formules donc d apr s le lemme 1 3 1 les l ments de l son
11. Vy Va y T a 8 et G B Va a gt a F Le jugement ne G G est d rivable D monstration re par P Ax Fe AB T T gt a par s et1 pe Y AS T Vart y T a par Vi et 2 oy gt a FE Va y T a par P Hyp et 3 a t q T a Hg y T T par P Ve 4 et 1 2 Va A T gt 4 T gt T par et 5 BAT TJ F par Vi et 6 F e F par P Hyp et 7 s F a par gt i et 8 ee VE F F par Vi et 9 re Va a a ais ment d rivable i G G par P V 10 et 11 N e SS Dow w UT LL T Sxe KH Fe TRE EN ee Oo NS SS ND wa Enfin nous d montrons que pour tout n 3 w le calcul PC CP admet au moins une implication syntaxiquement nulle Proposition 3 3 5 Il existe une formule G close telle que le jugement HS G gt G soit d rivable et que le jugement Fy G ne soit pas d rivable D monstration Soit G Vy 7 Va y T a 7 Va a a D apr s le lemme 3 3 4 le jugement FF G G est d rivable D apr s le lemme 3 3 3 le jugement F G n est pas d rivable 68 3 4 Calculs propositionnels p dagogiques d ordre sup rieur 3 4 Calculs propositionnels p dagogiques d or dre sup rieur 3 4 1 Pr sentation des calculs Nous avons construit dans le lemme 3 3 3 une formule G non d rivable dans PC CP telle que le jugement Pe G G soit d rivable Par cons quent aucun
12. a nous avons p a UY et Ua UYVy SiT H3 UY est d rivable alors DE UV est d rivable D apr s le lemme 2 5 2 le jugement y ce UY est d rivable donc si I aie UV est d rivable alors F Pe UT est d rivable B a nous avons 4 8 87 et 7 87 B7 F A B supposons que le jugement T Ee u A B soit d rivable La formule y A est motivable dans P CP d apr s le lemme 2 5 3 donc elle est HTM dapre la proposition 2 3 9 1 TA FS u A par P Hyp u A 2 o U A par hypoth se de r currence u A o H A B par hypoth se u A o H A y BY par d finition ue A H p B7 par gt 2 et 4 u A p u B par hypoth se de r currence 2 u A u B par gt i et 6 2 u A B par d finition i que le jugement T EA u A B soit d rivable Les for mules UT et A sont motivables dans P CP d apr s le lemme 2 5 3 donc elles sont HTM d apr s la proposition 2 3 9 Ainsi la formule u7 A7 est HTM d apr s 2 lemme 2 3 7 L TIILI ATH m A B par hypoth se pI AY FS mA gt u B par d finition uY AT ES U AT par P Hyp AT p u A par hypoth se de r currence HA p u B par gt e 2 et 4 AFH AS B7 par hypoth se de r currence ze L A pB par x et 6 2 u A gt B par d finition supposons que le jugement T ES u7 VB A soit d rivable 2 u Y8 A par hypo
13. et nous allons d montrer qu elle est d rivable dans F CP Dans ce but nous prouvons ci dessous une propri t des contextes motivables s par ment si I et A sont deux contexte motivables s par ment le contexte U A est motivable d s que leurs ensembles respectifs de variables libres sont disjoints dans ce cas on peut toujours d river I A F partir d une d rivation de I H F quand A ne partage aucune variable libre avec I et F 25 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre Lemme 2 2 6 Pour tout jugement T F d rivable et pour tout conterte A motivable dans F CP par une substitution u si VI T F N VI A 0 alors le jugement T A F est d rivable D monstration Par r currence sur la d rivation de IT F les seuls cas non imm diats tant ceux des r gles P Ax P Hyp et Vi H oT TT gements F ovim uva T et F aviary vya A sont d rivables et ainsi nous d rivons le jugement T A F par la r gle P Ax P Ax par hypoth se nous avons VI T N VI A donc les ju 2 as T a P Hyp ce cas est analogue P Ax f 2 2 a oan Vi par hypoth se de r currence le jugement T A A f est d rivable par hypoth se nous avons V1 A N VI A donc a VI T A ainsi on d rive le jugement T A Ya A par la r gle Vi On peut alors prouver la validit de la r gle F Aff dans F CP Proposition
14. p U pa P p la U P ainsi p motive a U P dans P CP A et B sont o UTM dans P CP par hypoth se de r currence a U A et a U B sont p UTM dans P CP ainsi a U P est p UTM dans P CP P V 6 A soit p une substitution triviale dans P CP telle que Dom p Dom o a U Dom y d apr s le lemme 3 4 11 P est p UTM dans P CP donc p motive P dans P CP d apr s le lemme 3 4 7 de m me p motive U dans P CP donc la substitution a p U est triviale dans P CP d apr s le lemme 3 4 6 le jugement F5 p a a p U P est d rivable nous avons a p U Aa P p a U P ainsi p motive a U P dans P CP soit U une formule d rivable dans P CP A est fo a U J UTM dans P CP par hypoth se de r currence a U A est p q a U UTM dans P CP ainsi a U P est p UTM dans P CP P Aa A analogue au cas P VG A P AB analogue au cas P A gt B Les deux lemmes suivants concernent le cas de la r gle Ext Lemme 3 4 14 Soit n l ment de 2 w Soit k un genre Pour tout pr dicat P KketQ K et pour toute substitution o triviale dans P CP si P Q est o UTM dans P CP alors P et Q sont o UTM dans P CP D monstration Par r currence sur kK k x supposons que la formule P amp Q soit o UTM dans P CP donc P et Q sont o UTM dans P CP k 1 0 supposons que la formule Va Pa Qa soit o UTM dans P C
15. soit p une substitution triviale dans P CP telle que Dom p Dom o U Dom u nous avons a Dom p donc le jugement F p a est d rivable ainsi P est p UTM dans P CP P A B soit p une substitution triviale dans P CP telle que Dom p Dom o U Dom y u motive o P dans P CP donc u motive P dans P CP nous avons Dom u o Dom o U Dom yu donc d apr s le lemme 3 4 6 p motive P dans P CP 75 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur o Aet o B sont u UTM dans P CP par hypoth se de r currence A et B sont p UTM dans P CP ainsi P est p UTM dans P CP P Va A soit p une substitution triviale dans P CP telle que Dom p Dom o U Dom y u motive o P dans P CP donc u motive P dans P CP nous avons Dom u o Dom o U Dom yu donc d apr s le lemme 3 4 6 p motive P dans P CP soit U une formule d rivable dans P CP o A est pa a U UTM dans P CP par hypoth se de r currence A est p a a U UTM dans P CP ainsi P est p UTM dans P CP P a A analogue au cas Va A P AB analogue au cas P A gt B Le lemme suivant concerne les cas des r gles faisant appel des substitutions comme les r gles Ext et P W Lemme 3 4 13 Soient n un l ment de 2 w k un genre et a une variable Soient P et U k deux pr dicats Pour toutes substitutions o et u triviales dans P C
16. A N Kolmogorov On the principle of the excluded middle russe Mathe maticheskij Sbornik Vol 32 1925 pp 646 667 Traduction anglaise dans 38 pp 414 437 V N Krivtsov A Negationless Interpretation of Intuitionistic Theories I Studia Logica 64 3 2000 pp 323 344 V N Krivtsov A Negationless Interpretation of Intuitionistic Theories II Studia Logica 65 2 2000 pp 155 179 V F Mezhlumbekova Deductive Capabilities of Negationless Intuitionistic Arithmetic Moscow University Mathematical Bulletin Vol 30 2 1975 V F Mezhlumbekova The system of negationless calculus of predicates with meaningfulness operator Transactions of NAS of Azerbaijan Vol 4 Num XXIII 2003 pp 109 112 G Mints Notes on Constructive Negation Synthese Vol 148 3 2006 pp 701 717 132 30 31 32 33 34 39 36 37 38 39 1 C R Murthy Extracting Constructive Content from Classical Proofs Ph D Thesis Cornell University 1990 D Nelson Non null Implication Journal of Symbolic Logic 31 1966 pp 562 572 D Nelson A Complete Negationless System Studia Logica 32 1973 pp 41 49 G D Plotkin Call by name call by value and the A calculus Theoretical Computer Science Vol 1 1975 pp 125 159 H Poincar Derni res pens es Flammarion Paris 1913 English transla tion in Last thoughts Dove
17. B par la r gle 8 ainsi nous d rivons le jugement H T B par la r gle a par hypoth se de r currence le jugement HPH T par hypoth se de r currence le jugement HPH T gt Gr ce au lemme pr c dent nous pouvons d montrer que pour n gt 2 tout th or me de CP est un th or me de F CP Proposition 3 2 10 Soit n un l ment de 2 w Pour toute formule F si le jugement H F est d rivable alors le jugement F est d rivable D monstration Imm diat par le lemme 3 2 9 Ainsi dans les calculs F CP pour n gt 3 le jugement Ff Va L a est d rivable la n gation est d finissable dans ces calculs F CP Le calcul F CP fait exception Quand n w nous avons donc un r sultat encore plus fort tout th or me de CP est un th or me de F CP 64 3 3 Calculs propositionnels p dagogiques contraints d ordre sup rieur 3 3 Calculs propositionnels p dagogiques con traints d ordre sup rieur 3 3 1 Pr sentation des calculs Malgr la non nullit syntaxique des jugements dans les calculs F CP la n gation y est d finissable d s que n est sup rieur ou gal 3 Pour obtenir un calcul dans lequel la n gation dispara t nous allons appliquer aux calculs CP la m thode de p dagogisation qui nous a permis de construire le calcul p dagogique P CP dans le chapitre pr c dent P CP est un calcul dans lequel toutes les f
18. FT est d rivable rH f A ag VIP NS 2 Ty DE Raf Va A vi 1 Fy h T T dapr s le lemme 5 5 2 2 H M T Va A d apr s le lemme 5 5 3 3 I7 k Va A Fip k Ya A par P Hyp 1 et 2 4 I7 k Ya A FX f A7 par hypoth se de r currence et P Aff 5 T7 k Va A Fy Aa f Va A par vi et 4 6 T7 k Va A Fy k Aa f y apr 8 et 5 7 T7 H3 AWA k Aa f Va A par gt i et 6 ainsi le jugement TT H Aa f Va A est d rivable TH f Va A eo ME NAAN TF2 fU UA Ve 1 Fy M TI TY d apr s le lemme 5 5 2 2 Fip M TI F7 d apr s le lemme 5 5 3 3 Fip D T Va A d apr s le lemme 5 5 4 4 T7 k F ES f Ya A par hypoth se de r currence et P Aff 5 7 k FT m Va AT ES m Va A7 par P Hyp 1 2 et 3 6 Fip D T U d apr s le lemme 5 5 4 7 IX k F m Va At on mU F par Ve 5 6 et le lemme 5 5 1 8 7 k F7 m Ya AT ae k F par P Hyp 1 2 et 3 OPN k F7 M Ya A Hip mu key par gt e 7 et 8 LORS A AA mU ee Vo APT parn etg 11 T7 k NES JAME TE MmU k y par 4 4 et 10 LES AR me mo 2B par Sp eh ll ainsi le jugement I H fU a U A est d rivable rH t G TESTER d rivable d apr s le lemme 5 5 5 nous avons G7 F7 ainsi nous d rivons le jugement T7 F3 t F avec la r gle a a par hypoth se de r currence le jugement TT Fip t G7 est
19. T par P Ax 2 6H T par P Ax et 1 He ee 4 H VB B T par Vi et 3 5 V3 8 a F Y B par P Hyp et 4 6 V3B at T a par Ve et 5 7 VBB at T par P Ax et 4 8 V8 8 gt aH a par gt e 6 et 7 9 F V8 8 par et 8 10 Va V3 8 a par Vi et 9 L objet indispensable pour un syst me p dagogique est la motivation que nous d finissons de suite D finition 2 2 2 Soit C un calcul dont la morphologie est constitu e par l en semble des jugements de la forme T H F Pour tout contexte A une motivation de A dans C est une substitution o telle que les jugements 2 oT soient d rivables Quand un contexte admet une motivation dans C on dit qu il est motivable dans C De plus une motivation d une formule F dans C est une motivation du singleton F dans C La premi re question qui vient l esprit concerne la nature des motivations sont elles compos es de formules closes ou non Intuitivement une substitution close correspond un exemple concret enti rement d termin comme par exemple un num ral en arithm tique 0 1 2 Au contraire une substitution ouverte repr sente un exemple g n rique n tant pas suffisamment contraint pour repr sen ter un objet unique dans le cas de l arithm tique un tel exemple pourrait corres pondre la donn e d un entier pair quelconque Il est l gitime de se demander si une formule motivable
20. Vy Ve A 7 y dans laquelle y est une variable fra che pour A R gle d introduction Dans le cas de F CP la r gle d introduction du quantificateur existentiel est d rivable C e U A ee Ex 2 REP si est valide dans F CP Proposition 2 4 9 La r gle D monstration Supposons que le jugement T e U A est d rivable l aide de la proposition 2 2 4 le contexte T U e U A A est motivable dans F CP 1 T e U A AF T par P Ax 2 T e U At AT par et 1 3 T e U A Ve A T par Vj et 2 4 T e U A Ye A y Ve A y par P Hyp et 3 5 T e U A Ve A y e U A par Ve et 4 6 T e U A Ve A y e U A_ par P Hyp et 3 7 T e U A Ve A y y par gt e 5 et 6 8 T e U A F Ve A y par et 7 9 T ae A H Vy Ve A y y par Vj et 8 10 TH U A Vy Ve A y par gt i et 9 11 TH aU A par hypoth se 12 T H Vy Ve A y y par 10 et 11 13 T Je A par d finition et 12 Il en est de m me dans le cas de P CP Proposition 2 4 10 La r gle w lA 3 est valide dans P CP H2 pea T 2 4e A D monstration Cette preuve est analogue celle de la proposition 2 4 9 Cepen dant la ligne 5 nous devons motiver dans P CP la formules U pour appliquer la r gle P V la place de la r gle Ye
21. a dans CP donc le jugement a L Lt a est d rivable ce qui est absurde Nous concluons par contradiction que le jugement F lt F n est pas d rivable Cependant on peut faire en sorte que les formules F et F soient toujours quivalentes f mais il faut alors se placer dans un calcul classique Proposition 2 5 13 Posons B T 7 V y gt L Pour toute formule F le jugement F Yy B FT est d rivable D monstration Deux cas sont consid rer lt 1 Yy B FY H Vy B FT par Hyp 2 VyB FP T 1 V L 1 F par et 1 3 Y B FT T 1 V L l ais ment d rivable 4 Vy B F7 F par 2 et 3 5 Vy B FH F par la proposition 2 5 6 et 4 6 H VWy B FY F par et 5 1 F BE T r V y gt 1 par Hyp 2 F B T gt yH y T F par le lemme 2 5 3 3 F B T yH FY cary et T sont suppos s quivalents 4 F B y LH F par Hyp 5 F B y Lt Ft par la proposition 2 5 6 and 4 6 F B y LH FY cary et T sont suppos s quivalents 7 F Bt F par Ve 1 3 et 6 8 Ft BF par gt et 7 9 Ft Vy B FT par Vj et 8 10 2F Vy B FT par et 9 Ce r sultat laisse penser qu il existe une traduction fid le entre CP et P CP Nous tudierons ce point dans la section 3 5 du chapitre 3 51 52 Chapitre 3 Calculs propositionnels p dagogiques d ordre
22. absence d ambiguit sont d finis par r currence comme suit la constante o est un terme les variables x y z sont des termes si x est une variable A un type ett un A terme alors x4 t est un terme sit etu sont des termes alors tu est un terme Afin d all ger l criture des A termes nous crivons tuv les termes de la forme tu v De m me nous crivons x tu les termes de la forme r4 tu Les d rivations dans les syst mes fonctionnels ont la m me structure que celle dans les syst mes formels comme nous utilisons la d duction naturelle la Gentzen Prawitz pour crire les d rivations nous avons besoin d une notion de contexte adapt e 102 4 1 calcul simplement typ D finition 4 1 3 Un contexte propositionnel du premier ordre est un ensemble fini de couples x A ou x est une variable et A un type tel que pour tout x A ET et pour tout y BET six y alors A B dans ce chapitre nous les appelons contextes quand aucune ambiguit n est craindre Un X jugement propositionnel du premier ordre est un triplet not T Fi t F avec T un contexte t un A terme F un type et id un identifiant textuel Dans ce chapitre les jugements propositionnels du premier ordre sont appel s jugements quand cela ne pr te pas confusion Le contexte vide est repr sent par le mot vide ainsi pour tout A terme t pour tout type F et
23. des calculs PC CP pour n 3 w ne v rifie la non nullit syntaxique des impli cations Cependant la formule G n est pas non plus d rivables dans CP donc la contrainte p dagogique n est pas trop restrictive ce n est pas cause d elle que G n est pas d rivable De plus le calcul PC CP quivalent P CP admet la non nullit syntaxique des implications En observant la preuve du lemme 3 3 3 on se rend compte que l impossibilit de d montrer la formule G est due au fait de ne pas pouvoir substituer des pr dicats quivalents dans les formules prouvables or il se trouve que PC CP admet cette propri t Nous allons donc enrichir les calculs PC CP afin que tous les pr dicats quivalents soient librement substituables dans les formules d montrables La notion de pr dicats quivalents n est correctement d finie que dans le cas des formules pour g n raliser cette notion nous d finissons l galit extensionnelle entre les pr dicats D finition 3 4 1 Soit k un genre Pour tous les pr dicats P k et Q k l galit extensionnelle entre P et Q not e P Q est une formule d finie par r currence sur kK k x A B est d finie par la formule gt B K t gt 0 A B est d finie par la formule Va Aa Ba Nous d finissons alors les calculs p dagogiques extensionnels d ordre sup rieur D finition 3 4 2 Pour tout n l ment de 2 w le calcul propositionnel p dago gique d
24. nos avons P Q VO 4 gt By gt By gt Ay gt 7 0 gt 1 1 TH VE A gt B gt By gt Ay gt gt 1 6 par hypoth se 2 FH y T 8 par le lemme 3 5 2 et la r gle P Aff 3 T E 4 gt By gt By gt Ay gt mA gt By gt Ay gt B par P Ve 1 et 2 4 TH 4 gt By A gt B par le lemme 3 5 5 5 r a A gt By gt B gt Ay gt A gt By gt 4 gt By par Ext 3 et 4 6 T H A gt B gt B gt Ay gt A gt B ais ment d rivable 7 TH Ay By par gt e 5 et 6 donc le jugement IT F5 A B est d rivable de m me le jugement T H By gt est d rivable ainsi le jugement HF a 6 nous avons alors une d rivation du jugement l E A By k gt 0 supposons que le jugement I H3 P Q soit d rivable soit a une variable fra che pour I U P Q nous avons alors une d rivation du jugement T Fi Vat Pa Qa ainsi le jugement T Hp Pa Qa est d rivable l aide de la r gle P Ve par hypoth se de r currence le jugement l H Pa o Qa est d rivable d apr s le lemme 3 5 5 le juge ment I H Py O P est d rivable ainsi nous avons une d rivation du jugement IT FY Py Aa 0 P 0 a le jugement T Hi Pya Aa 0 P O a a est d rivable l aide de la r gle P Ve le juge ment TF Aa 0 P O a a p P O a est ais ment d rivable nous d rivo
25. objet des deux lemmes suivants Lemme 3 5 1 Soit n un l ment de 2 w Pour tout pr dicat P de genre r et pour toute variable y fra che pour P si P est motivable dans P CP alors le pr dicat 9 P est motivable dans P CP par la substitution y T D monstration Par r currence sur kK k x Nous avons y T 0 P P T T donc il suffit de d river le jugement Hp P gt T gt T 1 Fp oP par hypoth se 2 PHE T par P Ax et 1 3 Fp P gt T par gt et 2 4 P THT par P Ax et 3 84 3 5 Traductions 5 Fp P gt T gt T par gt i et 4 k t gt 0 Le pr dicat P est motivable par hypoth se donc il existe une sub stitution o telle que le jugement F oVat Pa soit d rivable Ainsi le jugement a Vat o Pa est d rivable Par hypoth se de r currence le pr dicat a est motivable dans P CP donc le jugement H9 o PO a est d rivable par la r gle P V ainsi le pr dicat PO a est motivable dans P CP Par hypoth se de r currence le jugement H 7y T 0 P0 a est d rivable Nous d rivons le jugement H y T Va 6 P68 a par la r gle Vi Nous avons O P s Va 0 PO a ainsi le pr dicat O P est motivable dans P CP Lemme 3 5 2 Soit n un l ment de 2 w Pour tout pr dicat P et pour toute variable y fra che pour P le pr dicat P est motivable dans P CP par la substi tution y T D monstration Montrons par r cur
26. se de r currence H A T gt A gt Tr B par gt e 12 et 13 H FA par hypoth se de r currence H TB par gt e 14 et 15 Proposition 1 2 4 Pour toute formule F le jugement F F est d rivable si et seulement si le jugement F F est d rivable D monstration Imm diate l aide des lemmes 1 2 2 et 1 2 3 Bien que CPM et N CPM soient quivalents du point de vue des th or mes nous ne savons encore rien sur les jugements de N CPM quand leur contexte n est pas vide nous allons montrer qu il existe des jugements d rivables dans CPM qui ne sont pas d rivables dans N CPM On d finit deux ensembles de formules M et NF avec NW construit la mani re de l ensemble des formules vraies et M la mani re de l ensemble des formules fausses la seule diff rence consiste faire de la formule T un l ment de M D finition 1 2 4 Pour toute formule F les relations F N et F N sont d finies simultan ment par r currence sur F F T FE N t FEN F a FN eFEN F A gt B FEN siet seulement si ACN ou B E M et FEN si et seulement si A E N et BEN Lemme 1 2 5 Pour toute formule F F Ng si et seulement si F N D monstration Par r currence sur F F T nous avons T M et T ZN F a nous avons a M et a Z M 8 1 2 Calcul propositionnel p dagogique minimal F A B nous traitons les deux sens de l quivalenc
27. 2 2 7 Pour tout jugement T F d rivable et pour toute formule U telle que TU U soit motivable dans F CP le jugement T U F est d rivable D monstration Nous d rivons le jugement T F par la r gle D finissons la substitution u comme tant un renommage des variables contenues dans len semble VI T F telle que nous ayons une d rivation du jugement u T F dans laquelle aucune des variables contenues dans VI F U n apparaisse Posons Dom u a a et Bi ua pour tout i 1 n 1 T U F u T F d apr s le lemme 2 2 6 2 T U HF Ybi YBa T gt F par Vi et 1 3 T UH T F par et 2 4 T U T par P Hyp sachant que F U U est motivable dans F CP 5 T U F par 4 3 et 4 2 2 4 Va a ne d finit pas l absurde On sait gr ce la proposition 2 2 4 que certains jugements d rivables dans CP ne sont pas d rivables dans F CP par exemple le jugement Va a Va a car la formule Va a n est pas motivable Mais on ne sait pas encore si on peut prouver ou non tous les th or mes de CP dans F CP C est pourquoi nous allons exhiber un th or me de CP qui n est pas prouvable dans F CP Nous allons en 26 2 2 Calcul propositionnel du second ordre faiblement p dagogique fait d montrer un r sultat plus fort en caract risant dans F CP le comportement de la constante L d finie par la formule Va a Notation 2 2 1 La formule V
28. 4 5 le jugement I F5 1 o a p a est d rivable pour tout a Dom y Par hypoth se le jugement I F5 o F est d rivable donc le jugement TF wOo F est d rivable d apr s le lemme 3 4 2 Ainsi le jugement I F u F est d rivable par la r gle Ext Nous allons maintenant d montrer les propri t s attendues des motivations uni formes la premi re propri t est que toute motivation uniforme est une motiva tion Lemme 3 4 7 Soit n l ment de 2 w Pour tout pr dicat P et pour toute sub stitution o triviale dans P CP si P est o UTM dans P CP alors o motive P dans P CP D monstration Par r currence sur P nous traitons uniquement les cas P T et P a les autres cas tant imm diats d apr s la d finition 3 4 5 P T nous avons o T T donc o motive P dans P CP P a nous avons a Dom o et est triviale donc o motive P dans P CP La seconde propri t est que toute motivation uniforme d un pr dicat est une motivation uniforme de tous les sous pr dicats de ce pr dicat Lemme 3 4 8 Soient n un l ment de 2 w et o une substitution triviale dans P CP Pour tout pr dicat U et P tel que a VI P et que a U soit adapt e a P si a U P est o UTM dans P CP alors U est o UTM dans P CP D monstration Par r currence sur P P T ce cas est imm diat P deux cas se pr sentent B a nous avons a U P U co
29. 8 Pour tout contexte I et toute formule F le jugement DF F est d rivable si et seulement si le jugement TH F est d rivable D monstration Nous d montrons successivement les deux sens de l quivalence lt nous d montrons cette implication par r currence sur la d rivation de FH F tous les cas sont imm diats except pour les r gles Ax et Hyp Ax le jugement H I est d rivable d apr s le lemme 1 2 1 ee ainsi nous pouvons appliquer la r gle P Ax afin de d river le jugement Pkg T T FR F Hyp les jugements F Fr et F Fr sont d rivables d apr s le lemme 1 2 1 ainsi nous pouvons appliquer la r gle P Hyp afin de d river le jugement I F F F la d monstration de cette implication est imm diate par r currence sur la d rivation du jugement F F 1 3 propos de la n gation 1 3 1 Calculs propositionnels classiques et intuitionnistes Maintenant que l on dispose d une m thode produisant un calcul propositionnel p dagogique minimal satisfaisant nous allons l appliquer des calculs sur l impli cation et la n gation afin d observer le comportement de la contrainte p dagogique en pr sence de formules absurdes Nous enrichissons la notion de formule l aide du symbole d notant la formule absurde D finition 1 3 1 Les L formules propositionnelles du premier ordre abr g es en L formules sont d finies par r currence comme suit la cons
30. Aa est valide dans P CP TFA Proposition 2 4 4 La r gle D monstration Cette preuve est analogue celle de la proposition 2 4 3 Cepen dant aux lignes 2 et 7 nous devons motiver dans P CP les formules A et B pour appliquer la r gle P V la place de la r gle Ve mais A et B sont des formules motivables dans P CP d apr s la proposition 2 3 9 39 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre 2 4 2 Disjonction Nous allons prouver que les r gles d introductions et d limination de la dis jonction restent les m mes dans F CP Cependant m me si la r gle d limination usuelle de la disjonction est valide P CP ce n est pas le cas pour les r gles d in troductions D finition 2 4 2 La disjonction A V B des formules A et B est d finie par la formule Vy A y B y gt 7 dans laquelle y est une variable fra che pour et B R gles d introduction Dans le cas de F CP les r gles d introductions de la disjonction sont d ri vables on ne traite que le cas de la r gle d introduction gauche la r gle d intro duction droite tant analogues TH A oe Pr z k i 2 T AVE Va est valide dans F CP Proposition 2 4 5 La r gle D monstration Supposons que le jugement T H A soit d rivable l aide de la proposition 2 2 4 le contexte F U A est motivable dans F CP 1 T T par P Ax 2 T BH T par P Hy
31. B nous avons alors Va A V3 B par la r gle ay ainsi nous avons P a par hypoth se de r currence nous avons A a ay par hypoth se de r currence nous Qy a 5 A ee E L E TE A Bor AB AB Qapp analogue au cas a Pour montrer que la quivalence est stable par traduction nous avons besoin des deux lemmes suivants Lemme 3 5 9 Soient n un l ment de 2 w et T un ensemble motivable dans P CP Soient P k et Q k deux pr dicats motivables dans P CP Si P g Q alors le jugement I F P Q est d rivable D monstration Par r currence sur K 91 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur K x comme P et Q sont motivables le jugement I H P P est ais ment d rivable par hypoth se nous avons P Q donc le jugement I Hg P Q est d rivable l aide de la r gle p k 0 soit a une variable fra che pour IF U P Q par hypoth se nous avons P Q donc nous avons Pa g Qa par la r gle Bapp par hy poth se de r currence le jugement T F Pa 9 Qa est d rivable nous d rivons alors le jugement PF P Q l aide de la r gle Vi Lemme 3 5 10 Soient n un l ment de 2 w et T une ensemble motivable de formules Soient P k et Q k deux pr dicats Soit y une variable fra che pour T U P Q P Si P Q est d rivable alors le jugement T Hp Py x Qy est d r
32. C un calcul dont la morphologie est constitu e par l en semble des jugements de la forme T H t F Soit U t F une propri t portant sur t un A terme et F un type Pour tout terme t et tout type F on d finit la propri t H U t F par r currence sur F F T H U t F si et seulement si le jugement 2 t F est d rivable F a H U t F si et seulement si le jugement 2 t F est d rivable F A B H U t F si et seulement si il existe un terme u clos tel que le jugement 2 tu B soit d rivable et que H U tu B F Va A H U t F si et seulement si il existe un type U clos tel que le jugement 2 tU a U A soit d rivable et que U tU a U A Nous souhaitons faire appel au th or me de point fixe de Knaster Tarski il nous faut alors prouver que la propri t H U t F est croissante par rapport l argu ment Lemme 5 4 1 Soit C un calcul dont la morphologie est constitu par l ensemble des jugements de la forme T H t F Soient U t F et U t F deux propri t s portant sur t un terme et F un type Si pour tout A terme t et tout type F on a U t F implique U t F alors H U t F implique H U t F D monstration Par r currence sur F F T H U t F ne d pend pas de U donc le r sultat est imm diat F a analogue au cas pr c dent F A B supposons que H U t F par d finition il existe un terme u clos tel que le jugement H tu B soit d rivable et
33. CP et nous d rivons y A7 Fe BY avec la r gle P Aff Nous d rivons alors le jugement y H A B par application de la r gle F Va A par hypoth se de r currence le jugement y z A7 est d rivable Nous avons y a car y est une variable fraiche pour Va A ainsi nous d rivons le jugement y i Va A par application de la r gle Vj ND 2 7 Pp 27 3 4 5 Lemme 2 5 3 Pour toute formule F et pour toute variable y fra che pour F le jugement F y T F7 est d rivable D monstration Voici la d rivation du jugement Fe MATIE 1 y ae FY par le lemme 2 5 2 2 iy F7 par i et 1 3 F2 Vy y F par vi et 2 4 HT par P Ax 5 T gt h T F par P Ve 3 et 4 6 Es AAT FY par gt e 4 et 5 Pour que la y traduction soit compatible avec les r gles Ve et P V il faut qu elle commute avec l application des substitutions Lemme 2 5 4 Soient F et U deux formules I un contexte HTM et y une variable fraiche pour T U F U distincte de a Le jugement T H a U F est d rivable si et seulement si le jugement T F a U F est d rivable D monstration Notons u la substitution a U et u7 la substitution a U7 Nous allons prouver le lemme par r currence sur F 45 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre F T nous avons T T et uT T F 6 deux cas se pr sentent B
34. Curry Howard L identification des preuves et des programmes fonctionnels motiva la construc tion de syst mes dans lesquels les preuves sont repr sent s par des fonctions du A calcul et les formules sont des sp cifications des fonctions c est dire des des criptions du contenu informatique des fonctions ce qu elles calculent comment on peut les utiliser avec quelles donn es etc dans ce contexte les formules sont appel s types de tels syst mes sont dits fonctionnels Le plus simple des syst mes fonctionnels est sans doute le calcul simplement typ introduit par Church 4 la fin des ann es 1930 il correspond via l isomorphisme de Curry Howard au calcul propositionnel minimal d crit dans le chapitre 1 nous allons le pr senter dans cette section Nous commen ons par d finir les types des fonctions D finition 4 1 1 Les types simples que nous appelons types dans ce chapitre en l absence d ambiguit sont d finis par r currence comme suit la constante T est un type les variables 3 y sont des types si A et B sont des types alors B est un type Afin d all ger l criture des types nous crivons A B C les types de la forme A B C Puis nous d finissons les termes qui sont les fonctions du calcul correspondant aux preuves D finition 4 1 2 Les termes propositionnels du premier ordre que nous appe lons A termes dans ce chapitre en l
35. I n est pas forc ment motivable par exemple quand U Va a M me dans le cas o U est une formule motivable le nouveau contexte TU U ne l est pas forc ment par exemple quand T T gt qa et U a 1 comme l atteste le lemme suivant Lemme 2 2 5 Le jugement T a H a est d rivable et la formule a L est motivable dans F CP mais le jugement T a a L a west pas d rivable D monstration Voici la d rivation du jugement T gt a H a DET par P Ax 2 THT par P Ax et 1 3 Ff T T par i et 2 4 T a T a par P Hyp et 3 5 T gt at T par P Ax et 3 6 T at a par gt e 4 et 5 La formule a est motivable dans F CP car le jugement L L est d rivable Supposons que le jugement T a a L a soit d rivable Le contexte T a a L est motivable dans F CP d apr s la proposition 2 2 4 Soit a U une motivation de T a a 1 dans F CP les jugements H T U et U L sont d rivable donc le jugement T L est d rivable ce qui est absurde compte tenu de la consistance de F CP On peut d river des r gles d affaiblissements dans F CP mais elles doivent pren dre en compte la contrainte p dagogique comme toutes les r gles manipulant le contexte des jugements Nous proposons en remplacement de la r gle Aff la r gle d affaiblissement faiblement p dagogique F Aff CERF et TUF ma
36. T Ya A TF Va A i Tr F a U A We THA A B E TH B Zi On dit qu un jugement T H F est d rivable quand il existe une d rivation dans CP dont la derni re r gle utilis e produit ce jugement 2 2 Calcul propositionnel du second ordre faible ment p dagogique 2 2 1 Pr sentation du calcul L tude du calcul CPM dans le chapitre pr c dent nous a permis de d gager une m thode de p dagogisation remplacer les r gles Ax et Hyp par les r gles P Ax et P Hyp nous allons appliquer directement cette m thode au calcul CP D finition 2 2 1 Le calcul propositionnel du second ordre faiblement p dago gique abr g en F CP est d fini par sa morphologie constitu par l ensemble des jugements de la forme T H F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles gt i gt e Vi Ve et a ainsi que des deux r gles suivantes 7 H oT Fer e oT T A F P Hyp On dit qu un jugement T H F est d rivable quand il existe une d rivation dans F CP dont la derni re r gle utilis e produit ce jugement La contrainte p dagogique n est pas toujours facile utiliser quand on n y est pas habitu c est pourquoi nous proposons un exemple simple de d rivation dans F CP Exemple d rivation du jugement Va Y8 8 a a 21 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre 1
37. T A B A gt B gt yt 7_ par gt e 5 et 6 8 T ABH A B 7 7 par et 7 9 T A BH Vy A B 7 7 par Vj et 8 10 THA B Vy A B 7 7 par i et 9 11 TH A par hypoth se 12 THB Vy A B 7y 7 par 10 et 11 13 TH B par hypoth se 14 TH Yy A B gt 7 gt y par gt e 12 et 13 38 2 4 D finition des connecteurs logiques 15 T AAB par d finition et 14 Il en est de m me dans le cas de P CP THA THB Ai est valide dans P CP TH AAB Proposition 2 4 2 La r gle D monstration Cette preuve est analogue celle de la proposition 2 4 1 R gles d limination Dans le cas de F CP les r gles d liminations de la conjonction sont d rivables on ne traite que le cas de la r gle d limination gauche la r gle d limination droite tant analogue THF AAB 2 TRA Aa est valide dans F CP Proposition 2 4 3 La r gle D monstration Supposons que le jugement T H AA B soit d rivable l aide de la proposition 2 2 4 le contexte T U A A B est motivable dans F CP 1 T W A B 7 7 par hypoth se 2 TH 4A B A A par v et 1 3 TH T par P Ax 4 T a Bt a par P Hyp et 3 5 THa fB a par et 4 6 T F Va V3 a gt B a par Vj et 5 7 TH A B A par Ve et 6 8 T A par gt e 2 et 7 Il en est de m me dans le cas de P CP TH AAB
38. Une substitution est une application des formules dans les formules d termin e par un ensemble de variables propositionnelles not Dom o et par une application f des variables dans les formules Pour toute formule F l image de F par o not e o F est d finie par r currence sur F comme suit Fa N pt kT F a oF f a si a Dom o eto F a sinon F A gt B 0 F 0 A gt 0 B L ensemble Dom o est appel le domaine de la substitution o Pour tout contexte I pour toute substitution o et tout identifiant id l ensemble des jugements F 0 F tels que F T est not F oT La r gle Ax constitue une r gle sans pr misse mais elle n est pas en accord avec la conception intuitive des syst mes p dagogiques cause de la pr sence d un contexte arbitraire Nous avons besoin d une r gle sans pr misse en effet la r gle P Hyp poss dant des pr misses il nous faut une r gle Ax adapt e La r gle N Ax constitue un candidat potentiel ET N Ax Nous pouvons alors d finir une version p dagogique de CPM D finition 1 2 2 Le calcul propositionnel p dagogique minimal na f abr g en N CPM est d fini par sa morphologie constitu par l ensemble des jugements de la forme TE F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles et gt e ainsi que des deux r gles suivantes p r N Ax n CHAPITRE 1 Cal
39. apr s le lemme 5 5 2 2 Fip M TI F7 par le lemme 5 5 3 3 IT k FY at k F par P Hyp 1 et 2 AT k FY att x F7 par P Hyp 1 et 2 DR RENE Paks par gt e 3 et 4 6 7H AK ak FY par u et 5 ainsi le jugement 7 4 x F7 est d rivable SAS f tp FB 4 1 R MATIN A d apr s le lemme 5 5 2 2 Fip M TI 4 B d apr s le lemme 5 5 3 3 I7 k A gt B H k 4 B par P Hyp 1 et 2 4 I k A gt B zr Fip f B par hypoth se de r currence et P Aff 5 RNA DIT i At f A B par et4 GER A ENT RS kg po par e et 5 7 T7 H3 ARGENT AGE f A B par gt i et 6 ainsi le jugement 7 F Ax4 f FT est d rivable Se di oe Pegg A S T Fip fg r rip Y T P7 d apr s le lemme 5 5 2 in DAT F d apr s le lemme 5 5 3 ip LY T A7 F7 d apr s le lemme 5 5 4 k F Fy f A F par hypoth se de r currence et P Aff k F7 m AT F7 Fip m A7 F par P Hyp 1 2 et 3 Yk Fm AY F7 Fe g AT par hypoth se de r currence et fE Yk FY m A gt F EE mar par gt e 5 et 6 Yk FI m gt F7 He k F par P Hyp 1 2 et 3 127 CHAPITRE 5 A calcul p dagogique du second ordre EVENT mt AP PUES Mmgk y par gt e 7 et 8 WT kP ome mgk A FPT par jet 9 11 I7 k F H am F mgk y par 4 et 10 12 PES ARP f Am gt P mgk F par 3 et 11 ainsi le jugement 7 4 fg
40. constitu e par l ensemble des d rivations d finies par r currence l aide des r gles suivantes Tear z Fer Tr r Ep Pee Ak ee THt 4 B THu A 2 44 i 2 gt e T F5 rt A B Fy tu B TH t A ag VIT vi TH t Va A Ve T H Aa t Va A i T H tU a U A THA A B os Ekitap T On dit qu un jugement T H t F est d rivable quand il existe une d rivation dans AC dont la derni re r gle utilis e produit ce jugement 5 2 calcul p dagogique du second ordre Pour p dagogiser AC il faut prendre soin que le A calcul obtenu ait de bonnes propri t s Deux m thodes de p dagogisation ont t utilis es dans le chapitre 2 pour p dagogiser le calcul CP la premi re a engendr le calcul F CP mais ce calcul n admet pas la propri t de normalisation des preuves Voici la preuve du th or me F Va a Va a 1 H T par P Ax 2 at a_ par P Hyp et 1 3 Fa a par 4 et 2 4 F Va a gt a par Vj et 3 5 F Va a Va a par Ve et 4 Cette preuve correspond au terme Aa Axr x Va a dont la G r duction pro duit le terme r x mais ce terme en forme normale ne correspond aucune d rivation de F CP en effet la d rivation candidate est celle ci 1 Va a H Va a application de P Hyp incorrecte 2 F Va a Va a par et 1 La ligne 1 de cette preuve demande ce que la formule Va a soit motiv e mais ceci impli
41. construction d passe le cadre de cette these et donc nous n en parlerons pas Comme dans le cas du second ordre on peut plonger le calcul usuel dans le calcul XXIV p dagogique l aide d une traduction des formules on montre que ce plongement op re m me dans le cas d un calcul classique XXV XXV1 Premiere partie Systemes formels p dagogiques Chapitre 1 Calculs propositionnels p dagogiques du premier ordre 1 1 Rappels sur le calcul propositionnel minimal Le calcul propositionnel minimal est sans doute l un des plus simples syst mes formels connus Il d crit le comportement d un seul connecteur logique l implica tion op rant sur des propositions logiques Cependant il est suffisamment puissant pour simuler le comportement d autres connecteurs logiques tels que la conjonc tion la disjonction et la n gation En effet certaines traductions comme celle que nous pr senterons au chapitre 3 permettent de plonger le calcul propositionnel classique dans le calcul propositionnel minimal Nous d finissons tout d abord les formules du calcul D finition 1 1 1 Les formules propositionnelles du premier ordre que nous ap pelons formules dans ce chapitre en l absence d ambiguit sont d finies par r cur rence comme suit la constante propositionnelle T la formule vraie est une formule les variables propositionnelles a 3 y sont des formules si et B sont des formu
42. contrainte p dagogique montre son utilit dans la construction de calculs sans n gation Mais le symbole L repr sentant l absurdit est un l ment ad hoc le retirer des L formules ne pose aucun probl me il n en est pas de m me dans les calculs o l absurdit est d finissables par exemple le calcul propositionnel intuitionniste du second ordre est un calcul ind cidable dans lequel l absurdit est d finissable l limination de l absurdit y est un probl me impossible r soudre algorithmiquement La contrainte p dagogique est un moyen d ajouter suffisamment d informations dans les preuves afin de r soudre ce probl me L tude de ce calcul dans le chapitre sui vant va nous permettre d prouver la contrainte p dagogique et en plus de d duire les r gles p dagogiques r gissant la conjonction la disjonction et l existence car ces trois op rateurs logiques sont d finissables au second ordre 16 Chapitre 2 Calculs propositionnels p dagogiques du second ordre 2 1 Rappels sur le calcul propositionnel du se cond ordre Le calcul propositionnel intuitionniste du second ordre porte sur l implication et le quantification universelle des variables propositionnelles Son apparente simpli cit cache une grande expressivit on peut y d finir la conjonction la disjonction le quantificateur existentiel et la n gation c est un calcul ind cidable donc tr s complexe Nous allons tenter de
43. dans ce chapitre en l absence d ambiguit sont d finis par r currence comme suit la constante T est un type les variables 3 y sont des types si A et B sont des types alors A B est un type sia est une variable et A un type alors Va A est un type Afin d all ger l criture des types nous crivons A B C les types de la forme A B C De m me nous crivons Va A B les types de la forme Va A gt B Puis on distingue les variables libres des variables quantifi es D finition 5 1 2 Pour tout type F l ensemble VI F des variables libres de F est un ensemble de variables d fini par r currence sur F Fe TINTIN F a VI F a F A B VI F VIA UVI B F Va A VI F VI A a Par extension pour tout conterte T nous notons VI T l ensemble U ger VG Quand VI F 9 nous disons que le type F est clos D finition 5 1 3 Pour tout type F l ensemble Vq F des variables quantifi es de F est un ensemble de variables d fini par r currence sur F P Vq F Pa Vqaq F F A gt B Vqa F Vq A U Va B F Va A Vq F a U Vq A D finition 5 1 4 Une variable fra che pour un type F est une variable a telle que a VI F UVq F Par extension une variable fra che pour un contexte T est une variable fra che pour chacun des types apparaissant dans T L ensemble des variables fra ches d un contexte T est not
44. dans les pr dicats leur nom n a aucune importance sinon pour les distinguer des autres variables et nous consid rons que deux pr dicats ne diff rant que par le nom de leurs variables quantifi es ont la m me signification on dit alors qu ils sont a quivalents D finition 3 1 13 Pour tous les pr dicats P et Q la relation d a quivalence entre P et Q not e P Q est d finie par les r gles suivantes er 00 oF ave A Sg A B Sap A gt B Aa 00 la y A a 6 7 B y F A B Va A VB B av la y A a B 1 B y Fr A B ad ra A AB B A A B B AB AB sve Quand la relation P Q est v rifi e on dit que les pr dicats P et Q sont a quivalentes Les pr dicats sont d finis comme des fonctions op rant sur d autres pr dicats leur valuation produit des pr dicats syntaxiquement diff rents mais ayant la m me signification on dit alors qu ils sont quivalents D finition 3 1 14 Pour tous les pr dicats P et Q la relation de B quivalence entre P et Q not e P Q est d finie par les r gles suivantes Ten Gr Brvar a p a 57 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur A A B B A B A B 8 A A Vaf A Var A 9 A A Aa A p a A 9a A A B B Bao AB A B i A B y Psym Ba Pam A B B C vr 5 C Birans Aa
45. dans les syst mes p dagogiques sont propos s afin de mesurer l expressivit des syst mes contraints vill Dans un second temps nous proposons une s mantique des syst mes p dago giques sous la forme de systemes fonctionnels c est a dire de A calculs Usuel lement a chaque syst me formel correspond un syst me fonctionnel au calcul propositionnel minimal est associ le A calcul simplement typ et au calcul propo sitionnel du second ordre est associ le A calcul polymorphe du second ordre Dans chaque cas nous tudions la stabilit par G r duction et la normalisation dans les systemes p dagogiquement contraints Nous introduisons la notion de A termes utiles comme le pendant fonctionnel de l absence de n gation en logique Les tra ductions entre les syst mes logiques usuels et p dagogiques se muent au niveau fonctionnel en traductions CPS ix Pr sentation synth tique Historique Depuis l apparition des premi res notions de d monstration dans la Gr ce An tique jusqu au dix neuvi me si cle le cadre formel du d veloppement des math matiques tait assez flou personne ne savait pr cis ment formellement ce qu tait une preuve ou un th or me on en avait une vague id e mais sans plus Au dix neuvi me si cle les math maticiens se sentent de plus en plus concern s par cette absence de fondations rigoureuses le raisonnement math matique devient peu peu un objet math matique part
46. de o F donc o G est HTM il existe une substitution triviale p telle que kz p o G soit d rivable D apr s le lemme 2 3 5 le jugement a TiDom p o G est d rivable D apr s la proposition 2 3 2 le jugement Be T o G est d rivable Nous d montrons de mani re analogue que le jugement 2 T o a est d rivable pour toute variable a Dom o Ainsi la substitution 7 a est triviale D apr s le lemme 2 3 5 le jugement Le T G est d rivable donc G est TM Le lemme suivant servira traiter le cas de la r gle P V 34 2 3 Calcul propositionnel p dagogique du second ordre Lemme 2 3 7 Pour toutes formules U et F HTM dans P CP et pour toute variable a telles que la substitution a U soit adapt e a F la formule a U F est HTM dans P CP D monstration Soit H une sous formule de a U F Deux cas se pr sentent H est une sous formule de U la formule U est HTM donc H est TM il existe une sous formule G de F telle que H a U G la formule U est HTM donc il existe une substitution triviale p telle que le jugement ES p U soit d rivable D apr s le lemme 2 3 5 le jugement H2 T Dom p U est d rivable D apr s la proposition 2 3 2 le jugement Fe Ur est d rivable De m me le jugement es GT est d rivable Posons u a UT uitc ar La substitution u de domaine V1 G est triviale donc d apr s le lemme 2 3 5 le jugement u G est d rivable Nous avons u G
47. dit qu un jugement I F F est d rivable quand il existe une d riva tion dans CCP dont la derni re r gle utilis e produit ce jugement Pour toute formule F et pour toute variable y la formule F y est not e F et la formule F est not e 1 F Dans les traductions n gatives la double n gation ici remplac e par la double pseudo n gation F joue un r le pri mordial nous avons besoin de la g n raliser pour pouvoir lui donner un sens dans le cadre des pr dicats d ordre sup rieur ainsi l quivalent de la double n gation d un pr dicat P est repr sent par une double pseudo n gation g n ralis e O P D finition 3 5 2 Pour tout pr dicat P de genre k et pour toute variable y fraiche pour P le pr dicat P est d fini par r currence sur k Hero Pl enr k gt 90 O P a 0 PO a Nous d finissons maintenant notre traduction de CCP dans P CP la y traduc tion d ordre sup rieur D finition 3 5 3 Pour tout pr dicat P et pour toute variable y fra che pour P le pr dicat P est d fini par r currence sur P PRES P a P 0 P P A gt B P 4 gt B P Ya A P Va Az P NOP AS Py a Az P AB P A amp B Pour que la y traduction fonctionne bien il faut qu elle poss de de bonnes pro pri t s il faut tout d abord qu elle transforme tout pr dicat en un pr dicat moti vable la preuve de ceci est l
48. du pr sent m moire il voque l id e que la syntaxe i e la notion de programme preuve puisse subsumer la morphologie i e la notion de type formule afin que les types mergent de l objet qui leur donne une signification menant ainsi un calcul sans absurdit L id e de base tait d ajouter une contrainte la g n ration des formules si le terme t est de type A alors A est un type mais elle ne fonctionne pas car elle contraint tous les types tre habit s Bien que le concept ne fut pas clairement d fini il me fut pr sent par son auteur sous le nom de syst me formel p dagogique Seule la composante logique du calcul tait maintenant prise en compte L id e avait volu elle consistait alors remplacer la r gle Hyp dans le calcul des s quents intuitionnistes Fer TFF DP par la r gle p dagogique P Hyp Fer For dans laquelle est une substitution des variables libres des formules du contexte I Le terme p dagogique fut choisi cause de l analogie entre l utilisation d exemples dans la pratique de l enseignement et la motivation des formules l aide de substitutions les rendant prouvables Avec cette seule alt ration du syst me au cun jugement ne peut tre d riv puisqu il n existe plus aucune r gle sans pr misse La solution propos e tait d ajouter au syst me la r gle N Ax FT N Ax dans laquelle la constante propositionnelle T d note la for
49. en est galement d pourvue la fonction d crite par A est parfaitement inutile car elle ne peut tre appliqu e aucun programme un programme utilisant une telle fonction en est r duit la passer de fonctions en fonctions sans jamais l appliquer quoi que ce soit telle qu il agirait face un objet neutre sans aucun contenu algorithmique M me si une formule peut avoir un sens dans la s mantique fonctionnelle certaines de ses sous formules n en ont pas forc ment dans le sens o elles sont d nu es de repr sentation fonctionnelle de plus il n existe aucun moyen de donner un sens aux formules ind cidables si tant est qu elle en ont un xvi De m me que le principe du tiers exclu est rejet par les constructivistes en raison de ses cons quences ontologiques quelques logiciens rejettent les formules n admettant aucune repr sentation fonctionnelle apte leur donner un sens En effet la raison d tre d une s mantique est de donner un sens aux formules il est clair qu une s mantique autorisant l occurrence de formules n ayant pas de sens choue dans sa mission On pourrait objecter le fait que de telles formules l instar de L d notant l absurde ont pour sens de ne pas avoir de sens mais l expression de cette absence de sens au niveau du m ta syst me n cessite de donner un sens la n gation donc de garantir que l absurdit au niveau du m ta syst me est galement d nu
50. enti re la logique math matique se d gage comme une discipline formelle au m me titre que l arithm tique ou la g om trie Les premiers syst mes formels destin s fonder les math matiques comme la th orie na ve des ensembles se r v lent incoh rents tout un bestiaire de paradoxes entache les modes de raisonnements que l on croyait valides il s ensuit alors au d but du vingti me si cle ce qu on appelle aujourd hui la crise des fondements il devenait urgent de donner aux math matiques des fondements corrects complets et surtout coh rents Parmi les math maticiens ayant particip aux r flexions sur les raisonnements s rs on compte en particulier Henri Poincar qui nous a l gu quelques ouvrages sur le sujet dans derni res pens es 34 on peut lire un passage qui ne semble justifi par aucune de ses r flexions ni par celles des autres math maticiens de son poque comme si elle relevait du simple bon sens La d finition par postulat n a de valeur que quand on a d montr l existence de l objet d fini dans le langage math matique cela veut dire que le postulat n implique pas contradiction on n a pas le droit de n gliger cette condition il faut bien admettre l absence de contra diction comme une v rit intuitive comme un axiome par une sorte d acte de foi mais alors il faut se rendre compte de ce qu on fait et savoir qu on allong la liste des axiomes ind
51. est ais ment d rivable nous avons w A BY T T A B ainsi nous avons une d rivation du jugement DFS ASR F Va A par hypoth se de r currence le jugement I Fip AT est d rivable nous d rivons alors le jugement T TA Va u A7 avec la r gle V nous avons y a donc nous avons Va u AT wVa A ainsi nous avons une d rivation de T Fip Va A7 le jugement T Hip u Ya AY T T est ais ment d rivable nous avons w Ya A T gt T Ya A donc nous avons une d rivation du jugement P F3 w Ya A 125 CHAPITRE 5 calcul p dagogique du second ordre Pour des raisons techniques pour tout type F il faut galement pouvoir motiver les types F et F75 Lemme 5 5 3 Notons u la substitution y T Soient F un type et un contexte motivable dans P C Pour toute variable fra che pour T U F le jugement Dy uF est d rivable D monstration Analogue la preuve du lemme pr c dent Lemme 5 5 4 Pour tout type F et pour toute variable y fraiche pour F le type F est motivable dans P AC D monstration Par cas sur F quand F T ou F a le type FT est ais ment motivable et les autres cas sont la cons quence des lemmes 5 5 2 et 5 2 1 La y traduction ne doit pas alt rer le sens des formules relatif aux variables quan tifi es donc notre traduction doit rester stable par rapport aux renommage des variab
52. formule Va A soit o UTM dans a e fs P CP Soit U une formule d rivable dans P CP La formule A est o a U UTM dans P CP Par hypoth se de r currence la formule A est o a a U UTM dans P CP Le jugement 7 o Va A est ais ment d rivable par la r gle g Ainsi la formule Va A est o UTM dans P CP L autre sens de l implication est analogue A g A NRA a Al Gy analogue au cas pr c dent 5 E A g A B g B AB AB Gapp supposons que le pr dicat AB soit o UTM dans e P CP Les pr dicats A et B sont o UTM dans P CP Par hypoth se de r currence les pr dicats A et B sont o UTM dans P CP Le jugement F5 o A B est ais ment d rivable par la r gle g Ainsi le pr dicat A B est o UTM dans P CP L autre sens de l implication est analogue A g B B g A hypoth se de r currence le pr dicat B est o UTM dans P CP L autre sens de l implication est analogue A g B B gC Gsym Supposons que le pr dicat A soit o UTM dans P CP Par A a Girans Supposons que le pr dicat A soit o UTM dans P CP Par hypoth se de r currence le pr dicat B est o UTM dans P CP donc par hypoth se de r currence le pr dicat C est o UTM dans P CP L autre sens de l implication est analogue Hu Vaf A Hu B Qa AJB p ap A PP supposons que le pr dicat Aa A B soit o UTM dans P CP Pour toute formule U d riv
53. interne rien sur son contenu algorithmique rien sur ses arguments son existence ou plut t sa non existence est postul e de mani re purement discursive sans jamais tre justifi e par un objet s mantique Puisque les formules absurdes de m me que les formules ind cidables ne semblent pouvoir tre associ un programme une solution possible consiste restreindre la notion de formules qu on appelle la morphologie de mani re ce que les formules sans repr sentation fonctionnelle en soient exclues Pour construire cette morpho logie il faut faire appel aux r gles du syst me formel la syntaxe du syst me afin de garantir par certaines d monstrations que les formules sont associ es cer tains programmes mais la construction de la syntaxe pr suppose habituellement la donn e d une morphologie on est alors contraint d introduire une syntaxe de laquelle on peut d river la morphologie la syntaxe doit subsumer la morphologie 5 De cette mani re aucune formule d nu e de sens ne peut appara tre dans une d monstration et on obtient la propri t recherch e toute formule a un sens donn xvii Pr sentation synth tique par le programme dont elle d crit les propri t s Bien str la n gation disparait totalement de toutes les formules c est pourquoi de tels syst mes formels sont dits sans n gation ou positifs Il n est pas n cessaire de s engager dans des r flexions philosophiques p
54. jugement d rivable T ee t F le jugement Tja Ut5 t F est d rivable D monstration Par r currence sur la d rivation de I Fip t F on ne traite que les cas P Ax et P Hyp les autres cas tant imm diats par r currence be oT FT P Ax d apr s la proposition 5 2 1 les jugements Fip TT sont d rivables ainsi nous d rivons le jugement I x U se o T l aide de la r gle P Ax y Fer HoT i y F ae I sont d rivables ainsi nous d rivons le jugement I x U at y F l aide de la r gle P Hyp P Hyp d apr s la proposition 5 2 1 les jugements Nous pouvons alors d montrer que l application de la r gle Ared pr serve le typage des termes r duits Lemme 5 3 2 Pour tout jugement d rivable TK Ac4 t u F le jugement TH a u t F est d rivable D monstration Par hypoth se les jugements I x A ae t FetT Fip u A sont d rivable nous allons prouver par r currence sur la d rivation de T x A ae t F que le jugement PF x u t F est d rivable kipo Tr A F x A Fip o T T H v u o T l aide de la r gle P Ax y FelT s A poa T z A HER t i F y F x A par hypoth se le jugement T an u A est d rivable de plus u a u y donc le jugement T ase x u y F est d rivable P Ax nous avons xz u o o donc nous d rivons P Hyp il y a deux cas a traiter 117 CHAPITRE 5 A calcul p dagogique du second ordr
55. la preuve du lemme 2 2 2 Nous avons galement la propri t que les motivations se propagent par d rivabilit des hypoth ses aux conclusions Lemme 3 2 5 Soit n un l ment de 2 w Pour tout jugement T F F d rivable et pour toute substitution o adapt e T si les jugements FF o T sont d rivables alors le jugement o F est d rivable D monstration Analogue la preuve du lemme 2 2 8 Ainsi dans tout jugement d rivable le contexte et la conclusion sont motivables par la m me motivation ceci signifie que toutes les variables libres sont repr sen tables par le m me exemple dans toutes les formules d un jugement Proposition 3 2 6 Soit n un l ment de 2 w Pour tout jugement T FP F d rivable l ensemble T U F est motivable dans F CP En particulier TE F est syntaxiquement non nul D monstration D apr s le lemme 3 2 4 le contexte I est motivable dans F CP et donc d apr s le lemme 3 2 5 la formule F est motivable dans F CP 3 2 3 La r gle d affaiblissement La r gle d affaiblissement usuelle PE Toe Ai n est plus d rivable dans les calculs F CP car la formule U introduite dans le contexte n est pas forc ment motivable Lemme 3 2 7 Soit n un l ment de 2 w Le jugement T at a est d rivable et la formule a L est motivable dans F CP mais le jugement T a a gt Va a FF a n est pas d rivable D mo
56. le cadre des syst mes fonctionnels issus de l isomorphisme de Curry Howard On obtient alors un calcul p dagogique simplement typ partir du calcul simplement typ Apr s avoir construit un syst me formel p dagogique viable la seconde tape fut d observer son comportement en pr sence de la n gation Pour cela on ajoute au calcul p dagogique minimal les r gles r gissant la constante propositionnelle L d notant l absurdit Dans le premier cas on ajoute la r gle Li IE TFF M afin d obtenir la version p dagogique du calcul propositionnel intuitionniste sur l implication et la n gation Dans le second cas on d finit la n gation F d une formule F par la formule F L puis on ajoute la r gle Le TAF FL eS eh FHF Le afin d obtenir la version p dagogique du calcul propositionnel classique Dans les deux cas le calcul p dagogique obtenu se r v le quivalent au calcul p dagogique minimal car la contrainte p dagogique interdit toute occurrence du symbole L dans les formules Par l isomorphisme de Curry Howard il est alors possible de XXI Pr sentation synth tique donner un sens informatique la disparition de l absurdit puisque tous les types sont motivables pour tous les A termes t de type A B clos il existe toujours un A terme u de type A pouvant tre pass en param tre t on dit alors que tous les termes typables sont utiles car leur contenu algor
57. le cas des formules d rivables la traduction de F en F pr serve l quivalence des formules Proposition 2 5 11 Pour toute formule F si l un des deux jugements H F et L F est d rivable alors le jugement H F F est d rivable D monstration Deux cas se pr sentent supposons que le jugement F soit d rivable Le jugement ee F est d rivable d apr s la proposition 2 5 10 Le jugement F F est alors ais ment d rivable de m me que le jugement F F Nous d rivons ainsi les jugements F F et F F avec la r gle supposons que le jugement a F soit d rivable Le jugement H F est d rivable d apr s la proposition 2 5 10 Nous concluons alors comme dans le cas pr c dent Malheureusement l quivalence des formules n est pas pr serv pour toutes les formules c est le cas de la formule a 3 6 Proposition 2 5 12 Il existe une formule F telle que le jugement F F ne soit pas d rivable 90 2 5 Traductions D monstration Posons F a 3 8 et supposons que le jugement H F F soit d rivable Dons H F F est d rivable Ainsi le jugement a 3 BY aV y BV BV y est d rivable En substituant y par a et B par L nous obtenons une d rivation du jugement a L LH a V a gt LV a 1 Va La formule a V a L V a est d rivable dans CP et la formule L V a est quivalente
58. le p dagogiser Comme toujours on d finit les formules en premier D finition 2 1 1 Les formules propositionnelles du second ordre que nous ap pelons formules dans ce chapitre en l absence d ambiguit sont d finies par r cur rence comme suit la constante propositionnelle T la formule vraie est une formule les variables propositionnelles a 3 y sont des formules si A et B sont des formules alors A B est une formule si a est une variable propositionnelle et A est une formule alors Va A est une formule On note F l ensemble des formules et V l ensemble des variables propositionnelles Afin d all ger l criture des formules nous crivons A B C les formules de la forme A B C De m me nous crivons Ya A B les formules de la forme Va A gt B Puis on d finit les ensembles d hypoth ses c est dire les contextes 17 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre D finition 2 1 2 Un contexte propositionnel du second ordre est un ensemble fini de formules et dans ce chapitre nous les appelons contextes Un jugement pro positionnel du second ordre est un triplet not T H F avec T un contexte F une formule et id un identifiant textuel Dans ce chapitre les jugements propositionnels du second ordre sont appel s jugements Le contexte vide est repr sent par le mot vide ainsi pour toute formule F et tout identifian
59. les fonctions l existence de points fixes pour tous les ensembles produit des incoh rences comme dans le paradoxe de Russell mais dans le cas des fonctions cela nous permet de programmer r cursivement et ainsi de repr senter tout ce qui est calculable le A calcul est le prototype des langages de programmation fonctionnels Toujours dans les ann es 1930 Arendt Heyting 19 et ind pendamment An dreii Kolmogorov 23 explicit rent la signification informelle des op rateurs lo giques dans la logique intuitionniste donnant ainsi naissance l interpr tation de Brouwer Heyting Kolmogorov ou BHK interpr tation Chaque connecteur logique est interpr t en termes de preuves une preuve de A B est un couple compos d une preuve de A et d une preuve de B une preuve de V B est compos e soit d une preuve de A soit d une preuve de B une preuve de B est une construction qui transforme toute preuve de en une preuve de B etc Chaque preuve intuitionniste poss de alors un contenu algorithmique qui laisse pr sager 101 CHAPITRE 4 calcul p dagogique simplement typ l existence de processus associ s aux preuves la fin des ann es 1960 William Howard 21 exprima clairement le lien entre les preuves intuitionnistes et les pro cessus en identifiant les preuves des fonctions du calcul lien d j en gestation dans les travaux de Haskell Curry 8 il porte aujourd hui le nom d isomorphisme de
60. nulle une implication A B est nulle quand la formule A est fausse quel que soit l instanciation de ses variables libres Dans le cas contraire l implication est dite non nulle La nullit est principalement un concept s mantique car il fait intervenir la notion de v rit Comme nous travaillons dans un contexte purement syntaxique nous introduisons le concept d implication syntaxiquement nulle une implication A B est syn taxiquement nulle quand la formule A n est pas motivable dans le cas contraire l implication est syntaxiquement non nulle La non nullit est une propri t tr s forte qui n est videmment pas toujours v rifi e en particulier le calcul F CP admet des occurrences d implications nulles dans certaines d rivations Exemple d rivation du jugement Va a Va a 1 T par P Ax 2 6H 8 par P Hyp et 1 3 H2B B par gt et 2 4 HE VB 8 B par vi et 3 5 F Va a Va a par Ve et 4 La formule Va a d finissant l absurde dans CP n est videmment pas motivable car CP est un calcul coh rent l implication Va a Va a est donc nulle dans F CP elle l est galement dans CP Comme Va a est une formule close elle n est pas motivable donc l implication Va a Va a est aussi syntaxiquement nulle La propri t de nullit des jugements est d finissable de la m me mani re que la nullit des implications un jugement l E F est nul quan
61. ordre n abr g en P CP est d fini par sa morphologie constitu par l ensemble des jugements de la forme TFS F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles P Ax P Hyp i gt e Vi P Ve a et ainsi que de la r gle suivante TH a A F TH A B T o B F E Le calcul P CP est galement appel le calcul propositionnel p dagogique d ordre sup rieur On dit qu un jugement I F F est d rivable quand il existe une d riva tion dans P CP dont la derni re r gle utilis e produit ce jugement 69 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur 3 4 2 Non nullit syntaxique des implications Nous allons d montrer que pour tout n l ment de 2 w les calculs P CP respectent la propri t de non nullit syntaxique des implications dont la d finition est facilement g n ralis e l ordre sup rieur D finition 3 4 3 Soient n l ment de 2 w et C un calcul dont la morphologie est constitu e par l ensemble des jugements de la forme TH F Une implication A B est syntaxiquement non nul quand la formule A est motivable dans C Nous allons en fait prouver un r sultat plus fort tous les sous pr dicats des for mules apparaissant dans les d rivations des calculs P CP sont motivables par une seule et m me motivation la motivation T qui remplace toutes les variable
62. programmes de nature informatique via un isomorphisme dit de Curry Howard La g n ralisation aux formules non existentielles permet alors de justifier les formules par le programme informatique dont elles d crivent les propri t s une formule A B repr sente un programme qui pour tout programme d crit par A construit un programme d crit par B de meme une formule A A B d crit un couple de deux programmes A d crivant le premier et B le second Chaque connecteur logique est ainsi interpr t sous la forme d une construction informatique les formules sont maintenant justifi es par des objets de nature diff rentes travers une s mantique dite fonctionnelle on sait maintenant de quoi parlent les formules elles parlent d actions automatisables d une capacit concr tiser l objet du discours Bien que la s mantique fonction nelle donne un sens bien d fini aux formules d montrables la signification apport e aux formules non d montrables semble assez floue Dans les syst mes constructifs la n gation A d une formule A est usuellement d finie par l implication A L avec L la formule absurde celle qui n admet aucune repr sentation La formule A est r futable quand sa n gation est d montrable alors L est repr sent sous la forme d une fonction qui attend un programme d crit par et qui calcule un programme d crit par L La formule L n ayant pas de repr sentation fonction nelle A
63. propositionnels p dagogiques d ordre sup rieur Lemme 3 4 17 Soient n un l ment de 2 w et o une substitution triviale dans P CP Pour tout pr dicat A et B si A B alors A est o UTM dans P CP si et seulement si B est o UTM dans P CP D monstration Par r currence sur la d rivation de A B lt gt ar ce cas est imm diat Pen Qyar ce cas est imm diat a A A B B AB Vip a supposons que la formule A B soit o UTM dans P CP Ainsi les formules et B sont o UTM dans P CP Par hypoth se de r currence les formules A et B sont o UTM dans P CP Le jugement Fp o A B est ais ment d rivable par la r gle a Ainsi la formule A B est o UTM dans P CP L autre sens de l implication est analogue a 7 A a B 7y B 7 Fr A B Var VOB ay supposons que la formule Va A soit o UTM dans P CP Soit U une formule d rivable dans P CP La for mule A est a U UTM dans P CP D apr s le lemme 3 4 16 la formule a y A est o y U UTM dans P CP Par hypoth se de r currence la formule 3 y B est a y y U UTM dans P CP D apr s le lemme 3 4 16 la formule B est o g B U UTM dans P CP Le jugement H5 o VBF B est ais ment d rivable par la r gle a Ainsi la formule V3 B est o UTM dans P CP L autre sens de l implication est analogue la y A a 8 y B y FA B ar AB B
64. que H U tu B par hypoth se de r currence H U tu B ainsi H U t F F Va A supposons que H U t F par d finition il existe un type U clos tel que le jugement H2 tU a U A soit d rivable et que U tU a U A donc U tU a U A ainsi H U t F Nous pouvons ainsi construire le point fixe de la propri t H U t F 121 CHAPITRE 5 A calcul p dagogique du second ordre Lemme 5 4 2 Soit C un calcul dont la morphologie est constitu e par l ensemble des jugements de la forme T H t F Il existe une propri t U t F portant sur t un terme et F un type telle que pour tout A terme t et tout type F U t F si et seulement si H U t F D monstration D apr s le lemme 5 4 1 la propri t H U t F est croissante par rapport U ainsi d apr s le th or me de point fixe de Knaster Tarski il existe une propri t U t F telle que pour tout terme t et tout type F U t F si et seulement si H U t F Le pr dicat U d fini dans le pr c dent lemme poss de des propri t s qui ne sont pas exprimables par r currence sur ses arguments car elles seraient alors mal fond es elles motivent la construction de U par point fixe Lemme 5 4 3 Soit C un calcul suppos coh rent dont la morphologie est consti tu e par l ensemble des jugements de la forme T H t F Soit U t F la propri t d finie dans le lemme 5 4 2 pour tout terme t et pour tout
65. s mantique positive m ne l exp rimentation de l acquisition du savoir travers des processus automatiques Ce projet est tr s ambitieux on esp re dans un premier temps d gager clairement et rigoureusement certaines propri t s du savoir abstrait Un exemple serait l impl mentation d une m thode de raison nement par g n ralisation dans le cadre de l intelligence artificielle La machine commence par extraire une repr sentation d une partie de son environnement par mesure directe via des capteurs qu elle conserve en m moire l aide de formules Ces formules sont n cessairement closes c est dire qu elle ne porte que sur des objets concrets Puis la machine construit des formules destin es repr senter un savoir abstrait en substituant certains sous termes des formules concr tes par des variables libres Il ne reste plus qu d montrer les formules abstraites la machine peut s aider de strat gies de preuve automatiques mais elle dispose de l information contenue dans le processus suivi lors de la construction des formules concr tes la d rivations des propri t s concr tes de l environnement servirait alors de guide lors de la d monstration des propri t s abstraites Il s agit ici de red finir le raisonnement par induction dans le cadre d un syst me formel positif par l m me on red finit la notion d abstraction conform ment aux s mantiques posi tives toute notion abstraite
66. sup rieur 3 1 Rappel sur les calculs propositionnels d or dre sup rieur Dans le calcul propositionnel du second ordre la quantification universelle porte uniquement sur des variables repr sentant des formules On voudrait pouvoir galement manipuler l int rieur du calcul des objets repr sentant des propri t s portant sur des formules qu on appelle des pr dicats propositionnels Les objets sur lesquels portent un pr dicat ainsi que la nature des objets produits par le pr dicat sont d crits par son genre D finition 3 1 1 Les genres sont d finis par r currence comme suit la constante x le genre des formules est un genre sik ete sont des genres alors k est un genre Afin d all ger l criture des genres nous crivons k 0 les genres de la forme k gt t 0 Tous les genres sont de la forme K gt Kn gt x et sont not s Ky x quand n 0 cette notation repr sente le genre x Les formules sont de genre x et les pr dicats portant sur des objets de genre et produisant des objets de genre amp ont pour genre K 4 Il ne reste plus qu d finir les pr dicats D finition 3 1 2 Les pr dicats sont d finis par r currence comme suit la constante T est un pr dicat de genre x les variables propositionnelles a 3 y sont des pr dicats de genre K L APE si A et B sont des pr dicats de genre x alors A B est un pr dicat de
67. t invent e dans le but de codi fier les raisonnements corrects et rigoureux se pr server de l erreur permettant de construire un savoir pertinent et efficace Les syst mes formels se sont peu peu distingu s comme l aboutissement le plus pur de cette recherche d exactitude Il convient cependant de trouver un moyen de lier les formules des syst mes for mels qui sont de simples juxtaposition de symboles une repr sentation qui leur donne un sens les syst mes formels ont besoin d une s mantique Parmi toutes les s mantiques d velopp es dans le cadre de l tude math matique des syst mes formels certaines d crivent mieux que d autres le sens ontologique donner aux formules selon le bon sens de chacun Mais le bon sens comptant parmi les choses les moins partag es plusieurs approches se distinguent les unes des autres Parmi les s mantiques les plus utilis es la notion de mod le est incontournable Un mod le est une structure math matique fournissant une interpr tation chaque symbole constituant les formules chaque symbole de fonction est repr sent par une fonction chaque symbole de relation est interpr t par une relation etc puis XIV chaque connecteur logique est interpr t directement par exemple l interpr tation d une formule conjonctive A B est la conjonction au sens math matique des interpr tations de et de B On cherche essentiellement plonger le syst me fo
68. t s algorithmiques des traductions CPS ce r sultat met en vidence la possibilit de repr senter fidelement et p dagogiquement les pro grammes typables dans AC l int rieur de P AC Comme toujours dans les systemes d ordre sup rieur nous avons besoin d un lemme de substitution Lemme 5 5 1 Pour tout type F et U nous avons y U7 F a U F D monstration Imm diat par induction sur F Dans notre contexte p dagogique il convient que les types soient tous motivables il faut alors prouver que la y traduction transforme n importe quel type en un type motivable Lemme 5 5 2 Notons u la substitution y T Soient F un type etT un contexte motivable dans P C Pour toute variable fra che pour T U F le jugement TH uF est d rivable D monstration Par r currence sur F F T nous avons pT T gt T gt T et le jugement T H3 T T gt est ais ment d rivable F a nous avons pa a gt T gt T et le jugement PF a T gt est ais ment d rivable F A B par hypoth se de r currence le jugement Ea AT est d rivable le contexte P U x u A7 est motivable dans P AC ainsi par hypoth se de r currence le jugement l x w A7 Fip u B7 est d rivable nous d rivons alors le jugement T u A B7 avec la r gle d apr s le lemme 5 2 1 le type A B7 est motivable dans P C donc le jugement D4 W AT BY T T
69. tout ces syst mes p dagogiques toutes les formules motivables admettent la m me mo tivation la plus simple de toutes la motivation T Cette caract ristique a de nombreuses contreparties philosophiques tout d abord car elle constitue l expres sion math matique que pour un nonc sens il n y a qu une seule mani re d tre vrai les objets effectifs n ont qu une seule modalit d existence formelles en suite car c est gr ce elle que l isomorphisme de Curry Howard est applicable aux syst mes formels p dagogiques permettant ainsi l apparition de syst mes fonction nels p dagogiques sous la forme de calculs typ s nous sommes alors en mesure de sp cifier p dagogiquement des programmes informatiques notre connais sance aucun syst me fonctionnel sans n gation n a t con u avant les calculs p dagogiques except le A calcul simplement typ puisqu il est naturellement po sitif De plus les propri t s des syst mes formels se transportent dans les syst mes fonctionnels ce qui nous a permis d introduire la notion d utilit dans les A calculs 129 Conclusion un programme est utile quand son contenu algorithmique est utilisable Il est notable que tous les chercheurs s tant pench s sur les math matiques sans n gation n aient jamais commenc par l tude des logiques propositionnelles leur travail concerne exclusivement les logiques des pr dicats De ce point d
70. type F si F T ou F a alors U t F si et seulement si le jugement H t F est d rivable si F A B alors U t F si et seulement si il existe un A terme u clos tel que le jugement F tu B soit d rivable et que U tu B si F Va A alors U t F si et seulement si il existe un type U clos tel que le jugement H3 tU a U A soit d rivable et que U tU a U A D monstration Par cas sur F F T par d finition de H U t F U t F si et seulement si le jugement H2 t F est d rivable F a analogue au cas pr c dent F A B par d finition de H U t F U t F si et seulement si il existe un terme u clos tel que le jugement H tu B soit d rivable et que H U tu B et par d finition de U tu B nous avons H U tu B si et seulement si U tu B F Va A par d finition de H U t F U t F si et seulement si il existe un type U clos tel que le jugement tU a U A soit d rivable et que U tU a U A Grace la propri t U construite dans le lemme 5 4 2 nous sommes en mesure de d finir formellement ce que signifie tre utile pour un A terme du second ordre D finition 5 4 2 Soit C un calcul dont la morphologie est constitu e par l en semble des jugements de la forme T 2 t F Soit U t F la propri t d finie dans le lemme 5 4 2 Soit t un A terme tel qu il existe un jugement T H3 t F d rivable 122 5 4 Utilit Le te
71. 27 28 29 Bibliographie J Y Girard Interpr tation fonctionnelle et limination des coupures dans l arithm tique d ordre sup rieur Th se d tat Universit de Paris 7 1972 K G del Zur intuitionistischen Arithmetik und Zahlentheorie Ergebnisse eines mathematischen Kolloquiums 4 1933 pp 34 38 G F C Griss Negationless Intuitionistic Mathematics Indagationes Mathe matice 8 1946 pp 675 681 G F C Griss Negationless Intuitionistic Mathematics II Indagationes Ma thematic 12 1950 pp 108 115 G F C Griss Negationless Intuitionistic Mathematics II Indagationes Ma thematicee 13 1951 pp 193 199 G F C Griss Negationless Intuitionistic Mathematics IVa IVb Indaga tiones Mathematic 13 1951 pp 452 462 463 471 A Heyting Mathematische Grundlagenforschung Intuitionismus Beweis teorie Springer 1934 A Heyting Intuitionism an Introduction Studies in Logic and the Foun dations of Mathematics North Holland 1956 W Howard The formulae as types notion of construction To H B Curry Essays on Combinatory Logic Lambda Calculus and Formalism Academic Press Limited 1980 pp 479 490 manuscript original de 1969 S C Kleene Introduction to Metamathematics North Holland 1952 A N Kolmogorov Zur Deutung der intuitionistischen Logik Mathema tische Zeitschrift Vol 35 1932 pp 58 65
72. 40 pp 56 58 L Colson Quelques remarques sur l environnement dans la Th orie Intui tionniste des Types D E A report University of Paris Sud Orsay Septem ber 1986 L Colson D Michel Pedagogical Natural Deduction Systems the Pro positional Case Journal of Universal Computer Science 13 10 2007 pp 1396 1410 L Colson and D Michel Pedagogical Second order Propositional Calculi Journal of Logic and Computation 18 4 2008 pp 669 695 H B Curry Functionality in Combinatory Logic Proceedings of the Natio nal Academy of Sciences Vol 20 pp 584 590 P de Groote A CPS Translation of the Ayi Calculus Lecture Notes in Com puter Science Vol 787 Springer Verlag 1994 pp 85 99 H Friedman Classically and Intuitionistically Provably Recursive Functions Higher Set Theory Springer Lecture Notes Vol 669 1978 pp 21 27 G Gentzen Investigations into Logical Deduction Mathematische Zeit schrift 39 1935 pp 176 210 405 431 Reprinted in The Collected Papers of Gerhard Gentzen Studies in Logic and the Foundations of Mathematics North Holland 1969 P C G Gilmore The Effect of Griss Criticism of the Intuitionistic Logic on Deductive Theories Formalized within the Intuitionistic logic Indagationes Mathematic 15 1953 pp 162 174 175 186 131 13 14 15 16 17 18 19 20 21 22 23 24 25 26
73. 7 nous d rivons H T F Les jugements H T T et H F F sont d rivables d apr s la proposition 2 5 6 Ainsi le jugement I F est d rivable de m me que le jugement T F Grace aux lemmes 2 5 5 et 2 5 7 nous avons les outils pour d montrer que la y traduction pr serve la notion de d rivation Proposition 2 5 8 Le jugement T F est d rivable si et seulement si le juge ment T7 F3 Fest d rivable avec y une variable fra che pour TU F D monstration Cons quence imm diate des lemmes 2 5 5 et 2 5 7 Ainsi les calculs CP F CP et P CP sont aussi puissants les uns que les autres du point de vue de la d rivabilit 2 5 2 Traduction de CP dans F CP Pour qu une traduction soit pertinente il faut non seulement qu elle pr serve la d rivabilit mais aussi que les formules restent quivalentes m me apr s tra duction Le lemme 2 5 6 atteste que pour toute formule F la formule F est quivalente F Il reste prouver que F est un th or me de CP si et seulement si F est un th or me de F CP afin de montrer que F est une traduction fid le de F dans F CP Proposition 2 5 9 Pour toute formule F le jugement F si et seulement si le jugement F est d rivable D monstration Deux cas sont consid rer supposons que le jugement F est d rivable D apr s la proposition 2 5 8 le jugement Ee FT est d rivable Donc le jugement F7 es
74. 8 x v u 107 CHAPITRE 4 calcul p dagogique simplement typ Quand on ne peut plus r duire un A terme cela signifie que le programme associ a achev son ex cution et on obtient alors la donn e correspondant au r sultat de l valuation Un terme qui repr sente un r sultat est dit en forme normale D finition 4 4 2 Un terme t est en forme normale quand pour tout terme u tel que t g u on at u Quand on value un A terme ses propri t s statiques ne changent pas il calcule toujours la m me chose il admet toujours les m mes arguments et on peut toujours s en servir de la m me mani re cela signifie que le type d un A terme doit rester stable par r duction Proposition 4 4 1 Soient IT un contexte t et u deux termes et F un type Si le jugement T Fas t F est d rivable et t g u alors le jugement T ip u F est d rivable D monstration Supposons que le jugement T ae t F soit d rivable d apr s la proposition 4 3 2 le jugement T H t F est d rivable AC est stable par 8 r duction donc le jugement u F est d rivable ainsi d apr s la proposition 4 3 2 le jugement Py u F est d rivable Le type d un terme repr sente ce qui est calcul par ce terme comme quelque chose est calcul on s attend obtenir cette chose la fin de l valuation cela implique que toute valuation termine on dit alors que les termes typables sont normalis
75. Al BIB A B A B A et BY B 7 et par d finition nous avons A BY AT B ainsi que A B A B donc A B 4 B par la r gle a a d A a 9 5 B_ 6 Fr 4 B Va A V5 B avons a 5 4 5 6 B 7 Par une r currence imm diate sur A nous avons a 6 A 7 a 6 A7 de m me nous avons 3 6 B 3 6 B7 donc Ya A V3 B7 par la r gle ay par d finition nous avons Va AT Ya A et V3 B7 VG B donc Ya A VG B a par hypoth se de r currence nous avons A ay par hypoth se de r currence nous Pour plonger CP dans ses variantes p dagogiques il faut que la traduction transforme toute formule en une formule motivables ce que nous d montrons dans les deux lemmes suivant 44 2 5 Traductions Lemme 2 5 2 Pour toute formule F et pour toute variable y fra che pour F le jugement y za F7 est d rivable D monstration Par r currence sur F F T le jugement y H2 T est ais ment d rivable F a le jugement y H a V y est facilement d rivable F A B par hypoth se de r currence le jugement y Be B7 est d rivable D rivons maintenant le jugement H2 y T A 1 y Ee A par hypoth se de r currence Po hae AT par jet 1 H2 Vy y AY par Vi et 2 par P Ax y T A par P V 3 et 4 6 2 y T A par gt e 4 et 5 Ainsi A7 est motivable dans P
76. Fr T Enfin on d finit les substitutions sur les types D finition 5 1 5 Une substitution o est une fonction de domaine fini Dom o valeurs dans l ensemble des types Notation 5 1 1 Pour toute substitution o on note VI o l union des ensembles Vl o a pour tout a Dom o 110 5 1 A calcul du second ordre D finition 5 1 6 Pour toute substitution o et pour tout type F on dit que o est adapt e F quand l ensemble VI o O Vq F est vide D finition 5 1 7 Pour tout type F et pour toute substitution o adapt e F l application de o F not e o F est d finie par r currence sur F comme suit Sl d Due ete ala sia Dom o a sinon F A gt B 0 F 0 A o B F Va A oF Vaw A Apr s avoir d fini les types on introduit les termes qu ils vont typer D finition 5 1 8 Les termes propositionnels du second ordre que nous appe lons A termes dans ce chapitre en l absence d ambiguit sont d finis par r currence comme suit la constante o est un terme les variables x y z sont des termes six est une variable A un type ett un A terme alors x4 t est un terme sit etu sont des termes alors tu est un terme si a est une variable et t un A terme alors Aa t est un A terme sit est un terme et A un type alors tA est un terme Afin d all ger l criture des A termes nous crivons twv les termes de l
77. H F d rivable l ensemble TU F est HTM dans P CP D monstration Par r currence sur la d rivation de T Fe F 2 oT T Fe ji F est HTM donc d apr s le lemme 2 3 6 la formule F est HTM ainsi l ensemble FU T est HTM Fer Fe oT TH F Ax LAr B T a A B HTM et la formule A B est TM d apr s la proposition 2 3 1 T a AB Tr Be A T Pe B TU A B est HTM P Ax Soit F un l ment de I par hypoth se de r currence P Hyp le raisonnement est analogue celui du cas P par hypoth se de r currence l ensemble T U A B est par hypoth se de r currence l ensemble TH A ag VIT p o se NY T F7 Va 2 Vi le raisonnement est analogue celui du cas T H Ya A 2a U p p WW A T F2 AU P V par hypoth se de r currence o U est HTM donc d apr s le lemme 2 3 6 la formule U est HTM par hypoth se de r cur rence l ensemble F U A est HTM donc d apr s le lemme 2 3 7 la formule a U A est HTM THA A B rH B est HTM d apr s le lemme 2 3 8 a par hypoth se de r currence A est HTM donc B Parmi toutes les motivations triviales on distingue la motivation rempla ant toutes les variables libres des formules par la constante T qui repr sente la plus simple des motivations triviales on l appelle par abus de langage la motivation T Elle est d j pr sente dans le chapitre 1 car dan
78. Il est regrettable que les calculs PC CP pour n 3 w ne satisfassent pas la propri t de non nullit syntaxique des implications En effet nous allons construire un jugement ae G G d rivable tel que la formule G close ne soit pas motivable dans PC CP Tout d abord nous construisons la formule G requise 67 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur Lemme 3 3 3 Soient V Va a a H Va JT a et G Yy7 H yV Le jugement He G n est pas d rivable D monstration Toutes les d rivations dans le syst me CP admettent une forme normale voir 13 Supposons qu il existe une d rivation en forme normale du jugement G Ainsi le jugement H yV poss de une d rivation en forme normale dans laquelle une application de la r gle Hyp d rive le jugement H H H suivie par une s quence d applications des et Ye Nous pouvons uniquement appliquer la r gle Ve sur le jugement H H afin de d river un jugement de la forme H E q T U Nous ne pouvons appliquer ni la r gle ni la r gle Ve sur le jugement H FY T U donc nous avons y T U yV ce qui est contradictoire puisque la formule V n est pas de la forme T U Ainsi le jugement G n est pas d rivable Comme PC CP est un sous syst me de CP le jugement Fy G n est pas d rivable Ensuite nous d rivons le jugement Ex GG Lemme 3 3 4 Soient F
79. P avec a Fr A B soit U une formule d rivable dans P CP la formule Pa Qa est lo a U UTM dans P CP par hypoth se de r currence les pr dicats Pa et Qa sont o a U UTM dans P CP donc P et Q sont ai a U UTM dans P CP ainsi d apr s le lemme 3 4 11 les pr dicats P et Q sont o UTM dans P CP Lemme 3 4 15 Soient n un l ment de 2 w et o une substitution triviale dans P CP Pour tous pr dicats P U x et V k si la U P U et V sont o UTM dans P CP alors a V P est o UTM dans P CP D monstration Par r currence sur P P T ce cas est imm diat 77 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur P 6 deux cas se pr sentent B a nous avons a V P V comme V est o UTM dans P CP a V P est galement u UTM dans P CP B a nous avons a U P a V P comme a U P est o UTM dans P CP a V P est galement o UTM dans P CP P A B par hypoth se de r currence a V A et a V B sont o UTM dans P CP a U P est motivable par dans P CP donc d apr s le lemme 3 4 6 a U P est motivable par dans P CP ainsi a V P est o UTM dans P CP P VB A par a quivalence on peut supposer que 3 a soit W une formule d rivable dans P CP par hypoth se de r currence a V A est Los G W UTM dans P CP a U P est motivable par o dans P CP donc d ap
80. P si P est o UTM dans P CP et U u UTM dans P CP alors pour toute substitution p triviale dans P CP telle que Dom p Dom o a U Dom y le pr dicat a U P est p UTM dans P CP D monstration Par r currence sur P P T soit p une substitution triviale dans P CP telle que Dom p Dom o a U Dom p le pr dicat a U P est UTM dans P CP P 6 soit p une substitution triviale dans P CP telle que Dom p Dom o a U Dom u deux cas se pr sentent B a d apr s le lemme 3 4 11 U est p UTM dans P CP d apr s le lemme 3 4 7 p motive U dans P CP nous avons U a U P donc p motive a U P dans P CP ainsi a U P est p UTM dans P CP B a le pr dicat P est o UTM dans P CP comme P CP est coh rent le jugement gt P n est pas d rivable donc 3 Dom o ainsi 6 Dom p et le jugement Hp p P est d rivable comme P a U P le pr dicat a U P est UTM dans P CP P A B soit p une substitution triviale dans P CP telle que Dom p Dom a U Dom y d apr s le lemme 3 4 11 P est p UTM dans P CP donc p motive P dans P CP d apr s le lemme 3 4 7 de m me p motive U dans P CP donc la substitution a p U est triviale dans P CP d apr s le lemme 3 4 6 le 76 3 4 Calculs propositionnels p dagogiques d ordre sup rieur jugement FF p a a p U P est d rivable nous avons a
81. ROS Ges Ss ON dns Ge 2 52 PAA UCtIONS eases e 28 e ee le AS De ae SS 25l Setraduchione Aad bed hos a ee oe he Be ae 2 5 2 Traduction de CP dans F CP 2 5 3 Traduction de CP dans P CP 2 eis web dune Calculs propositionnels p dagogiques d ordre sup rieur 3 1 Rappel sur les calculs propositionnels d ordre sup rieur 3 2 Calculs propositionnels faiblement p dagogiques d ordre sup rieur 3 2 1 Pr sentation des calculs 4 5 2 Page dd ee ee D ae 3 2 2 Non nullit syntaxique des jugements 3 2 3 La r gle affaiblissement cone ess au nue ARS 3 2 4 Les th or mes de CP sont prouvables dans F CP 1 3 3 Calculs propositionnels p dagogiques contraints d ordre sup rieur 3 3 1 Pr sentation des calculs 424 m ee ace 26 de 0 GE 3 3 2 Non nullit s mantique des implications 3 3 3 Certaines implications sont syntaxiquement nulles 3 4 Calculs propositionnels p dagogiques d ordre sup rieur 3 4 1 Pr sentation des calculs 2 288 8 22 an dus Ew are 3 4 2 Non nullit syntaxique des implications 3 9 Traductions spes na Oe Ae SSSA EE MRA A BE ES Systemes fonctionnels p dagogiques A calcul p dagogique simplement typ AA A calcul simplement L 4 ts de nee ut OE So Oe BA 4 2 calcul p dagogique simplement typ 4 3 Traduction o o et ne sd oe Und cht Deo ie ad
82. Serge et J r me Un grand merci aussi au secr taire du LITA Damien Aignel sans qui les in vitables tracasseries de administration auraient eu raison de moi Merci galement tous les membres du d partement informatique de l IUT de Fontainebleau qui m ont accueilli parmi eux depuis que je suis ATER l Universit Paris 12 Bien s r je tiens remercier mes parents mon fr re mes s urs et toute ma famille pour leur soutien sans faille depuis toujours Enfin j exprime ma reconnaissance envers toutes les personnes que je n ai pas cit es elles sont nombreuses et se reconnaitront vi Introduction Il est commun dans la pratique des math matiques de fournir des exemples d objets math matiques afin d illustrer des concepts abstraits Cette observation a fait l objet d tudes en philosophie des math matiques en particulier Henri Poin car sugg rait dans 34 que toute d finition devrait tre imm diatement suivie d un exemple lui donnant un sens Malgr cette injonction les syst mes formels utilis s dans le cadre des fondements des math matiques comme les syst mes axio matiques de Hilbert ou les calculs des s quents ignorent totalement le dictum de Poincar Parall lement George Francois Cornelis Griss proposait dans une s rie d articles 15 16 17 et 18 que les math matiques devraient tre d velopp es sans l aide de la n gation Il avan ait que les d finitions math m
83. TES pvc f A B avec la r gle i TH Aer i g A T ae fg F ments p I EX wef u A F et w P EX weg pA sont d rivables ainsi nous d rivons le jugement u I Fip u fg u F avec la r gle gt e Dhs B amp VI T T Fip AB f VG A T ee uf pA est d rivable par a quivalence nous pouvons supposer que a 3 nous d rivons alors le jugement p T Ein LAG f u Y8 A avec la r gle V T Fip f VBA HoV TF JV BWA uT Pas uf u YB A est d rivable le type u V est motivable dans P C d apr s les lemmes 5 3 3 et 5 2 1 par a quivalence nous pouvons supposer que a p et a VI U nous d rivons alors le jugement wF EX w fV ju G V A avec la r gle P Ve TH t G Ga THF uT Fip u t u G est d rivable par une r currence imm diate sur la d rivation de G F nous avons 4 G u F ainsi nous d rivons le jugement p TF4 pet pF avec la r gle a P Ax nous avons o 0 et T u T le contexte y T est par hypoth se de r currence le jugement p par hypoth se de r currence les juge Vi par hypoth se de r currence le jugement u P Ve par hypoth se de r currence le jugement a par hypoth se de r currence le jugement 119 CHAPITRE 5 calcul p dagogique du second ordre Lemme 5 3 5 Pour tout jugement d rivable T oe Aa t U a U F le jugement TH a U t a U F est d rivable D monstration Par h
84. THESE pr sent e a L UNIVERSITE PAUL VERLAINE METZ pour obtenir le titre de DOCTEUR DE L UNIVERSITE PAUL VERLAINE METZ Sp cialit INFORMATIQUE Systemes formels et syst mes fonctionnels p dagogiques par DAVID MICHEL Soutenue le 24 octobre 2008 devant le jury compos de Patrick C GIELSKI fas wien di demie rapporteur LOI COLSON milione esae a a a a eut Gen directeur de th se Gilles DOW EK s cerris et ex neuen ee e ee wes rapporteur Serge GRIGORIEFF nc ati en pr sident du jury Maurice MARGENSTERN cccceceececeececeees examinateur paul AVERTISSEMENT riaine universite metz Cette th se est le fruit d un long travail approuv par le jury de soutenance et disponible l ensemble de la communaut universitaire largie Elle est soumise la propri t intellectuelle de l auteur au m me titre que sa version papier Ceci implique une obligation de citation de r f rencement dans la r daction de tous vos documents D autre part toutes contrefa ons plagiats reproductions illicites entra nent une poursuite p nale Enfin l autorisaton de diffusion a t accord e jusqu nouvel ordre gt Contact SCD Metz daniel michel scd univ metz fr Code de la Prori t Intellectuelle articles L 122 4 Code de la Prori t Intellectuelle articles L 335 2 L 335 10 http www cfcopies com V2 leg leg_droi php http www culture gouv fr culture infos pratiques droits protec
85. Tr H ern eA Vl c U telle que p a T pour toute variable a Dom p par hypoth se de r currence la formule o U est p UTM dans P CP d apr s le lemme 3 4 12 la formule U est HDom o UTM dans P CP d apr s le lemme 3 4 11 la formule U est u UTM dans P CP par hypoth se de r currence TU Va A est u UTM dans P CP donc A est w a a T UTM dans P CP d apr s le lemme 3 4 13 la formule a U A est u UTM dans P CP ainsi T U a U A est u UTM dans P CP Th le A F Tr A B r E5 oleae die UTM dans P CP par hypoth se de r currence la formule A B est u UTM dans P CP d apr s le lemme 3 4 14 les pr dicats A et B sont u UTM dans P CP par hypoth se de r currence la formule a A F est u UTM dans P CP par hypoth se de r currence la formule A est pp UTM dans P CP donc d apr s le lemme 3 4 15 la formule a B F est u UTM dans P CP TRA A 8B TH B dans P CP d apr s le lemme 3 4 17 la formule B est UTM dans P CP ainsi l U B est u UTM dans P CP TEA A B r B dans P CP d apr s le lemme 3 4 17 la formule B est UTM dans P CP ainsi IT U B est u UTM dans P CP P V notons p la substitution dont le domaine est Ext par hypoth se de r currence I est p a par hypoth se de r currence T U A est u UTM g par hypoth se de r currence U A est u UTM Par cons quent nous avo
86. Vi u U VI v Quand VI t 0 nous disons que le terme t est clos D finition 4 2 4 Pour tout terme t l ensemble Vq t des variables quan tifi es de t est un ensemble de variables d fini par r currence sur t t 0 Vath U t Nat b t dc4 u Va t x U Vq u t w Va t Vq u U Va v 104 4 2 calcul p dagogique simplement typ De m me que nous avons d fini les substitutions sur les types nous allons d finir les substitutions sur les termes D finition 4 2 5 Une substitution o est une fonction de domaine fini Dom o valeurs dans l ensemble des termes Pour toute A substitution on note VI o l union des ensembles Vl o x pour tout x Dom o D finition 4 2 6 Pour toute substitution o et pour tout A terme t on dit que o est adapt e at quand l ensemble VI o N Va t est vide D finition 4 2 7 Pour tout terme t et pour toute substitution o adapt e t l application de o at not e o t est d finie par r currence sur t comme suit t 0 ot 0 PT A a z si x Dom o xz sinon t Ar4u ot Ne oe t s t w ot oa ua v Soient I un contexte F un type o une substitution et id un identifiant On note t o F les jugements de la forme H4 t o F De m me les ensembles de jugements t o F avec x F ET sont not s F4 oT quip s de substitutions nous pouvons maintenant p dagogiser AC D finition 4 2 8 Le calcul p dagogique simple
87. a 6 T Va f a cela signifie que cette formule ne peut pas tre consid r e comme un l ment atomique du calcul 2 3 Calcul propositionnel p dagogique du se cond ordre 2 3 1 Pr sentation du calcul Nous avons constat que le jugement L L est d rivable ce qui est g nant pour un syst me p dagogique Il n est pas souhaitable que des formules non motivables puissent appara tre dans les formules des d rivations d un cal cul p dagogique On remarque que la preuve de L L demande aux va riables quantifi es de pouvoir tre instanci es par des formules non motivables Pour viter de rencontrer des sous formules non motivables dans une d rivation il suffit de n autoriser que l instanciation des variables quantifi es par des formules motivables Ainsi nous allons remplacer la r gle Ve par la r gle P V TH Ya A HoU T H a U A afin de d finir le calcul propositionnel p dagogique du second ordre P V D finition 2 3 1 Le calcul propositionnel p dagogique du second ordre abr g en P CP est d fini par sa morphologie constitu par l ensemble des jugements de la forme T Ez P sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles P Ax P Hyp i e Vi et a ainsi que de la r gle suivante T Es Va A Es a U TH a U A On dit qu un jugement T Fe F est d rivable quand il existe une d rivation
88. a par r currence sur K k x le jugement T F a a est ais ment d rivable kK l gt 0 nous avons a A6 O a0O 8 par hypoth se de r cur rence le jugement I H 5 0 8 est d rivable le jugement I F a a est ais ment d rivable donc le jugement I H a A8 O ap est d rivable par la r gle Ext par hypoth se de r currence le jugement T F a O1 a est d rivable donc le jugement T F a AB a8 est d rivable par la r gle Ext le jugement T a a est alors ais ment d rivable P A B par hypoth se de r currence les jugements F A A et TF B By sont d rivable le jugement T e A B A B est ais ment d rivable ainsi le jugement F A B A By est d rivable l aide de la r gle Ext nous avons alors une d rivation du juge ment THR A gt B A gt B P VB A par hypoth se de r currence le jugement T F A A est d rivable ainsi le jugement F VG A VG A est d rivable nous avons alors une d rivation du jugement I H V3 A YO A P B A soit 0 le genre du pr dicat A par hypoth se de r currence le jugement A A est d rivable nous avons A 15 A 6 et Ay AB A 6 ainsi le jugement PF AB A 8 o AG A 1G est d rivable par 95 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur la r gle g nous d rivons alors le jugement IT F B A AG A
89. a U G r donc nous avons une d rivation de F2 a U G Ainsi la formule a U G est TM Le cas de la r gle a n cessite le lemme suivant Lemme 2 3 8 Pour toutes formules F et G et pour toute substitution o adapt e F et G si F G alors o F a 0 G D monstration Par r currence sur la d rivation de F G Tegi ar nous avons o T c T car la relation est r flexive a Qyar nous avons o a C Q car la relation est r flexive AA B B A B A B o A et o B a o B et par d finition nous avons o A B o A oB et o A B o A o B donc o A B a a A B par la r gle a a y A a A y B y Fr 4 B Va A V3 B avons 0 4 a y A e angy OVB a_ par hypoth se de r currence nous avons 0 A ay par hypoth se de r currence nous ap la aa mat Q 5 10 a y Ata de m me ayt 0 8 7 NO 4 8 donc a 7 0 47 07 a F Io 6 8 ainsi par la r gle ay nous obtenons Va oi t a a YL B par cons quent Agy Va A gt 0 44 3 VG B mais comme y est une variable fraiche pour Va A et V3 B nous avons o Ya A a 0 VG B 39 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre Enfin voici le lemme principal celui qui d montre que toutes les formules conte nues dans les d rivations de P CP sont HTM Proposition 2 3 9 Pour tout jugement T
90. a a est not e L Pour toute formule F la formule F L est appel e la n gation de F et elle est not e aF Nous comptons mettre en vidence l impossibilit de faire de L une formule ab surde dans F CP en montrant qu on peut la remplacer par une variable fra che dans toutes les d rivations Pour cela nous d finissons une transformation qui remplace dans chaque formule les occurrences de la formule L par une variable fra che D finition 2 2 4 Pour toute formule F et pour toute variable y fraiche pour F nous d finissons la formule F par r currence sur F Fleet F a F a F A B F A 8B _f 7 siA a leks ie l Va A sinon La preuve du r sultat attendu sera faite par r currence sur les d rivations pour traiter le cas de la r gle Ve nous avons besoin d un lemme de substitution Lemme 2 2 8 Pour toutes formules F et U et pour toute variable y fra che pour F et U si la substitution G U est adapt e F alors B U F G U Fy D monstration La substitution 8 U est adapt e F quand G U est adapt e F car VI U A Vq F VI U A Vq F Nous d montrons maintenant le lemme par r currence sur F F T nous avons B U T T et T 6 U T donc 8 U T B U T F a deux cas se pr sentent a p nous avons G U a U et B U a Uy donc G U a 4 B U 2 af nous avons G U a a et G U a a donc G U a B U
91. a forme tu u et Ax tu les termes de la forme Ax4 tu avec u et v des termes ou des types selon les circonstances De m me nous crivons Aa tu les A termes de la forme Aa tu Puis on distingue les variables libres des variables quantifi es D finition 5 1 9 Pour tout terme t l ensemble VI t des variables libres de t est un ensemble de variables d fini par r currence sur t t 0 Vi v t rx VI t x t its VIG Vi z t w gt VI Vita U VI v t Nous Mt Vl u t uA VIG Via Quand VI t 0 nous disons que le terme t est clos D finition 5 1 10 Pour tout terme t l ensemble Vq t des variables quan tifi es de t est un ensemble de variables d fini par r currence sur t t 0 Vat Uy t Vat 0 111 CHAPITRE 5 A calcul p dagogique du second ordre t dc4 u Va t x U Va u t w Valt Vda U Valo t Aa u Vqa t Vqlu t uA Vqlt Vqlu Comme pour les types il nous faut introduire les substitution sur les types en premier lieu les A termes tant annot s par des types nous allons donner un sens l application d une substitution sur les formules un A terme D finition 5 1 11 Pour tout terme t et pour toute substitution o adapt e aux types apparaissant dans t l application deo t not e ot est d finie par r currence surt comme suit t o ot t t xz ot t t ru ot Artu t uv oaot oa ude v
92. a forme T H3 t F Pour tout contexte A une motivation de A dans C est une substitution o telle que pour tout x F A il existe un A terme t tel que le jugement H t o F soit d rivable Quand un contexte admet une motivation dans C on dit qu il est motivable De plus une motivation d une formule F dans C est une motivation du singleton F dans C L une des cons quences imm diates de l application de l isomorphisme de Curry Howard sur le calcul P CP est la possibilit de motiver tous les sous types des types apparaissant dans les d rivations de P AC Proposition 5 2 1 Pour tout jugement T Fip t F d rivable les jugements ase G sont d rivables pour tout sous type G d un type appartenant TU F D monstration Analogue la preuve de la proposition 2 3 10 115 CHAPITRE 5 calcul p dagogique du second ordre 5 3 Normalisation Apr s l introduction des A abstractions dans les termes du second ordre la B r duction se trouve alt r e par rapport au cas du calcul simplement typ vu dans le chapitre 4 Voici a quoi elle ressemble apr s modifications D finition 5 3 1 Pour tous les termes t et t la relation de G r duction entre t ett not e t g t est d finie par les r gles suivantes Cone ae Brvar u g u AAU g ATAU 8 ugu V8 uv gt uv Brapp u g u Aau g Aa u Ba u g u uA g uA Baapp t way t t RAS s g f H
93. a seule r gle d inf rence permettant d introduire de nouvelles formules dans le vu Introduction contexte I est la r gle de l hypoth se Fer PEE Hyp Dans cette r gle le contexte a pour seule contrainte d tre un ensemble de formules ventuellement non motiv ou m me contradictoire Nous introduisons alors la contrainte p dagogique comme suit nous demandons a ce qu au moins une instance o T de I soit prouvable c est dire que les jugements H o G1 F o Gy soient d rivables avec une substitution rempla ant certaines variables de I par quelques objets idoines des formules des entiers ou tout autres termes selon le cas Ainsi la r gle de l hypoth se se trouve modifi e en une r gle de l hypoth se p dagogique Fer tFoa T La contrainte p dagogique a d importantes cons quences sur les raisonnements possibles en d duction naturelle par exemple le raisonnement par contradiction n est plus autoris puisque pour prouver F en supposant F afin d en d duire une absurdit on doit en premier lieu postuler F n admettant aucun exemple o tel qu on puisse prouver F amp F Ainsi les syst mes p dagogiques se r v lent naturellement intuitionnistes Plus radicalement nous observons que la preuve d une assertion n gative F d fini par la formule F L le symbole L d notant l absurdit ne peut plus tre men e car on doit supposer F afin d en d duire mais n
94. a4 F A B par hypoth se de r currence nous avons 8 U A G U4 A et G U B B U B donc B U A gt B B U A By par d finition A B A gt B donc B U A gt B B U A B F Ya A deux cas se pr sentent A a nous avons Va A L G U 1L et G U L y donc Z U Va A G U Va A 27 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre A a deux cas sont consid rer a f nous avons G U Va A Va A et B U Va A Va A donc 3 U Va A A U Va A a Z b nous avons 6 U Va A Va B U A et par hypoth se de r currence nous avons 6 U A G U A donc F U Va A Va G U A et ainsi G U Va A 4 G U Va A De m me nous avons besoin du lemme suivant pour traiter le cas de la r gle a Lemme 2 2 9 Pour toutes formules F et G si F G alors Fy a Gy D monstration Par r currence sur la d rivation de F G ar par d finition nous avons T T donc T a T4 T EN TE Y Y Y er avar par d finition nous avons a a donc a ay A A B B A B A B A et By a Bi et par d finition nous avons A B A B et A gt B Al gt Bi donc A gt B A B par la r gle a_ a d A a B 6 B 6 Fr A B Va A Y B A a par hypoth se nous avons 6
95. able donc m motive l ensemble l U y A dans P CP et ainsi nous d rivons le jugement lu AH o A B l aide du lemme 2 3 4 le jugement T p A F yA est d rivable par la r gle P Hyp donc par hypoth se de r currence le jugement F u A ps o A est d rivable et ainsi nous d rivons I w A ES o B par la r gle par hypoth se de r currence I u A Fe LB est d rivable et ainsi nous d rivons I Ff y A B par la r gle 4 F Va A supposons que le jugement 3 o Va A soit d rivable deux cas se pr sentent a Dom o a Dom o nous avons oVa A Va o A et nous d rivons alors T Pe aA par la r gle P V par hypoth se de r currence le jugement T Fe WA est d rivable et ainsi nous d rivons p Va u A par la r gle V nous avons Dom o Dom u done u Va A Va u A et ainsi nous avons une d rivation de T H p Wa A La preuve que toutes les formules pr sentes dans les d rivations de P CP sont HTM se fera par r currence sur les d rivations Le lemme suivant nous permettra de traiter les cas des r gles P Ax P Hyp et P Ve qui sont les r gles n cessitant de motiver le contexte de leurs pr misses Lemme 2 3 6 Soient F une formule et o une substitution adapt e F Si o F est HTM dans P CP alors F est HTM dans P CP D monstration Posons o 0 pom c nvi F ainsi nous avons o F o F Soit G une sous formule de F La formule a G est une sous formule
96. able dans P CP le pr dicat A est o a a U UTM dans P CP et le pr dicat B est o UTM dans P CP D apr s le lemme 3 4 13 le pr dicat a B A est o UTM dans P CP 80 3 4 Calculs propositionnels p dagogiques d ordre sup rieur lt supposons que le pr dicat a B A soit o UTM dans P CP D apr s le lemme 3 4 9 nous avons VI Va A C Dom u Nous avons V1 Va A C VI a B A D apr s le lemme 3 4 9 nous avons VI a B A Dom o Ainsi VI Va A C Dom o d apr s le lemme 3 4 11 la formule Va A est a UTM Pour toute formule U d rivable dans P CP la formule A est o a a U UTM ainsi d apr s le lemme 3 4 10 pour toute formule U d rivable dans P CP le pr dicat A est o q a U UTM De m me le pr dicat B est o UTM dans P CP D apr s le lemme 3 4 7 o motive Va A dans P CP donc o motive Va Aa A a dans P CP gr ce la r gle ainsi le pr dicat Aa A est o UTM dans P CP Ainsi le pr dicat 1a A B est o UTM dans P CP Voici enfin le lemme principal celui qui montre que toutes les formules dans les d rivations des calculs P CP sont uniform ment trivialement motivables Proposition 3 4 19 Soit n un l ment de 2 w Pour tout jugement d rivable TH F et pour toute substitution u triviale adapt e F U F si VITU F Dom u alors TU F est u UTM dans P CP D monstration Soit u une substitution trivi
97. ables Proposition 4 4 2 Soient T un contexte t un terme et F un type Si le juge ment TH t F est d rivable alors il existe un terme u en forme normale tel que t g u et que le jugement T Hi u F soit d rivable D monstration Supposons que le jugement T Fip t F soit d rivable d apr s la proposition 4 3 2 le jugement T H t F est d rivable tous les termes typables dans AC admettent une forme normale donc il existe un A terme u tel que t 3 u et que le jugement H u F soit d rivable d apr s la proposition 4 3 2 le jugement I Fp u F est d rivable La normalisation des termes n est pas une propri t qui va de soi il existe des termes qui n admettent aucune forme normale comme par exemple Ax xx Ax xx qui se r duit n cessairement en lui m me mais qui n est pas en forme normale cependant ce terme n est pas typable tous les termes typables sont normalisables 108 Chapitre 5 A calcul p dagogique du second ordre 5 1 A calcul du second ordre Dans le calcul propositionnel minimal quand on cherche a prouver le th oreme A A on passe g n ralement par les tapes suivantes 1 AF par Hyp 2 Fn A par et 1 Le terme isomorphe cette preuve est la fonction identit Ar4 x sur les termes de type A On remarque qu on peut d montrer de m me n importe quel th or me de la forme a a dont la preuve correspond au A terme Axr x
98. absurdit L d finie par la formule Va a est autoris e appara tre dans les formules des d rivations tandis que le jugement Va l a nest pas d rivable Nous sommes alors tent s de penser que F CP n est pas un calcul dans lequel l absurdit est d finissable Nous allons voir ce qu il en est dans le cas des calculs d ordre sup rieur D finition 3 2 1 Pour tout n l ment de 2 w le calcul propositionnel faible ment p dagogique d ordre n abr g en F CP est d fini par sa morphologie constitu par l ensemble des jugements de la forme T F F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles gt e Vi Ve a et g ainsi que des deux r gles suivantes FR or Fer Ho Le calcul F CP est galement appel le calcul propositionnel faiblement p dago gique d ordre sup rieur On dit qu un jugement IT Ff F est d rivable quand il existe une d rivation dans F CP dont la derni re r gle utilis e produit ce jugement Dans les d rivations il convient de motiver les contextes introduits comme dans l exemple suivant Exemple d rivation du jugement H VG Va a Ba B Va a Ba 1 FY T par P Ax 2 a H Aa T a par P Ax et 1 3 H a gt Aa T a par et 2 4 F Va a Aa T a par V et 3 59 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup ri
99. ale adapt e FU F telle que VI T U F Dom y Montrons par r currence sur la d rivation de TF F que FU F est u UTM dans P CP He oT TET que p a T pour toute variable a Dom p Soit G T par hypoth se de r currence la formule o G est p UTM dans P CP d apr s le lemme 3 4 12 la formule G est Dom c UTM dans P CP d apr s le lemme 3 4 11 la formule G est u UTM dans P CP ainsi TU T est UTM dans P CP P Ax notons p la substitution dont le domaine est VI o l telle Fer Fol p i Bah DF P Hyp analogue au cas pr c dent Ta hypoth se de r les f les dans l U A B i T B i par hypoth se de r currence les formules dans FU A B sont u UTM dans P CP d apr s le lemme 3 4 7 la substitution u motive T dans P CP donc u motive la formule A B dans P CP d apr s le lemme 3 4 4 ainsi TU A B est u UTM dans P CP rH ce ce MESA r H B UTM dans P CP ae oo Vi soit U une formule d rivable dans P CP par hy poth se de r currence I U A est fn a U UTM dans P CP d apr s le gt e par hypoth se de r currence TU A B est u 81 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur lemme 3 4 7 la substitution u motive I dans P CP donc u motive la for mule Va A dans P CP d apr s le lemme 3 4 4 par cons quent Va A est u UTM dans P CP PE YAA En
100. ans Bxred Ar4 u u g x v u Aau A 3 a A u Bared Nous avons donc deux types d valuation des applications celle associ e aux A abstractions et celle associ e aux A abstractions Pour chacune d elles nous allons d montrer qu elles pr servent le typage des termes r duits Nous nous occu pons premi rement de l valuation associ e aux A abstractions Par une r currence imm diate sur les d rivations on observe que l application de la r gle Ared un A terme typ par le jugement T Ax t u F produit une d rivation du ju gement I H x ul t F il est construit partir de la d rivation du jugement T x AH t F dans laquelle toutes les occurrences de la r gle Hyp produisant un jugement T A x A H x A sont remplac es par la d rivation du jugement 116 5 3 Normalisation T A F u A On remarque qu il faut pouvoir affaiblir le contexte de F H u A par le contexte A ainsi pour que l on puisse typer les termes r duits par la r gle Ared il faut pouvoir affaiblir tous les contexte par A nous avons besoin de d river la r gle d affaiblissement p dagogique P Aff de la mani re suivante Pub Fio o U Tal A ted aon Notons que le A terme t reste le m me apr s affaiblissement Nous allons d montrer que cette r gle est d rivable dans P C Proposition 5 3 1 Soient IT un contexte U un type et x une A variable n ap paraissant pas dans I Pour tout
101. atiques devraient tre limit es celles bas es sur des constructions effectives si une telle construc tion est impossible alors la d finition n a pas de sens Malheureusement aussi bien chez Poincar que chez Griss les motivations philosophiques et scientifiques sont tr s peu d velopp es et semblent alors assez faibles Griss consid rait que les math matiques sans n gation pouvaient tre trait es comme un pur probl me math matique La pr sente th se constitue une introduction une cat gorie de syst mes for mels destin s rendre compte des desiderata de Poincar Nous proposons d ajou ter aux syst mes formels une contrainte que nous appelons contrainte p dagogique Le cadre d tude choisi est constitu des syst mes de d duction naturelle intro duits l origine par Gerhard Gentzen 11 et Dag Prawitz 35 de tels syst mes manipulent des jugements F F o T est un ensemble fini G 1 G de for mules et F une formule avec la signification intuitive que la formule F est valide sous les hypoth ses I Les syst mes de d duction naturelle ne proposent aucun outils pour manipuler des d finitions en substitut quand on souhaite introduire un objet x satisfaisant une d finition on postule dans le contexte I un ensemble de formules dans lesquelles appara t la variable x cet ensemble de formules d crivant les propri t s que doit poss der x pour satisfaire la d finition Nous observons que l
102. ax analogue au cas pr c dent A Ar Bes B AB AB Qapp Supposons que le pr dicat AB soit o UTM dans P CP Les pr dicats A et B sont o UTM dans P CP Par hypoth se de r currence les pr dicats A et B sont o UTM dans P CP Le jugement gt o A B est ais ment d rivable par la r gle a Ainsi le pr dicat A B est o UTM dans P CP L autre sens de l implication est analogue Le lemme suivant concerne le cas de la r gle p Lemme 3 4 18 Soient n un l ment de 2 w et o une substitution triviale dans P CP Pour tout pr dicat A et B si A g B et si tous les pr dicats motiv s dans la d rivation de A B par une substitution u sont u UTM alors A est o UTM dans P CP si et seulement si B est o UTM dans P CP D monstration Par r currence sur la d rivation de A B 79 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur Tr G ce cas est imm diat era Gar ce cas est imm diat A y A B B AD AD G_ supposons que la formule B soit o UTM y dans P CP Ainsi les formules A et B sont o UTM dans P CP Par hy poth se de r currence les formules A et B sont o UTM dans P CP Le jugement H o A B est ais ment d rivable par la r gle Ainsi la formule A B est o UTM dans P CP L autre sens de l implication est analogue A g A Var ALNA Gy supposons que la
103. ce chapitre les jugements propositionnels du second ordre sont appel s jugements quand cela ne pr te pas confusion Le contexte vide est repr sent par le mot vide ainsi pour tout A terme t pour tout type F et tout identifiant id le jugement 0 2 t F s crit galement 2 t F De plus pour tous contextes I et A le contexte TUA est not I A En particulier pour tout type le jugement F U A H2 t F est not T A t F Dans les types le nom des variables quantifi es ne sert qu les distinguer des autres variables puisqu elle repr sente potentiellement n importe quel type deux type ne diff rant que par le nom de leur variables libres ont la meme signification ceci est formalis par la relation d a quivalence D finition 5 1 16 Pour tout type A et B la relation d a quivalence entre A et B not e A B est d finie par les r gles suivantes er 0 wage Pr A A B 8B A B A B a a y A a 6 7 B y Fr A B CS Ya A VB B Quand la relation A B est v rifi e on dit que les termes A et B sont a quivalents Nous avons enfin tous les outils n cessaire la d finition du A calcul du second ordre D finition 5 1 17 Le calcul du second ordre abr g en C est d fini par sa morphologie constitu par l ensemble des jugements de la forme TH t Ee 113 CHAPITRE 5 A calcul p dagogique du second ordre sa syntaxe
104. culs propositionnels p dagogiques du premier ordre Fert tol T F P Hyp On dit qu un jugement IT F F est d rivable quand il existe une d rivation dans N CPM dont la derni re r gle utilis e produit ce jugement N CPM permet d j de construire des d rivations de th or mes bien connus tels que F a a 2 5 dont la d rivation dans CPM a t donn e dans la section pr c dente Exemple d rivation du jugement H a a 6 b 1 F T par N Ax TH T par P Hyp et 1 3 F T T par 4 et 2 4 a a F amp par P Hyp 1 et 3 5 a a gt Gk a par P Hyp et 1 6 a a gt Bk 8 par 4et 5 8 F a a B gt 6 par et 7 Les syst mes p dagogiques induisent des objets propres la notion d exemple Les motivations sont des objets satisfaisant une d finition des exemples la moti vant Dans CPM et N CPM cette notion est formalis e comme suit D finition 1 2 3 Soit C un calcul dont la morphologie est constitu par l ensemble des jugements de la forme TH F Pour tout contexte A une motivation de A dans C est une substitution o telle que les jugements a A soient d rivables Quand un contexte admet une motivation dans C on dit qu il est motivable De plus une motivation d une formule F dans C est une motivation du singleton F dans C Pour toute formule F on note Fr la formule F dans laquelle toutes les variables propositio
105. d la conjonction des formules de est fausse quel que soit l instanciation de ses variables libres De m me le jugement l E F est syntaxiquement nul quand le contexte I n est pas motivable Nous allons d montrer que dans F CP tous les jugements apparaissant dans les d rivations sont non nuls D finissons d abord formellement la non nullit des jugements D finition 2 2 3 Soit C un calcul dont la morphologie est constitu par l ensemble 23 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre des jugements de la forme T H F Un jugement T 2 F est syntaxiquement non nul quand son contexte I est motivable dans C On prouve maintenant la non nullit des jugements d rivables dans F CP Lemme 2 2 2 Pour tout jugement T F d rivable le conterte T est motivable dans F CP D monstration Par r currence sur la d rivation de T F les cas des r gles Vi Ve et a tant analogues H oT Ter Fer HoT TES T AH B rH A gt B tivable dans F CP donc I est motivable dans F CP r A gt B THA r B motivable P Ax est une motivation de I dans F CP P Hyp cas analogue P Ax par hypoth se de r currence le contexte I U A est mo par hypoth se de r currence le contexte I est La non nullit d un jugement I H F ne concerne que le contexte I mais on peut montrer que la motivation de I constitue par d
106. dans P Ve P CP dont la derni re r gle utilis e produit ce jugement 2 3 2 Non nullit syntaxique des implications Dans F CP tous les jugements sont syntaxiquement non nuls Nous allons montrer que dans P CP toutes les implications sont syntaxiquement non nulles Formellement on d finit la non nullit des implications comme suit 31 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre D finition 2 3 2 Soit C un calcul dont la morphologie est constitu e par l en semble des jugements de la forme T H F Une implication A B est syntaxi quement non nulle quand la formule A est motivable dans C Nous allons en fait prouver un r sultat plus fort que la non nullit syntaxique des implications la motivabilit de toutes les sous formules des formules apparaissant dans une d rivation de P CP Toutes ces sous formules sont de plus motivables par la m me motivation c est dire qu il existe des motivations qui motivent toutes les formules motivables il s agit des motivations triviales et les formules sont alors dites h r ditairement trivialement motivables D finition 2 3 3 Soit C un calcul dont la morphologie est constitu par l ensemble des jugements de la forme T F F une substitution o est triviale dans C quand le jugement F o a est d rivable pour toute variable a Dom o un contexte T est trivialement motivable TM dans C quand T est motivable par une subs
107. doit n cessairement porter sur quelque objet concret inversement de toute propri t concr te on peut extraire des propri t s abstraites xviii valables dans des classes d objet plus vastes En g nie logiciel les syst mes formels sont utilis s pour garantir que les pro grammes d velopp s sont exempts d erreurs On r dige une sp cification formelle compos e de formules correspondant au cahier des charges du programme parmi ces formules certaines d crivent l environnement d ex cution et d autres corres pondent des invariants des formules devant toujours tre v rifi es quel que soit l tat d ex cution du programme On construit alors le programme pas pas l aide d outils garantissant que pour tout environnement d crit par la sp cification le programme respecte les invariants On distingue plusieurs types de propri t s parmi lesquels on compte la s ret la coh rence et la vivacit Un programme est s r quand il v rifie les invariants qui lui sont associ s La coh rence concerne les sp cifications comme suit on souhaite que toute sp cification admette un envi ronnement la respectant En effet quand une sp cification est incoh rente elle permet de valider n importe quel invariant un programme quelconque est alors jug s r bien qu il soit inutilisable en pratique faute d un environnement ad quat Un tel programme issu d une sp cification inadapt e au dispositif qu elle e
108. duction une motivation de Bs Lemme 2 2 3 Pour tout jugement T H F d rivable et pour toute substitution o adapt e T si les jugements o T sont d rivables alors le jugement o F est d rivable D monstration Posons I F Fa et Dom o a1 a Nous d rivons le jugement Fi F F par applications successives de la r gle Puis nous d rivons le jugement Vas Vas gt gt Fa F par applications successives de la r gle V Puis nous d rivons le jugement o F gt oF o F par applications successives de la r gle Ve Enfin nous d rivons le jugement o F par applications successives de la r gle Ainsi tout jugement I H F d rivable en plus de sa non nullit admet une pro pri t plus forte les formules dans I ainsi que F sont motivables par la m me motivation Proposition 2 2 4 Pour tout jugement F d rivable l ensemble TU F est motivable dans F CP En particulier T F est syntaxiquement non nul D monstration D apr s le lemme 2 2 2 le contexte I est motivable dans F CP et donc d apr s le lemme 2 2 3 la formule F est motivable dans F CP 24 2 2 Calcul propositionnel du second ordre faiblement p dagogique 2 2 3 La r gle d affaiblissement Dans le calcul F CP la r gle usuelle d affaiblissement TH F s Aff T U H F G n est plus d rivable car la formule U ajout e au contexte
109. e y F x A nous d rivons le jugement T me y F l aide de la r gle P Hyp LGAs Boe OO DA Ay f BOC est d rivable et d apr s la proposition 5 2 1 le type B est motivable dans P C ainsi nous d rivons le jugement T y B ee u l aide de la r gle P Aff par hypoth se de r currence le jugement F y B ES RATES f C est d rivable nous d rivons alors le jugement T y B Eag z u Ay fs F avec la r gle T z AH f B gt F T z A g B Tre A fo F awe r currence les jugements I 4 x u f B gt F et TH x u 9 B sont d rivables donc nous d rivons le jugement T H r u fg F avec la r gle e T x AFi ae a amp VI T a A x ES Aa f Ya B gement T Fip x u f B est d rivable par a quivalence nous pouvons supposer que n apparait pas dans u ainsi nous d rivons le jugement I H uj Aa f F avec la r gle Vj r r AHi evo Hip oU T z A ae fU a U B gement P 4 x u f Ya B est d rivable nous d rivons alors le jugement TH z u fU F avec la r gle P Ve Pg ARG G aF DRAP D4 x uft G est d rivable ainsi nous d rivons le jugement I 4 r u F avec la r gle a i par hypoth se le jugement Ty u A hypoth se de Vi par hypoth se de r currence le ju P V par hypoth se de r currence le ju a par hypoth se de r currence le jugement L application de
110. e ainsi le jugement I Hp Aa0 0 A x Aa A est d rivable laide du lemme 3 5 4 le jugement r Fp da 0 a 9 a A Aa A est d rivable par la r gle Ext le jugement T H5 a O a A p Aa A O est ais ment d rivable ainsi le jugement T F Aa A Aa A est d rivable par la r gle p nous avons alors une d rivation du jugement I F5 6 p x Py P AB soit gt x le genre du pr dicat A nous avons AB A B et 0 AB 0 A B par hypoth se de r currence le jugement rT F O A Ay est d rivable d apr s le lemme 3 5 2 le pr dicat B est motivable ainsi le jugement I H5 0 A B A B est motivable comme 0 A Aa 0 A 0 a nous avons une d rivation du jugement FS Aa 0 A 0 By AB le jugement FF Aa 0 A O a B g 90 A 0 B est ais ment d rivable ainsi le jugement FS 0 A 0 B A B est d rivable l aide de la r gle p par 2 88 3 5 Traductions hypoth se de r currence le jugement T F B By est d rivable ainsi le jugement I F5 8 4 B A B est d rivable l aide de la r gle Ext nous avons alors une d rivation du jugement I H p Py Pour que les substitutions se comportent bien apr s traduction il est n cessaire que la y traduction et l application de substitution commutent Lemme 3 5 6 Soit n un l ment de 2 w Soient P k et U deux pr d
111. e de sens une notion quivalente la coh rence Or on a observ dans le cas des s mantiques bas es sur les mod les que la coh rence d un syst me donn chappe in vitablement ce syst me On se retrouve de nouveau tenter justifier une formule dans un syst me par une formule de m me nature dans le m ta syst me elle m me fond e par une formule analogue dans un m ta m ta syst me etc selon un principe mal fond demandant une r gression le long d une suite infinie de syst mes de plus en plus puissants et donc a priori de plus en plus douteux Le comportement relatif aux programmes d crits par L qui n est pas cens exister mais ceci ne saurait tre ontologiquement pertinent est enti rement r sum dans la r gle du ex falso dont voici l nonc de l absurde on peut d duire toutes les formules Quand cette r gle fait partie des r gles de base du syst me formel rien ne nous permet de comprendre sa raison d tre mais quand elle est d rivable partir des autres r gles comme dans la logique propositionnelle du second ordre ou l arithm tique on dispose d un moyen d investigation en tudiant sa d monstration qui se r v le d une grande pauvret dans la logique propo sitionnelle du second ordre la fonction associ e la r gle du ex falso est l identit qui plus est une fonction dont le domaine est vide Rien n est dit sur le programme associ L rien sur sa structure
112. e des calculs p dagogiques Notons que la n gation est galement d finissable dans CP mais on ne peut pas l exprimer dans le calcul P CP cause de la non nullit syntaxique des implications apparaissant dans les d rivations Dans F CP la situation est plus complexe car nous ignorons si oui ou non une formule absurde y est d finissable consid rant la d finition usuelle de l absurde l aide le la formule Va a la proposition 2 2 13 nous permet de r pondre par la n gative dans ce cas particulier 2 4 1 Conjonction Nous allons prouver que les r gles d introduction et d liminations de la con jonction restent les m mes dans F CP et P CP D finition 2 4 1 La conjonction A A B des formules A et B est d finie par la formule Vy A B y y dans laquelle est une variable fra che pour A et B R gle d introduction Dans le cas de F CP la r gle d introduction de la conjonction est d rivable THA THB THF AAB Proposition 2 4 1 La r gle Ai est valide dans F CP D monstration Supposons que les jugements I A et T H B soient d rivables l aide de la proposition 2 2 4 le contexte I U A B est motivable dans F CP 1 T A BH T par P Ax 2 T A4 B A gt B T par et 1 3 T A B A Boyt A B y par P Hyp et 2 4 T A B A B q F A par P Hyp 5 T A B A gt Boyt Boy par gt e 3 et 4 6 T A B A B 7y t B par P Hyp 7
113. e g on remarque que V repr sente un ensemble non vide quel que soit le type Au final la traduction de la formule intuitionniste A est la formule 27 T Vz A y Vz gt z r Y 0 d montrable dans le syst me sans n gation de Mezhlumbekova Ce r sultat tr s technique a le m rite de mettre en vidence l expressivit des syst mes sans n gation il est toujours possible de traduire un th or me arithm tique usuel en un th or me quivalent sans n gation dont malheureusement la pertinence est quelque peu noy e dans un arsenal technique assez peu intuitif Dans un travail plus r cent 28 Mezhlumbekova propose un calcul des pr dicats du premier ordre sans n gation dans lequel ni l implication ni la disjonction ne sont quantifi es Cependant elle introduit un nouveau quantificateur logique unaire qu elle nomme la signifiance meaningfulness en anglais en particulier la cl ture existentielle d une formule A est d montrable d s que la formule A l est Ainsi la notion de signifiance permet d internaliser et de pr ciser la notion de non nullit d finie par Nelson L ensemble des r gles de d duction est malgr tout alourdi par les r gles structurelles r gissant le comportement de la signifiance ce que l on gagne en supprimant les implications et les disjonctions quantifi es on le perd par l ajout de la signifiance Motivations On peut supposer qu l origine la logique a
114. e l arithm tique intuitionniste peut tre plong e dans son arithm tique sans n gation au prix d une interpr tation dialectica des formules arithm tiques chaque formule intuitionniste est transform e en une formule 7Vy d dans laquelle est une formule sans quantificateurs Cette for mule est alors interpr t e sous la forme d une galit f 0 dans laquelle f est une fonctionnelle de type entier les fonctionnelles sont limin es en utilisant le pr dicat T de Kleene 22 on commence par coder les fonctionnelles t et u par des entiers t et Hu l application d une fonctionnelle t une fonctionnelle u est alors codable sous la forme d une galit T t u y 0 avec T t u y un terme r cursif primitif gal 0 si et seulement si l entier y code un calcul terminant de Vapplication de t u le r sultat du calcul tant codable par un terme r cursif primitif U y L application d une fonctionnelle t une fonctionnelle u dans une formule A est ensuite cod e par la formule Ay T t u y A A t u U y avec xiii Pr sentation synth tique A t u U y d notant la formule A dans laquelle les applications t u de t u sont remplac es par le terme U y En it rant ces transformations on obtient une formule 27Vy r t y 0 avec r T y un terme r cursif primitif Mezhlumbekova d finit alors pour chaque type o une formule a V signifiant que a est le code d une fonctionnelle de typ
115. e nous ap pelons formules dans ce chapitre en l absence d ambiguit sont les pr dicats de genre x Selon la complexit des genres des pr dicats ceux ci seront plus ou moins expres sifs cette expressivit est repr sent e par l ordre des pr dicats plus l ordre est grand plus le pr dicat est capable d exprimer des propri t s d un haut niveau d abstraction en particulier l ordre des arguments pouvant tre pass s en argu ment un pr dicat est toujours strictement inf rieur l ordre de ce pr dicat la notion d ordre d pend donc essentiellement des genres D finition 3 1 4 Pour tout genre k l ordre Ord x de k est un entier d fini par r currence sur K eae Ord k 2 K t gt 0 Ord K max Ord v 1 Ord 6 Nous crivons N le compactifi de l ensemble N Pour tout couple m n N nous crivons m n l ensemble i N m lt i et i lt n c est dire l intervalle des l ments de N compris entre m et n Une fois qu un ordre est associ a chaque genre on peut d finir ce qu est l ordre d un pr dicat 54 3 1 Rappel sur les calculs propositionnels d ordre sup rieur D finition 3 1 5 Pour tout pr dicat P et pour tout n l ment de 2 w le pr dicat P est dit d ordre n si l ordre de tous les genres des sous pr dicats de P est inf rieur an Comme toujours dans les calculs hypoth tico d ductifs la Gentzen Prawitz nous avo
116. e plus U tT a T A par hypoth se de r currence ainsi U t F Puis on g n ralise l utilit des termes clos celle des termes quelconques Proposition 5 4 6 Pour tout jugement d rivable T ae t F le terme t est utile dans P C D monstration Le terme AQ AT t est clos donc U AG XT Var F d apr s le lemme 5 4 5 ainsi le terme t est utile dans P AC 123 CHAPITRE 5 calcul p dagogique du second ordre 5 5 Traduction CPS Les traductions CPS Continuations Passing Style constituent une technique de compilation utilis e pour simplifier la compilation des langages de programma tion fonctionnels 1 Au niveau des types les traductions CPS correspondent des interpr tations de la logique classique dans la logique intuitionniste fond es sur les traductions n gatives de G del Kolmogorov ou Kuroda Nous allons adapter la y traduction tudi e dans le chapitre 2 pour plonger AC dans P C en nous ins pirant de la traduction n gative de Kolmogorov 24 telle qu elle est utilis e dans le travail de De Groote 9 D finition 5 5 1 Soit F un type et y une variable fraiche pour F Nous d finis sons la y traduction FT du type F par r currence sur F PEUT Ve Ta F a F a F A gt B F A B F Va A FY Ya A Nous d finissons le type F par l unique type tel que FY F gt et nous crivons FY le type F Pour que les termes
117. e s par ment supposons que A gt B Nf par d finition nous avons A M et B Ni donc par hypoth se de r currence nous avons Ne et B N ainsi A B gN supposons que A B N par d finition nous avons A Net B Z N donc par hypoth se de r currence nous avons A M et B M ainsi A BEN L ensemble A est con u pour qu il h rite de certaines propri t s des formules r futables en particulier dans tout syst me coh rent si on peut d river une for mule r futable F sous les hypoth ses I alors I contient une formule r futable Lemme 1 2 6 Pour tout jugement TH F d rivable si F Ng et T 4 alors l ensemble TON est habit i e non vide D monstration Par r currence sur la d rivation de TH F N Ax par hypoth se nous avons I 0 ce qui est absurde FT F oT PE a E T 2 P Hyp par hypoth se nous avons F T et F M donc FETrTAM r At B 11 DE D par d finition de F M nous avons A M et B N par hypoth se de r currence l ensemble T U A AM est habit donc deux cas se pr sentent Ne d apr s le lemme 1 2 5 nous avons N mais nous avons A E N par d finition de F M ce qui est absurde TAN est habit ce cas est imm diat DEA TRA deux cas se pr sentent rH B A NF par hypoth se de r currence sur F A l en
118. e vue une remarque de Heyting dans 20 est frappante il y affirme que sans n gation il n y aurait aucun calcul propositionnel parce que dans ce cas seules les propositions vraies ont un sens A ce niveau de notre tude nous pouvons affirmer que d une part seules le propositions vraies cr ent du sens car les formules p dagogiques sont h r ditairement trivialement motivables et que d autre part la pr sente these n existerait pas si il n y avait aucun calcul propositionnel sans n gation nous pen sons avoir combl un manque dans ce domaine La suite naturelle de notre travail rejoint les pr occupations des autres chercheurs car elle concerne la p dagogisation des calculs des pr dicats et de leurs syst mes fonctionnels associ s La plupart des outils n cessaires ont t d velopp s et utilis s dans les syst mes propositionnels en particulier la notion de formule uniform ment motivable est primordiale dans l tude des calculs des pr dicats p dagogiques 130 Bibliographie 12 A W Appel Compiling with Continuations Cambridge University Press 1992 H P Barendregt Lambda Calculi with Types Handbook of Logic in Com puter Science Vol 2 1992 A Church A set of postulates for the foundation of logic Annals of Mathe matics Ser 2 Vol 33 1932 pp 346 366 A Church A formulation of the simple theory of types Journal of Symbolic Logic Vol 5 19
119. ee T A 4A Normalisation aiie ya nd a tas 2 a Se ete CS NS A A calcul p dagogique du second ordre 5 1 A calcul du second ordre in NT nn de D ae ge ed 5 2 A calcul p dagogique du second ordre Dis Normalisation s S94 Nan be RNA ees athe SY a the Se Rs M Se AE LP D te Ea Mae yea Rd Oe 5 5 Trad ction CGPS inip oon ee a ern eh Boe ee Ee Be i Conclusion Bibliographie iv 101 101 104 106 107 109 109 114 116 120 124 129 131 Remerciements Tout d abord je remercie mon directeur de these Loic Colson qui m a encadr tout le long de ma formation universitaire du DEUG au doctorat Son soutien ind fectible sa bonne humeur et ses encouragements m ont permis de travailler dans les meilleures conditions J exprime toute ma gratitude a Patrick C gielski et Gilles Dowek d avoir rap port cette th se et pour le temps qu ils ont consacr l analyse de ce document Je tiens remercier Serge Grigorieff d avoir accept de pr sider mon jury de soutenance ainsi que pour ses encouragements et son soutien Je remercie galement Maurice Margenstern pour avoir accept de faire partie du jury de cette th se Ma reconnaissance s adresse tous les enseignants techniciens et personnels administratifs qui m ont accueilli au LITA pendant quatre ans Je pense en parti culier mes amis doctorants Mathieu Thomas Micha l et Mihaela sans oublier les stagiaires que j ai c toy s
120. er la s mantique dans un syst me plus puissant mais aucun n chappe l existence de formules ind cidables quelle que soit la puissance de la logique utilis e pour tudier la s mantique il y a toujours des formules dont la valeur de v rit reste ind termin e Cependant quand le tiers exclu est une r gle valide du m ta syst me ce dernier servant de canon le tiers exclu au niveau du syst me est alors justifi de mani re ad hoc On se retrouve face une contradiction ontologique bien que cette construction logique soit formellement coh rente Il convient de mentionner le statut de la coh rence formelle car elle n est pas exempte des probl mes mentionn s ci dessus en effet la coh rence formelle quand est est exprim e dans un syst me formel suppos coh rent s exprime sous la forme d une formule ind cidable on ne peut justifier la coh rence d un syst me que par la coh rence du m ta syst me sa coh rence tant elle m me justifi e par un m ta m ta syst me Pire un syst me formel coh rent peut tr s bien affirmer l incoh rence d un de ses sous syst mes de m me qu un syst me incoh rent peut tr s bien affirmer la coh rence d un de ses sous syst mes On a le sentiment d avoir affaire une s mantique b tie sur du sable Face aux paradoxes que g n rent les s mantiques bas es sur les mod les on rencontre plusieurs attitudes certains jugent que la coh rence formelle es
121. es variables ont t remplac es par T De m me pour tout A terme t on note t le terme t dans lequel tous les types A y apparaissant sont remplac s par Ay Pour tout contexte I on note l ensemble des couples x Fr tels que x F T Dans P CPM toutes les formules sont motivables de m me dans P AC tous les types admettent une instance typant un terme Lemme 4 3 1 Pour tout type F il existe un A terme t tel que le jugement Fip t Fr soit d rivable D monstration Par r currence sur F F T nous avons T7 T ainsi le jugement Ei o Fr est d rivable par la r gle P Ax F a nous avons ar T et on conclut comme dans le cas pr c dent F A B nous avons Fy At gt Br 1 GS u Ar par hypoth se de r currence 2 Fip v Br par hypoth se de r currence 3 x B7 y T Fip x By par P Hyp 1 et 2 4 x Bry y Ar Br par et 3 5 Fip AxPT y 2 Br At Br par et 4 6 Fip Az t Ay4t 2 u Ar Br par 5 et 2 ainsi il existe un A terme t tel que le jugement Hip t A Bjr soit d rivable Ce r sultat a pour cons quence l quivalence de la typabilit dans AC et P AC Proposition 4 3 2 Soient L un contexte t un A terme et F un type Le jugement TH t F est d rivable si et seulement si le jugement T Fip t F est d rivable D monstration Nous d montrons successivement les deux sens de l quivalence
122. eti lt n le jugement H5 VBR o a est d rivable l aide de la r gle V ainsi comme pu est une substitution triviale le jugement Fp u c a est d rivable l aide de la r gle P Ve Dom u Dom o nous avons 4 c a u amp comme y est une substitution triviale le jugement F5 u g a est d rivable Il est important de pouvoir compl ter les motivations ouvertes et des motivations closes La proposition suivante garantit que c est toujours le cas pour les motiva tions triviales Proposition 3 4 2 Soient n un l ment de 2 w et F une formule motivable dans P CP par la substitution o Pour toute substitution u triviale dans P CP la substitution est une motivation de F dans P CP D monstration Par hypoth se le jugement F oF est d rivable Posons Dom y BF 1 lt ieti lt n l aide de la r gle Vi nous d rivons le jugement FF VBR OF ainsi l aide de la r gle P V nous d rivons le jugement Ff u o F De m me que dans les calculs F CP la r gle d affaiblissement faiblement p dago gique F Aff est valide dans les calculs P CP Lemme 3 4 3 Soit n un l ment de 2 w Pour tout jugement T Hp F d rivable et pour toute formule U telle que 1 U U soit motivable dans P CP le jugement T U F F est d rivable 71 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur D monstration Analogue
123. eur 5 Va a Ba FY Va a Ba par P Hyp et 4 6 Va a Ba FP Va a Ba B Va a Ba par Ve et 5 Va a Ba FP f B Va a Ba par gt e 5 et 6 FF Va a gt Ba Va a Ba par gt i et 7 He VBPX Vat a Ba B Va a Ba par Vi et 8 Bien que la notion de motivation soit bien d finie dans le cas des formules elle ne l est pas encore dans le cas g n ral des pr dicats Pour l instant nous ne dis posons pas des r sultats n cessaires pour justifier le choix d une d finition de la motivabilit des pr dicats la d finition suivante est donn e par anticipation car nous en avons besoin dans certaines preuves nous justifierons plus tard le fait que la motivation d un pr dicat P corresponde la motivation de la formule P D finition 3 2 2 Pour tout genre k et pour tout pr dicat P k la formule P est d finie par r currence sur k k k P P K t gt 60 P Va Pa Si A P P est un ensemble de pr dicats alors A d note l ensemble Pig eds Les calculs d ordre sup rieur font beaucoup appel aux applications de substitu tions ne serait ce qu cause de la r gle Ve la preuve que l application des sub stitutions commute avec la transformation P constitue une propri t technique incontournable Lemme 3 2 1 Soit o une substitution Pour tout pr dicat P k nous avons o P a P D monstration Par r cu
124. f A B a B A Brea uand la relation P est v rifi e on dit que les pr dicats P et Q sont p B quivalents Apr s toutes ces d finitions nous pouvons maintenant d finir les calculs proposi tionnels d ordre sup rieur D finition 3 1 15 Pour tout n l ment de 2 w le calcul propositionnel d ordre n abr g en CP est d fini par sa morphologie constitu par l ensemble des jugements de la forme T F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles suivantes A rer M9 pre Fr Hyp DASE ps rreASB TPA reA gt B TFB THA og VIT TH Var A Diva Wi Pr ropa Vo TFA A B F Oon B a THA A B TB 3 2 Calculs propositionnels faiblement p dagogiques d ordre sup rieur Le calcul CP est galement appel le calcul propositionnel d ordre sup rieur On dit qu un jugement T H F est d rivable quand il existe une d rivation dans CP dont la derni re r gle utilis e produit ce jugement 3 2 Calculs propositionnels faiblement p dago giques d ordre sup rieur 3 2 1 Pr sentation des calculs Nous allons reprendre notre premi re m thode de p dagogisation introduite dans le chapitre 1 afin de l appliquer au calcul CP Dans le chapitre 2 nous avons utilis cette m thode pour p dagogiser le calcul CP et nous avons obtenu le calcul F CP dans lequel l
125. genre x 93 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur sta est une variable propositionnelle de genre k et A un pr dicat de genre x alors Va A est un pr dicat de genre x sta est une variable propositionnelle de genre k et A un pr dicat de genre L alors a A est un pr dicat de genre kK gt 1 si A est un pr dicat de genre k et B un pr dicat de genre k alors AB est un pr dicat de genre t Pour tout pr dicat P et tout genre la notation P k signifie que le pr dicat P est de genre x Toute variable propositionnelle a pourra tre not e a en l absence d ambiguit sur son genre Afin d all ger l criture des pr dicats nous crivons A B C les pr dicats de la forme A B C et Va A B les pr dicats de la forme Va A B De m me nous crivons ABC les pr dicats de la forme A BC et Aa AB les pr dicats de la forme Va AB Les pr dicats de la forme AB ont la pr c dence la plus forte le pr dicat AB C d note le pr dicat AB gt C Les pr dicats de la forme Aa Aak P sont not s XP et quand n 0 cette notation repr sente le pr dicat P Les pr dicats de la forme PQ Q sont not s PQ et quand n 0 cette notation repr sente le pr dicat P On remarque que les formules sont des pr dicats particuliers ne portant sur aucun objet D finition 3 1 3 Les formules propositionnelles d ordre sup rieur qu
126. icats Soient y une variable fra che pour P et U et a une variable diff rente de y Le jugement FF a U P a U P est d rivable D monstration Notons y la substitution a UT et u la substitution a U Nous prouvons le lemme par r currence sur P P T nous avons u T T et wT T de plus le jugement F T T est d rivable ainsi le jugement Hp u P uP est d rivable P ff deux cas sont consid rer B a nous avons uyay O U et ua U d apr s le lemme 3 5 5 le jugement H U U est d rivable ainsi le jugement F5 u P uP est d rivable B a nous avons u B p et uB b d apr s le lemme 3 5 2 le pr dicat est motivable ainsi le jugement F5 6 3 est ais ment d rivable donc le jugement F5 Hy Py x uP est d rivable P A B le jugement I H u A gt B u A B est ais ment d rivable nous avons u A B u A u B donc nous avons une d rivation du jugement T FP u A gt u B w A gt B par hypoth se de r currence les jugements T FP uy Ay uA et CFP u By u B sont d rivables ainsi le jugement T F uy Ay gt By u A B est d rivable l aide de la r gle Ext nous avons uy A gt B yA gt uyB ainsi nous avons une d rivation du jugement DEP m A gt B u A gt B nous avons alors une d rivation du jugement FP
127. insi que des deux r gles suivantes PER Ver an n K P Ve PER a U A r A A g B pe TF B e Le calcul PC CP est galement appel le calcul propositionnel p dagogique con traint d ordre sup rieur On dit qu un jugement IT Fp F est d rivable quand il existe une d rivation dans PC CP dont la derni re r gle utilis e produit ce juge ment 3 3 2 Non nullit s mantique des implications Les calculs PC CP satisfont la propri t de non nullit des implications en particulier pour tout sous pr dicat P des formules apparaissant dans les d riva tions la formule P est instanciable en une formule vraie au sens de la s mantique bool enne a deux valeurs de v rit Proposition 3 3 2 Soit n un l ment de 2 w Pour tout jugement TE F d rivable et pour tout sous formule G d une formule de T U F il existe une substitution o telle que la formule o G soit vraie dans la s mantique bool enne D monstration Afin de prouver la pr sente proposition nous avons besoin du syst me P CP d fini dans la section suivante En effet d apr s la proposition 3 4 20 il existe une substitution telle que la formule o G soit close et d montrable dans le calcul P CP Le calcul P CP est une extension consistante du calcul PC CP dans la s mantique bool enne donc la formule o G est vraie dans la s mantique bool enne 3 3 3 Certaines implications sont syntaxiquement nulles
128. ion nulle une implication A B est dite nulle si la formule A est fausse pour toute instance Puis il d veloppa une logique des pr dicats du premier ordre dans laquelle toutes les implications sont non nulles pour cela il fut contraint de remplacer l implication usuelle B par une nouvelle notion d implication A B dans laquelle 7 d note une liste de variables X1 m quantifi es Une telle implication quantifi e poss de une traduction dans les syst mes usuels par la formule 27 4 A Vz A B Nelson d finit alors toute une collections de r gles plus ou moins intuitives plus ou moins compliqu es afin xii de garantir pour chaque formule A apparaissant dans une implication quantifi e A z B que la formule 4 A est d montrable De m me il remplace la disjonction usuelle A V V A par une disjonction quantifi e 0 A A En plus de ces nouveaux connecteurs logiques il subsiste dans ce syst me quelques points d licats comme la pr sence d un principe de contradiction affaiblie que Nelson juge la limite de la respectabilit pour un raisonnement sans n gation Dans la continuit du travail de Nelson Victor Krivtsov enrichit le syst me formel sans n gation existant en une arithm tique simple 25 puis en une arithm tique d ordre sup rieur 26 Il conserve les implications quantifi es mais laisse en suspend les disjonctions quantifi es jug es techniquement trop pesantes Il u
129. it que le contexte introduit soit seulement motivable pour obtenir une r gle plus en ad quation avec les autres On d cide alors de remplacer la r gle N Ax par la r gle P Ax ol afin d obtenir un syst me p dagogique ayant de bonnes propri t s D finition 1 2 5 Le calcul propositionnel p dagogique minimal abr g en P CPM est d fini par sa morphologie constitu par l ensemble des jugements de la forme I F F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles P Hyp gt i et gt e ainsi que de la r gle suivante F or On dit qu un jugement DF F est d rivable quand il existe une d rivation dans P CPM dont la derni re r gle utilis e produit ce jugement Nous allons tout de suite v rifier que le jugement T gt TF T est d rivable afin de se rendre compte que le nouveau syst me est plus expressif que l ancien Exemple d rivation du jugement T gt TF T 1 H T par P Ax 2 TH par P Hyp et 1 3 F TT par gt i et 2 4 T TF T par P Ax et 3 10 1 3 propos de la n gation De plus puisque N CPM est une restriction de P CPM toutes les formules sont motivables dans P CPM il suffit pour chaque formule de mener dans P CPM la preuve qu elle est motivable dans N CPM Il reste v rifier que tout jugement d rivable dans CPM est galement d rivable dans P CPM Proposition 1 2
130. ithmique peut toujours tre utilis pour manipuler leur param tre Ainsi l utilit est le pendant fonctionnel de la contrainte p dagogique Le calcul propositionnel minimal pose assez peu de probl mes parce que d une part l absurdit y est d finie de mani re ad hoc et d autre part il est d cidable La confrontation de la contrainte p dagogique avec un calcul ind cidable dans le quel l absurde est naturellement d finissable constitue un passage obligatoire afin de juger sa robustesse c est pourquoi la p dagogisation du calcul propositionnel du second ordre s impose naturellement L absurde y est d finissable par la for mule Va a que nous notons alors Dans un premier temps il convient d tudier le syst me dans lequel on se contente d introduire les r gles P Ax et P Hyp comme cela t fait avec le calcul minimal Le syst me obtenu est appel le calcul propositionnel du second ordre faiblement p dagogique il est dit faible car il est possible d y d montrer des th or me contenant la formule L comme par exemple L L Cependant la formule ne poss de pas les propri t s usuelle de l absurde tout d abord la r gle L n est pas d rivable dans le calcul p dagogique ensuite la formule Va a n est pas un th or me du calcul p dagogique Ainsi la for mule se comporte comme une constante propositionnelle neutre dans tous les th or mes elle peut tre remplac e par
131. itution T la r gle d affaiblissement faiblement p dagogique peut tre grandement simplifi e dans P CP par cons quent la r gle d affaiblissement p dagogique P AfF PE eo TURF P Af est d rivable dans P CP Il nous semble important de remarquer que le calcul P CP capture toutes les propri t s d montrables usuellement dans le calcul usuel CP m me si la preuve du r sultat n est pas d une grande profondeur en effet la notion de formule mo tivable est destin e constituer la bonne notion de formules dans les syst mes p dagogiques puisque les formules non motivables sont totalement absentes de toute d rivation Proposition 2 3 11 Pour toute formule close F HTM dans P CP le jugement F est d rivable si et seulement si le jugement F est d rivable D monstration la formule F est close et HTM dans P CP donc Ee F est d rivable lt sit F est d rivable alors H F est d rivable 2 4 D finition des connecteurs logiques Dans CP en tant que calcul du second ordre la conjonction a disjonction et l existence sont d finissables 35 Il en est de m me dans F CP mais dans P CP 37 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre les r gles r gissant la disjonction sont alt r es par la contrainte p dagogiques Nous allons exposer cela en d tail pour chaque connecteur logique en reprenant leur d finition usuelle dans le cadr
132. ivable D monstration Par r currence sur la d rivation de P g Q ei Gr nous avons P Q car T T les pr dicats P et Q sont motivables dans P CP d apr s le lemme 3 5 2 ainsi nous d rivons T F5 Py Q l aide du lemme 3 5 9 ar Bvar la relation g est r flexive donc nous avons a a les p Q aes P et Q sont motivables dans P CP d apr s le lemme 3 5 2 ainsi nous d rivons l E Py l aide du lemme 3 5 9 A p A B Bh B B p A B A et B B nous avons alors A B g A B par la r gle G_ nous avons P Q les pr dicats P et Q sont motivables dans P CP d apr s le lemme 3 5 2 ainsi nous d rivons I F Py Q l aide du lemme 3 5 9 A Va A g Yat A nous avons alors Va A g Ya A par la r gle Gy nous avons P p Q4 les pr dicats P et Q sont motivables dans P CP d apres le lemme 3 5 2 ainsi nous d rivons I F5 Py Q4 l aide du lemme 3 5 9 A Bx analogue au cas By Bapp analogue au cas 8 A f B B A avons alors B g A par la r gle Gym les pr dicats P et Q sont moti G_ par hypoth se de r currence nous avons A p Gy par hypoth se de r currence nous avons A g A Gsym par hypoth se de r currence nous avons A B nous y 92 3 5 Traductions vables dans P CP d apr s le lemme 3 5 2 ai
133. jours pas appliquer cette m thode de p dago gisation sans pr caution la pr sence d objets d ordre sup rieur pose d autres dif ficult s par exemple la r gle g permet de faire appara tre la formule L dans l importe quelle d rivation par 8 expansion 1 T par P Ax 2 H3 Aa T L par p et 1 De m me la r gle g peut g n rer dans les formules des pr dicats d ordre sup rieur non motivables D P V 65 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur 1 HT par P Ax 2 par P Ax et 1 3 T T par et 2 4 T TH T par P Ax et 3 5 8 T T T par et 4 6 H3 Aa a a a T par p et 5 Dans ce jugement le pr dicat non motivable est Aa a a a Lemme 3 3 1 Le pr dicat A a a a a n est pas motivable dans F CP D monstration Supposons que le pr dicat Aa a a a soit motivable dans F CP Alors le jugement H Va Aa a a a a est d rivable 1 FR Va Aa a a gt aja T HR Va a a a par et 1 He aa a par Ye et 2 He T par P Ax oR W bd at a par P Hyp et 4 e a a par i et 5 a par 3 et 6 8 F Va a par Vi et 7 F CP est un sous syst me de CP donc le jugement H Va a est d rivable ce qui est absurde compte tenu de la coh rence de CP ND Nous sommes alo
134. jugement T F est d rivable D monstration Par r currence sur la d rivation de IT Fp F ET Ax nous avons juste d river le jugement K T 1 T par le lemme 1 2 1 2 F T par N Ax 3 TH T par P Hyp 1 et 2 4 T T T par et 3 5 FT par 2 et 4 FFE F Hyp nous avons juste d river le jugement F T F gt F aIr par le lemme 1 2 1 n FT par le lemme 1 2 1 TrT F H F par P Hyp 1 et 2 4 F T F F par et 3 ewe eee r A B est d rivable et comme I B T A gt B le jugement F T A gt B est d rivable r H 4A B rH A ye go RE zy par hypoth se de r currence le jugement F F gt A gt B e nous avons juste d river le jugement F gt B CHAPITRE 1 Calculs propositionnels p dagogiques du premier ordre par le lemme 1 2 1 A Bjr par le lemme 1 2 1 Ar par le lemme 1 2 1 A B T AH T par P Hyp 1 2 et 3 7 AH T 4 8B par P Hyp 1 2 et 3 7 A A B par 5 et 4 A B T AH TA par P Hyp 1 2 et 3 T AH par 7et 4 r r A gt B rT AF B par 6et8 Tr A gt B r gt Ak TB par et 9 Tr A gt B I A T B par et 10 een OO I DOK ND e JF P A B T A T B8B par et 11 H F A B par hypoth
135. l application de la r gle P V 32 2 3 Calcul propositionnel p dagogique du second ordre Puis on d montre que toute motivation triviale reste triviale quand on lui applique une motivation triviale ce qui nous permettra de les compl ter et ventuellement de les rendre closes Lemme 2 3 3 Pour toutes substitutions u et o triviales dans P CP telles que u soit adapt es aux formules o a pour tout a Dom o la substitution u est triviale dans P CP D monstration Soit une variable contenue dans Dom o Par hypoth se le ju gement L o a est d rivable et d apr s le lemme 2 3 2 le jugement a LOQ est d rivable Ainsi la substitution u est triviale dans P CP De m me que le calcul F CP le calcul P CP permet de d river la r gle d affai blissement faiblement p dagogique F Aff Lemme 2 3 4 Pour tout jugement T L F d rivable et pour toute formule U telle que T U U soit motivable dans P CP le jugement T U re F est d rivable D monstration Analogue la preuve de la proposition 2 2 7 O Pour montrer que toutes les motivations triviales motivent les formules motivables il faut pouvoir les substituer les unes aux autres pour cela on d montre un lemme permettant de remplacer dans une formule toute sous formule prouvable par n im porte quelle formule prouvable Lemme 2 3 5 Soit T U F un ensemble de formules HTM dans P CP Pour toutes substitutions
136. l propositionnel du second ordre tudi dans le chapitre pr c dent D finition 3 1 7 Pour tout pr dicat P l ensemble VI P des variables libres de P est un ensemble de variables propositionnelles d fini par r currence sur P PS Ti a 0 P a VIP a PS eae VIP VI A U VI B P Va A gt VIP VI A a P A VIP VIVA tar P AB VI P VI A U VI B Par extension pour tout contexte T nous notons VI T l ensemble Ucer VIG Quand VI F 9 nous disons que le pr dicat F est clos D finition 3 1 8 Pour tout pr dicat P l ensemble Vq P des variables quan tifi es de P est un ensemble de variables propositionnelles d fini par r currence sur P 99 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur PS re Vq P 0 P o Vqaq P 0 P A gt B Va P Vq A U Va B P Va A Va P a U Vq A P a AE Vq P a U Vq A P AB Vq P Vq A U Vq B Pour instancier les variables quantifi es dans les pr dicats on a besoin de substi tutions D finition 3 1 9 Une substitution o est une fonction de domaine fini Dom o valeurs dans l ensemble des pr dicats Pour toute substitution on note VI o l union des ensembles VI c a pour tout a Dom o D finition 3 1 10 Pour toute substitution o et pour tout pr dicat P on dit que o est adapt e P quand l ensemble VI o N Vq P est vide D finition 3 1 11 Pour to
137. la quan tification universelle dans P CP porte uniquement sur les formules motivables ces calculs ne partagent plus exactement les m mes notions il est alors n cessaire de passer par l interm diaire d une traduction pour les comparer 43 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre 2 5 1 y traduction Friedman 10 d finit une traduction la A traduction permettant entre autres de plonger le calcul propositionnel intuitionniste dans le calcul propositionnel mi nimal Nous d finissons ci dessous la y traduction en nous inspirant du travail de Friedman pour plonger le calcul CP dans F CP et P CP Notons que plonger F CP et P CP dans CP est trivial puisque ces deux calculs p dagogiques sont des restrictions du calcul intuitionniste D finition 2 5 1 Soit F une formule et y une variable fraiche pour F La y traduction de F not e F7 est d finie par r currence sur F Flers F a FH Ay Ge F A gt B F A B F Va A F Va A La y traduction doit pr server l quivalence des formules par rapport aux d rivations J en particulier deux formules a quivalentes doivent rester a quivalentes apr s traduction Lemme 2 5 1 Pour toutes formules F et G si F G alors F GT D monstration Par r currence sur la d rivation de F a G ar par d finition nous avons T T donc T T7 n Qyar par d finition nous avons a7 a V y donc a a A
138. la r gle Ared sur un A terme typ par le jugement T H Aa t U a U F produit une d rivation du jugement I H a U t a U F il s agit de la d rivation du jugement T H F dans laquelle toutes les occurrences de la variable a sont remplac es par le type U Dans le cas de P AC il faut pouvoir motiver les types U dans tous les types a U A tels que A apparaisse dans la d rivation de I H t F nous allons prouver que c est toujours le cas Lemme 5 3 3 Pour tout type U et F motivables dans P C et pour toute variable a tels que la substitution a U soit adapt e F le type a U F est motivable dans P CP D monstration analogue la preuve du lemme 2 3 7 118 5 3 Normalisation Ainsi nous pouvons d montrer que l application de la r gle Ared pr serve le typage des termes r duits l aide des deux lemmes suivants Lemme 5 3 4 Pour tout jugement d rivable T ae t F sile type U est motivable dans P C alors le jugement a U T 3 la U t a U F est d rivable D monstration Notons js la substitution a U nous prouvons le lemme par r currence sur la d rivation de T ES t F Fip oT Pos T motivable dans P AC d apr s les lemmes 5 3 3 et 5 2 1 nous d rivons alors le jugement p T 3 H0 fT avec la r gle P Ax 2 ie T GE P Hyp analogue au cas pr c dent F x A as f B TH Att f AB T a A Fh 4 f w B est d rivable ainsi nous d rivons le jugement
139. le ainsi nous d rivons le jugement Pre 0 0 P 0 8 O PO 8 l aide de la r gle g par la r gle p nous d rivons galement le jugement T F 6 0 P 3 6 P 5 ainsi le jugement T F5 8 8 P 6 P est d rivable l aide de la r gle Vi BD 5 Lemme 3 5 4 Soient n un l ment de 2 w et T un ensemble motivable dans P CP Pour tout pr dicat P k pour tout pr dicat U motivable dans P CP tel que la substitution a U soit adapt e P et pour toute variable y fra che pour P le jugement T H a 8 U P a U P est d rivable 86 3 5 Traductions D monstration Par r currence sur P le cas P p est le seul cas non imm diat P p deux cas se pr sentent B a nous avons a U a 6 U et a O U a 8 8 U d apr s le lemme 3 5 3 le jugement TF 0 U de est d ri vable ainsi le jugement PF a 0 U P a U P est d rivable par la r gle Ext p a nous avons a O U 3 donc le jugement FF a 8 U P a U P est ais ment d rivable Dans les traductions n gatives les traductions des formules admettent l limina tion de la double n gation dans notre cas la double n gation d un pr dicat trans form P s crit O P il faut alors que P soit extensionnellement gale Pat Lemme 3 5 5 Soit n un l ment de 2 w Pour tout pr dica
140. les alors A B est une formule Afin d all ger l criture des formules nous crivons A B C les formules de la forme A B C Les formules seront toujours prouv es dans le cadre d un contexte repr sentant l ensemble des hypoth ses n cessaires au raisonnement D finition 1 1 2 Un contexte propositionnel du premier ordre est un ensemble fini de formules et dans ce chapitre nous les appelons contextes quand aucune ambiguit n est craindre Un jugement propositionnel du premier ordre est un CHAPITRE 1 Calculs propositionnels p dagogiques du premier ordre triplet not T F F avec I un contexte F une formule et id un identifiant tex tuel Dans ce chapitre les jugements propositionnels du premier ordre sont appel s jugements quand cela ne pr te pas confusion Le contexte vide est repr sent par le mot vide ainsi pour toute formule F et tout identifiant id le jugement 0 F F s crit galement F De plus pour tous contextes I et A le contexte UA est not I A En particulier pour toute formule le jugement TU A Fiq F est not T A Fi F Ensuite nous d finissons le calcul proprement dit sa morphologie et sa syntaxe Nous nous pla ons dans le cadre des syst mes de d duction naturelle d velopp s par Gentzen 11 puis par Prawitz 35 sous la forme d un calcul des s quents intui tionniste Nous l avons choisi car il offre une pr sentation fid le du raisonnemen
141. les quantifi es Lemme 5 5 5 Pour tout type F et G si F G alors FT GT D monstration Par r currence sur la d rivation de F G ET ar nous avons T7 T7 ainsi nous avons TY T7 7 D Qyar nous avons q7 a ainsi nous avons a a7 A A B a B A B A B A et BY B ainsi nous avons A B A B l aide de la r gle a a 6 A B B 6 Fr A B Va A V3 B par hypoth se de r currence nous avons a d A a 8 5 B7 d apr s le lemme 5 5 1 nous avons a 6 A7 a 67 A et G d A 6 67 B a_ par hypoth se de r currence nous avons A7 ay nous pouvons supposer que 7 nous avons 67 ainsi nous avons a A7 3 6 B7 nous avons Va AT VG B7 l aide de la r gle ay ainsi nous d rivons ais ment Va AT Y B Nous d montrons maintenant la proposition principale Proposition 5 5 6 Pour tout jugement d rivable T H3 t F le jugement FH t FY est d rivable 126 5 5 Traduction CPS D monstration Par r currence sur la d rivation de TF t F Teor HS DAT d apr s le lemme 5 5 2 ip DAT T d apr s le lemme 5 5 3 I7 k T a k T par P Hyp 1 et 2 I k T zA o T par P Ax 1 et 2 IY k T Fy ko y par 3 et 4 6 TTF AKT ko T7 par 4 et 5 ainsi le jugement FT F4 0 T7 est d rivable eS E rr Se Came os Fe yp Xp D
142. les systemes p dagogiques et les systemes sans n gation la contrainte p dagogique et les bonnes propri t s qu on lui demande sont fondamentalement syntaxiques car les motivations qui sont les t moins du sens des formules sont des objets finis construits partir des formules tandis que dans les syst mes sans n gation la contrainte peut n tre que s mantique On note que ces deux calculs le faible et le contraint ne sont pas associ s un A calcul normalisant dans les deux cas on peut construire une d rivation d un jugement F F dans lequel la formule F n est pas motivable mais la mise en forme normale de cette d rivation n cessite de pouvoir d river le jugement FH F ce qui n est possible que si F est une formule motivable L ajout d un principe d extentionnalit r sout ce probleme on d finit l galit extensionnelle P Q de deux pr dicats P et Q par le fait qu ils produisent des formules quivalentes quel que soit les arguments qu on leur passe en param tres P Q signifie que P et Q sont indiscernables du point de vue du calcul On ajoute alors au calcul la r gle d extentionnalit Ext TE la U A PRU Prva Ext On obtient le calcul propositionnel p dagogique du second ordre dans lequel tous les pr dicats sont h r ditairement trivialement motivables Malheureusement il n y a pas notre connaissance de calcul prenant en compte la r gle d extentionnalit sa
143. mais U est une formule motivable dans P CP d apr s la proposition 2 3 9 42 2 5 Traductions R gle d limination Dans le cas de F CP la r gle d limination du quantificateur existentiel est d rivable T HN eA TAC egVIT C TRO Proposition 2 4 11 La r gle E Je est va lide dans F CP D monstration Supposons que les jugements T de A et T A C soient d rivables 1 T H Vy Ve A y par hypoth se 2 T H Ye A gt C C par W 1eteg VIT C 3 T AH C par hypoth se 4 THA C par et 3 5 TH VeA C par V et 4 6 TH C par 2 et 5 Il en est de m me dans le cas de P CP H2 A PAHO eg VIT C 4 L 7 Je est va rH C Proposition 2 4 12 La r gle lide dans P CP D monstration Cette preuve est analogue celle de la proposition 2 4 11 Cepen dant la ligne 2 nous devons motiver dans P CP la formules C pour appliquer la r gle P Ve la place de la r gle Ye mais C est une formule motivable dans P CP d apr s la proposition 2 3 9 2 5 Traductions Comparer l expressivit respective de CP et des calculs p dagogiques n est pas imm diat puisque d apr s les propositions 2 2 13 et 2 3 10 il existe des th or mes de CP qui ne sont pas prouvables dans F CP ni dans P CP La contrainte p dagogique change la signification des op rateurs logiques par exemple
144. mble des variables fra ches d un contexte T est not Fr T Les variables li es sont destin es repr senter n importe quelle formule ainsi leur nom importe peu on est m me parfois oblig de les renommer pour viter qu elle ne prennent le nom de variables libres Pour pouvoir librement renommer les variables li es d une formule on introduit la relation d a quivalence deux for mules sont a quivalentes quand elles ne diff rent que par le nom de leurs variables li es D finition 2 1 9 Pour toutes formules A et B la relation d a quivalence entre A et B not e A B est d finie par les r gles suivantes T 7 ar az a me A A B B A B A B a a y A a 6 7 B y Fr A B on Ya A VB B Y Quand la relation A a B est v rifi e on dit que les formules A et B sont a quivalentes Enfin nous d finissons les r gles de d duction du calcul propositionnel intui tionniste du second ordre D finition 2 1 10 Le calcul propositionnel du second ordre abr g en CP est d fini par sa morphologie constitu par l ensemble des jugements de la forme T F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles suivantes Ter 20 2 2 Calcul propositionnel du second ordre faiblement p dagogique T rrr Hyp T A H B rT A gt B TPA TAB gt i T B 3g THA a VI
145. ment typ abr g en P AC est d fini par sa morphologie constitu e par l ensemble des jugements de la forme T Fip F3 sa syntaxe constitu e par l ensemble des d rivations d finies par r currence l aide des r gles et ainsi que des deux r gles suivantes 1 Frl P Ax Fiap o T 2 FET H oT Poa e On dit qu un jugement T Fip t F est d rivable quand il existe une d rivation dans P C dont la derni re r gle utilis e produit ce jugement Sans d rivation p dagogique il nous tait impossible de d finir les motivations puisque celles ci font appel la notion de preuve nous sommes maintenant en mesure de les introduire 105 CHAPITRE 4 calcul p dagogique simplement typ D finition 4 2 9 Soit C un calcul dont la morphologie est constitu par l ensemble des jugements de la forme T Hi F Pour tout contexte A une motivation de A dans C est une substitution o telle que pour tout x F A il existe un terme t tel que le jugement F t o F soit d rivable Quand un contexte admet une motivation dans C on dit qu il est motivable De plus une motivation d une formule F dans C est une motivation du singleton F dans C 4 3 Traduction Nous avons montr dans le chapitre 1 que le calcul p dagogique P CPM est quivalent au calcul usuel CPM il en est de m me dans les systemes formels Pour tout type F la notation Fr repr sente le type F dans lequel toutes l
146. mme a U P est o UTM dans P CP U est galement u UTM dans P CP B a nous avons a VI P ce qui est contradictoire on en d duit alors le r sultat par l absurde P A B comme a VI P nous avons soit a VI A soit a VI B dans chacun des deux cas le pr dicat U est o UTM dans P CP par hy poth se de r currence 73 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur P VB A par a quivalence on peut supposer que 8 4 a soit V une for mule d rivable dans P CP comme a VI P nous avons a VI A par hypoth se de r currence le pr dicat U est o s 3 V UTM dans P CP comme la substitution a U est adapt e P nous avons 8 VI U ainsi d apr s le lemme 3 4 11 le pr dicat U est o UTM dans P CP P B A analogue au cas pr c dent P AB analogue au cas P A gt B La troisi me propri t est qu une motivation uniforme est une motivation instan ciant toutes les variables libres des pr dicats qu elle motive Lemme 3 4 9 Soit n l ment de 2 w Pour tout pr dicat P et pour toute substi tution o triviale dans P CP si P est o UTM dans P CP alors VI P Dom o D monstration Imm diate par r currence sur P Enfin la quatri me propri t restaure le statut de repr sentant de chaque formule P en montrant que pour qu un pr dicat P soit uniform ment motivable il suffit que la f
147. montrables ou bien il faut construire une d monstration en r gle soit par l exemple soit par l emploi du raisonnement par r currence Ce n est pas que cette d monstration soit moins n cessaire quand il s agit d une d finition xi Pr sentation synth tique directe mais elle est g n ralement plus facile Rejetant les d finitions impr dicatives c est dire les d finitions d objets faisant appel implicitement ou explicitement a la totalit des objets de meme nature Poin car nonce ici un principe tout a fait en accord avec le reste de ses pr occupations mais on peut constater que tous les d veloppements logiques ult rieurs se r clamant de la pens e de Poincar en particulier dans le domaine des syst mes formels pr dicatifs ce principe est syst matiquement ignor Lors de la crise des fondements Luitzen Egbertus Jan Brouwer d veloppa les math matiques intuitionnistes formalis s plus tard par Arend Heyting en tant qu alternative aux syst mes formels dits classiques Les syst mes formels in tuitionnistes sont suppos s rendre fid lement compte de l activit intellectuelle du math maticien au travers des objets qu il manipule Ces syst mes ont la pro pri t d tre constructifs c est dire que tous les objets dont on peut prouver l existence sont repr sentables par des termes Cependant rien n interdit ces syst mes de manipuler des objets non instanciables do
148. mule trivialement vraie repr sentable dans les calculs des pr dicats par les formules atomiques telles que XX t t avec t un terme du premier ordre C est sous cette forme que j ai r cup r les systemes p dagogiques La premi re tape fut d tudier la tentative initiale de construction d un sys t me p dagogique bas sur le calcul propositionnel minimal le calcul p dagogique minimal naif Tout d abord on remarque que toutes les formules sont motivables c est dire que pour toute formule F il existe une substitution telle que la for mule o F soit prouvable On montre alors que tous les th or mes dans le calcul minimal sont des th or mes dans la version na ve du calcul p dagogique associ Malheureusement ce qui est vrai pour les th or mes ne l est plus pour les juge ments le jugement T T F T n est pas d rivable dans le calcul na f La solution est de modifier la r gle Ax sous la forme de la r gle P Ax FoI Tere On obtient alors le calcul p dagogique minimal dans lequel on peut d river tous les jugements d rivables dans le calcul usuel L observation de la preuve de ce r sultat met en vidence Videntit structurelle entre les preuves usuelles et les preuves p dagogiques dans lesquelles on remplace les occurrences de la r gle P Hyp par des applications de la r gle Hyp Comme la structure des preuves est conserv e il en est forc ment de m me pour les A termes dans
149. n gation g n ralis e peut tre limin e lors de l application de substitutions Lemme 3 5 3 Soit n un l ment de 2 w Pour tout pr dicat P k pour tout ensemble T motivable dans P CP et pour toute variable y fra che pour P le jugement T F5 0 0 P 6 P est d rivable D monstration Par r currence sur K k x nous avons P P et OOF Sam ae 5 P par P Hyp et le lemme 3 5 2 H P par P Hyp et le lemme 3 5 2 yP P mP HE Yy par gt e 1 et 2 F mym P par 5 et 3 mP P HE my P par P Hyp et le lemme 3 5 2 mP P Hy par gt e 4et 5 J v J D J J Y 50 50 8 TH mm P gt P par gt i et 7 donc le jugement T Hp 0 0 P P est d rivable 1 T P mnm P F m P par P Hyp et le lemme 3 5 2 2 T P mnm P Fi mP par P Hyp et le lemme 3 5 2 3 T P mym P pY par gt e 1 et 2 4 T P H mP par gt i et 3 5 FH mP gt mym P par et 4 donc le jugement Ff O P 0 0 P est d rivable ainsi le jugement TFS 0 0 P O P est d rivable Kk 1 0 soit B une variable fraiche pour I et P par hypoth se de r cur rence le jugement H 0 0 P0 3 o PO 6 par hypoth se de r currence le jugement T H 0 3 ainsi le jugement T F5 0 0 PO 8 e O PO 8 est d rivable l aide de la r gle Ext le jugement IT F5 P0 0 8 x 9 P 8 8 est ais ment d rivab
150. n peut tre close ou non comme nous l avons expliqu dans le chapitre pr c dent Dans le cas ces calculs d ordre sup rieur d s qu un pr dicat est motivable par une motivation ouverte alors on peut toujours la motiver par une motivation close on a alors la garantie qu un exemple abstrait peut toujours tre pr cis en un exemple concret Proposition 3 2 3 Soit n un l ment de 2 w Pour toute formule F d ordre n si o est une motivation de F dans F CP alors pour toute substitution u d ordre n adapt e ao F la substitution u o est une motivation de F dans F CP D monstration Analogue la preuve de la proposition 2 2 1 3 2 2 Non nullit syntaxique des jugements La notion de non nullit syntaxique des jugements introduite dans le chapitre pr c dent se g n ralise facilement aux calculs d ordre sup rieur D finition 3 2 4 Soient n un l ment de 2 w et C un calcul dont la morphologie est constitu par l ensemble des jugements de la forme T F F Un jugement Tr F F est syntaxiquement non nul quand son contexte IT est motivable dans C 61 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur Nous d montrons de suite que dans les calculs F CP tous les jugements sont syntaxiquement non nuls Lemme 3 2 4 Soit n un l ment de 2 w Pour tout jugement T H F d rivable le contexte T est motivable dans F CP D monstration Analogue
151. ne peuvent plus tre utilis es car elles requi rent la pr sence de la formule L dans les jugements constituant leurs pr misses Les calculs P CPT et P CPC sont donc quivalents CPM Proposition 1 3 4 Pour tout L jugement d rivable I F F le jugement PF F est un jugement d rivable D monstration D apr s le lemme 1 3 2 les l ments de IT U F sont des formules donc le L jugement F F est un jugement Montrons par r currence sur la d rivation de I Fp F que l E F est d rivable la d monstration est imm diate sauf pour le cas de la r gle 1 I asec Tr Li L est une formule d apr s le lemme 1 3 2 ce qui est absurde Proposition 1 3 5 Pour tout L jugement d rivableT F le jugement I F F est un jugement d rivable D monstration D apr s le lemme 1 3 3 les l ments de TU F sont des formules donc le L jugement IF F est un jugement Montrons par r currence sur la d rivation de I F e F que I F F est d rivable la d monstration est imm diate sauf pour le cas de la r gle Le PRE Here a est absurde Le Let F sont des formules d apr s le lemme 1 3 3 ce qui 15 CHAPITRE 1 Calculs propositionnels p dagogiques du premier ordre Ces deux r sultats ach vent notre tude des calculs P CPM P CPI et P CPC tous les trois quivalents amp CPM Le calcul propositionnel minimal est donc dans un sens implicitement p dagogique la pr sence de la
152. nnelles sont remplac es par T De m me pour tout contexte I on note I l ensemble des formules F telles que F ET Il convient tout d abord de caract riser les formules motivables dans N CPM on prouve ci dessous que toutes les formules sont motivables dans N CPM Lemme 1 2 1 Pour toute formule F le jugement F Fr est d rivable D monstration Par r currence sur F F T ona Ty T ainsi le jugement H Fr est d rivable par la r gle N Ax F a ona ar T et on conclut comme dans le cas pr c dent F A B ona Fr A By donc nous avons juste d river le juge ment Ar gt Br 1 2 Calcul propositionnel p dagogique minimal Ar par hypoth se de r currence By par hypoth se de r currence B A F Bt par P Hyp 1 et 2 By At gt Br par et 3 Br At Br par x et 4 Ar Br par gt e 5 et 2 n Q amp ND Fe en SES SE NS n Nous allons maintenant comparer l expressivit de CPM et de N CPM On remarque imm diatement que N CPM ne permet pas de prouver plus de choses que CPM puisque il est une restriction de CPM Lemme 1 2 2 Pour tout jugement I F F d rivable le jugement TH F est d rivable D monstration Imm diate par r currence sur la d rivation de I F F R ciproquement tout ce qui est prouvable dans CPM est prouvable dans N CPM Lemme 1 2 3 Pour tout jugement TH F d rivable le
153. ns alors le jugement T H Aya 0 P O l aide de la r gle g nous avons a O a ainsi nous avons une d rivation du jugement l E Pya Pa d apr s le lemme 3 5 5 le jugement 90 3 5 Traductions r Hp Pa 9 Pa est d rivable nous d rivons alors le jugement l E Pa Pa l aide de la r gle Ext de m me nous d rivons le juge ment P Fp Q a Qa nous d rivons alors le jugement I F Pya Q a l aide de la r gle Ext le jugement I F5 Va Pya Qa l aide de la r gle Vj ainsi nous avons une d rivation du jugement I F5 Py Q Parmi toutes les propri t s qui doivent tre conserv es apr s traduction on compte videmment l a quivalence Lemme 3 5 8 Soit n un l ment de 2 w Soient P k et U k deux pr dicats Soit y une variable fra che pour P et Q Si P a Q est d rivable alors Py a Q est d rivable D monstration Par r currence sur la d rivation de P Q See ar ce cas est imm diat car T T UE avar la relation est r flexive donc nous avons a A A BaB A B A B A et By a B nous avons alors Ay B A B par la r gle a_ ainsi nous avons P Q4 a d A B 6 B 6 Fr A B Va A VG B avons a A a B 5 B par une r currence imm diate sur A nous avons a A a A de m me nous avons 8 B B d
154. ns besoin de contextes qui sont des ensembles d hypoth ses D finition 3 1 6 Soit n un l ment de 2 w Un contexte propositionnel d ordre n est un ensemble fini de formules d ordre n Dans ce chapitre nous les appelons contextes d ordre n ou plus concis ment contextes en l absence d ambiguit Dans le cas o n est gal w les contextes d ordre w sont galement appel s contextes propositionnels d ordre sup rieur Un jugement propositionnel d ordre n est un triplet not T F avec T un contexte d ordre n F une formule d ordre n et id un identifiant textuel Dans ce chapitre les jugements propositionnels d ordre n sont appel s jugements d ordre n ou plus concis ment jugements en l absence d ambiguit Dans le cas o n est gal aw les jugements d ordre w sont galement appel s jugements propositionnels d ordre sup rieur Le contexte vide est repr sent par le mot vide ainsi pour tout l ment n de 2 w pour toute formule F d ordre n et pour tout identifiant id le jugement Ot F s crit galement H F De plus pour tous contextes I et A d ordre n le contexte TU A est not T A En particulier pour toute formule d ordre n le jugement T U A F F est not T A F F Les variables propositionnelles sont destin es tre ventuellement quantifi es uni versellement il nous faut distinguer les variables libres des variables quantifi es comme dans le cas du calcu
155. ns la propri t de non nullit syntaxique des jugements dans les calculs P CP par la proposition suivante Proposition 3 4 20 Soit n un l ment de 2 w Pour tout jugement d rivable T Hp F le jugement F5 G r est d rivable pour tout sous pr dicat G des formules dans FU F D monstration Soit 7 la substitution qui toute variable a associe le pr dicat T D apr s la proposition 3 4 19 l ensemble T U F est r UTM dans P CP Soit G un sous pr dicat d une formule dans F U F D apr s la proposition 3 4 8 la formule G est r UTM dans P CP Ainsi d apr s le lemme 3 4 7 G est motivable par 7 dans P CP 82 3 5 Traductions En particulier toutes les formules motivables sont motivables par T ce qui nous permet de simplifier la r gle d affaiblissement faiblement p dagogique F Aff a l aide de la r gle d affaiblissement p dagogique P Aff TRF Po TURF P Aff Le dernier r sultat important concerne les propri t s des formules motivables ex primables dans les calculs P CP le r sultat est que toutes les propri t s des formules motivables exprimables usuellement c est dire dans CP sont expri mables dans P CP ainsi ces calculs p dagogiques capturent toutes les propri t s qui concernent la bonne notion de formules dans les systemes p dagogiques Proposition 3 4 21 Soient n un l ment de 2 w et o une substitution triviale dans P CP Pou
156. nsi nous d rivons I FS Py Q l aide du lemme 3 5 9 A B B yC A C B et B C nous avons alors A C par la r gle Gtrans les pr dicats P et Q sont motivables dans P CP d apr s le lemme 3 5 2 ainsi nous d rivons Fp P Q l aide du lemme 3 5 9 ES u Vat A ze uB Aat A B p a B A lemme 3 5 2 les formules A et B sont motivables dans P CP par la substitution y T comme y a la formule Va A est motivable dans P CP par la substitution 7 T ainsi nous avons P a B A les pr dicat P et a B A sont motivables d apr s le lemme 3 5 2 d apr s le lemme 3 5 6 le jugement T Fp a B A la B A est d rivable Birans par hypoth se de r currence nous avons A P Greq nous avons P Aa A B d apr s le p ainsi le pr dicat a B A est motivable d apr s le lemme 3 5 9 le ju gement FY Py a B A est d rivable nous d rivons le jugement r Fy Py a B A l aide de la r gle Ext nous avons alors une d rivation du jugement FS Py x Q Nous pouvons maintenant prouver la premi re moiti de la propri t de pr serva tion de la d ductibilit par traduction si un jugement est d rivable dans CCP alors sa traduction est d rivable dans P CP Lemme 3 5 11 Soitn un l ment de 2 w Pour tout jugement d rivable T H F le jugement T Hp Fy est d rivable avec y une variable fra che po
157. nstration Analogue la preuve du lemme 2 2 5 62 3 2 Calculs propositionnels faiblement p dagogiques d ordre sup rieur Nous d montrons alors que la r gle d affaiblissement faiblement p dagogique CHEF Ho T U TURF F Aff est valide dans les calculs F CP Proposition 3 2 8 Soit n un l ment de 2 w Pour tout jugement T FP F d rivable et pour toute formule U telle que TU U soit motivable dans F CP le jugement l U F F est d rivable D monstration Analogue la preuve du lemme 2 2 7 3 2 4 Les th or mes de CP sont prouvables dans F CP La proposition 2 2 13 affirme que le jugement Va a n est pas d rivable donc F CP ne d montre pas tous les th or mes de CP Cependant nous allons d montrer que pour tout n gt 2 les th or mes de CP sont des th or mes de F CP Pour cela il suffit d exprimer toutes les preuves des th or mes de CP sous la forme de preuves la Hilbert dans lesquelles il n y a pas besoin de contextes et donc il n y a pas besoin de les motiver Lemme 3 2 9 Soit n un l ment de 2 w Pour tout jugement T F d rivable le jugement Fe T F est d rivable D monstration Par r currence sur la d rivation du jugement LH F Tp N 1 HT Yy T ais ment d rivable 2 HT T par v et 1 Fer rap p 1 HIVER qi ais ment d rivable avec 1 lt i lt n 2 HHT F par _ et 1 Tr AB
158. nt FF ua est d rivable P A B soit u une substitution triviale telle que VI P Dom u o motive P dans P CP donc d apr s le lemme 3 4 6 u motive P dans P CP A et B sont o UTM dans P CP par hypoth se de r currence A et B sont u UTM dans P CP ainsi P est u UTM dans P CP P Va A soit u une substitution triviale telle que VI P Dom u o motive P dans P CP donc d apr s le lemme 3 4 6 u motive P dans P CP soit U une formule d rivable dans P CP A est o q a U UTM dans P CP par hypoth se de r currence A est na a U UTM dans P CP ainsi P est u UTM dans P CP P a A analogue au cas P Va A P AB analogue au cas P A gt B La preuve que toutes les formules des d rivations des calculs P CP sont uni form ment trivialement motivables se fait par r currence sur les d rivations le lemme suivant concerne les cas des r gles contenant des preuves de motivations comme les r gles P Ax et P Hyp Lemme 3 4 12 Soit n un l ment de 2 w Soient P un pr dicat et o et u deux substitutions triviales dans P CP Si le pr dicat o P est 1 UTM dans P CP alors pour toute substitution p triviale dans P CP telle que Dom p Dom o U Dom u P est p UTM dans P CP D monstration Par r currence sur P P T soit p une substitution triviale dans P CP telle que Dom p Dom o U Dom u P est p UTM dans P CP P a
159. nt la d finition n est pas motivable ou m me incoh rente Cette observation a men George Francois Cor nelis Griss d velopper des math matiques dans lesquelles tous les objets uti lis s dans une d monstration sont d finis par des postulats non contradictoires des math matiques sans n gation Il affirmait que les notions math matiques de vraient tre limit es celles bas es sur des constructions si la construction s av re impossible on ne peut avoir une id e claire de la nature de l objet et la notion ne v hicule alors aucun sens Les arguments avanc s par Griss sont assez pauvres et l instar des arguments de Poincar ils semblent relever du simple bon sens pour son auteur Bien qu il y ait une certaine familiarit entre le principe nonc par Poincar et les consid rations de Griss nous ne savons pas si le premier a inspir le second ou si ces deux approches sont apparues ind pendamment Quoi qu il en soit Griss toffa ses recherches et publia dans une s ries d articles 15 16 17 et 18 une bauche informelle de ce que pourraient tre une arithm tique une g om trie et une analyse sans n gation Plusieurs tentatives de formalisation des id es de Griss ont t men es on peut citer les travaux de Vredenduin 39 Gilmore 12 et Valpola 37 mais la premi re formalisation la plus aboutie semble avoir t celle de David Nelson 31 32 Il introduisit la notion d implicat
160. nth tique contrainte p dagogique impose que toute formule d riv e soit motivable quel que soit le contexte ainsi le jugement I H L n est d rivable pour aucun contexte T alors que dans le cas usuel par exemple le jugement L est ais ment d rivable En rempla ant la r gle V par la r gle P V comme dans le cas du second ordre on obtient le calcul propositionnel p dagogique contraint Dans les calculs d ordre sup rieur les formules sont g n ralis s en pr dicats qui sont des fonctions dont le type est d crit par leur genre il y a le genre des formules not x et le genre k des fonctions consommant les pr dicats de genre x et produisant des pr dicats de genre v La notion de motivation est tendue aux pr dicats un pr dicat P est motivable si il produit une formule motivable quel que soit les pr dicats qui lui sont pass s en argument plus formellement si on note k gt gt kx le genre de P alors P est motivable quand la formule Va Va Pai a est motivable Dans ce syst me les formules apparaissant dans les d rivations ne sont pas forc ment h r ditairement motivables cependant toutes les sous formules de ces formules sont vraies pour au moins une distribution de valeurs de v rit s au sens de la s mantique bool enne binaire ainsi ce calcul est d nu de n gation mais il n est pas pour autant p dagogique au sens fort On observe ici une diff rence importante entre
161. o et u triviales dans P CP et adapt es F telles que Dom o Dom u si le jugement T F o F est d rivable alors le jugement T H u F est d rivable D monstration Par r currence sur F F T supposons que Re o T soit d rivable nous avons o T T et T u T donc nous avons une d rivation de Fe oT F a supposons que I ie o a soit d rivable deux cas se pr sentent a Dom c par hypoth se la substitution u est triviale dans P CP donc le jugement Ee 1 a est d rivable par hypoth se le contexte est motivable dans P CP donc le jugement T Re ua est d rivable d apr s le lemme 2 3 4 a Dom o dans ce cas nous avons une d rivation du jugement T Gs Q par hypoth se Dom o Dom u donc p a a et nous avons une d rivation de T F2 p a 33 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre F A B supposons que le jugement T Be o A B soit d rivable le contexte I est HTM dans P CP donc il existe une substitution 7 triviale qui motive I dans P CP et d apr s le lemme 2 3 3 la substitution 7 p est triviale dans P CP la formule A est HTM dans P CP donc il existe une substitution p triviale qui motive A dans P CP et d apr s les lemmes 2 3 2 et 2 3 3 nous pouvons supposer les domaines Dom r et Dom p suffisam ment grands pour que nous ayons Dom p Dom r y par hypoth se de r currence sur le jugement He p A le jugement zA TO pA est d riv
162. onction et la disjonc tion y soient d finissables pour deux formules A et B la conjonction A A B est d finissable par la formule A B et la disjonction A V B est d finissable par la formule A B La situation est diff rente dans CPI car la conjonction et la disjonction n y sont pas d finissables Cependant nous sommes seulement int ress s par la pr sence de la n gation l expressivit de CPI est donc suffisante 1 3 2 P dagogisation de la n gation La p dagogisation des calculs CPI et CPC se fait comme celle de CPM en rempla ant respectivement les r gles Ax et Hyp par les r gles P Ax et P Hyp D finition 1 3 6 Le calcul propositionnel p dagogique intuitionniste abr g en P CPI est d fini par sa morphologie constitu par l ensemble des L jugements de la forme THF sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles P Ax P Hyp i e et Li On dit qu un L jugement I F F est d rivable quand il existe une d rivation dans P CPI dont la derni re r gle utilis e produit ce L jugement D finition 1 3 7 Le calcul propositionnel p dagogique classique abr g en P CPC est d fini par sa morphologie constitu par l ensemble des L jugements de la forme PES sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles P Ax P Hyp i e et Le
163. ons que le jugement H a y y a soit d rivable alors le jugement H a 7 a est d rivable de m me que le jugement FY a T T gt par instanciation de y comme le jugement a T T est d rivable on obtient une d rivation de a ce qui contredit la coh rence de CCP C est pourquoi il nous faut d finir une autre traduction d riv e de la y traduction D finition 3 5 4 Pour tout pr dicat P on d finit le pr dicat P comme tant VAPCRE Nous avons deux propri t s d montrer la premi re est la pr servation de la d rivabilit par notre traductions et la seconde est l quivalence dans CCP des formules et de leur traduction Voici d abord la d monstration de la pr servation de la d rivabilit Proposition 3 5 15 Soit n un l ment de 2 w Pour toute formule F le juge ment Fe Fest d rivable si et seulement si le jugement F5 F est d rivable 96 3 5 Traductions D monstration D apr s la proposition 3 5 14 Enfin voici la preuve de l quivalence dans CCP des formules et de leur traduc tion Proposition 3 5 16 Soit n un l ment de 2 w Pour toute formule F d ordre n le jugement F F F est d rivable D monstration 1 FH Vy F par Hyp 2 F H Fi par We et 1 3 F H F F d apr s la proposition 3 5 12 4 F H F par Ext 2 et 3 5 F F gt F par et 4 ainsi le jugement F
164. ont d rivables par hypoth se les ensembles PU F et FU G sont trivialement motivables d apr s le lemme 3 4 4 donc les jugements I FF Get T G FS F sont d rivables d apr s le lemme 3 4 3 Les jugements Fp F G et PFS G F sont d rivables par la r gle ainsi le jugement T F F G est d rivable k gt 0 les jugements l E FeT ee G sont d rivables par hypoth se Nous avons F Va F a donc T Fa est d rivable par la r gle P V De m me le jugement l E Ga est d rivable Par hypoth se de r currence le jugement Fy Fa Ga est d rivable ainsi le jugement P Fp F G est d rivable par la r gle Vi Dans les calculs P CP on peut substituer une sous formule prouvable par une autre formule prouvable dans l importe quelle d rivation ce qui nous permettra de remplacer n importe quelle motivation triviale par la motivation T 72 3 4 Calculs propositionnels p dagogiques d ordre sup rieur Lemme 3 4 6 Soit n un l ment de 2 w Soient T un contexte trivialement motivable dans P CP et F une formule Pour toutes substitutions o et u triviales dans P CP et adapt es T U F telles que Dom o N VI F Dom wu si le jugement T ES o F est d rivable alors le jugement VFS u F est d rivable D monstration o et u sont deux substitutions triviales dans P CP donc d apr s le lemme 3 4 1 u est une substitution triviale dans P CP D apr s le lemme 3
165. or mules et sous formules apparaissant dans les d rivations sont motivables Nous souhaitons obtenir des calculs d ordre sup rieur jouissant des m mes propri t s que P CP Il faut d abord donner un sens la notion de motivation appliqu e aux pr dicats d ordre sup rieur pour pouvoir remplacer la r gle Ve par la r gle P V On remarque que le pr dicat Aa a repr sentant l identit sur les formules ne doit pas tre motivable sous peine de pouvoir d river H L L avec L Va a Ic par P Ax H8 YPAABET Va ya par Vi et 1 Va ya H Va ya par P Hyp et 2 F3 Va ya Va ya par et 3 or WwW ND H3 VX Var ya Va ya par Vi et 4 3 Va XB Ba Va AB 38 a par P V 5 et AG G motivable 7 H Va a Va a par p et 6 Ne pas avoir le droit de motiver l identit impose de tr s fortes restrictions sur la notion de motivation on ne peut pas se contenter d imposer la motivabilit du pr dicat pour seulement certains arguments par exemple ceux qui sont motivables il faut que le pr dicat soit motivable quelque soit ses arguments C est pourquoi nous avons choisi de d finir qu un pr dicat P est motivable quand la formule P Ya V3 Pa est motivable Avec cette d finition nous obtenons une version de la r gle P V adapt e aux calculs d ordre sup rieur TH Yaf A Ho U FF a U A Cependant nous ne pouvons tou
166. ormule P soit uniform ment motivable Lemme 3 4 10 Soit n l ment de 2 w Soit x un genre Pour tout pr dicat P k et pour toute substitution o triviale dans P CP si P est o UTM dans P CP alors P est o UTM dans P CP D monstration Par r currence sur kK K x nous avons P P donc P est o UTM dans P CP k 1 0 nous avons P Va Pa donc pour toute formule U d rivable dans P CP la formule Pa est o a U UTM dans P CP par hypoth se de r currence pour toute formule U d rivable dans P CP le pr dicat Pa est o a a U UTM dans P CP ainsi P est o a U UTM dans P CP par a quivalence on peut supposer que a VI P ainsi le pr dicat P est o UTM d apr s le lemme 3 4 11 La propri t suivante est sp cifique aux calculs p dagogiques propositionnels elle affirme que toutes les motivations triviales uniformes sont quivalentes donc in terchangeables Lemme 3 4 11 Soit n l ment de 2 w Pour tout pr dicat P et pour toute substitution o triviale dans P CP si P est o UTM alors pour toute substitution triviale u telle que VI P C Dom u P est u UTM D monstration Par r currence sur P 74 3 4 Calculs propositionnels p dagogiques d ordre sup rieur P T soit u une substitution triviale telle que VI P Dom u P est u UTM dans P CP P a soit u une substitution triviale telle que VI P C Dom y nous avons a Dom u donc le jugeme
167. ort au sens intuitif des formules reste malheureusement assez faible le fait qu il existe une traduction qui fonctionne ne signifie pas qu on puisse l appliquer syst matiquement des th or mes classiques afin d obtenir peu de frais un quivalent positif La possibilit de reformulation existe mais c est au math maticien de choisir la bonne mani re de reformuler ses th or mes de mani re satisfaisante par rapport aux objets qu il tudie 98 Deuxieme partie Systemes fonctionnels p dagogiques 100 Chapitre 4 A calcul p dagogique simplement typ 4 1 calcul simplement typ Le A calcul a t cr par Alonzo Church 3 dans les ann es 1930 pour tenter de fournir un fondement aux math matiques plus naturel que la th orie des ensembles Il est compos de variables x y z repr sentant des fonctions d applications tu de fonctions t des fonctions u et d abstractions Ax t qui toute fonction x associe la fonction t x tant une variable Il y a une analogie tr s forte entre le A calcul et la th orie na ve des ensembles les fonctions correspondent des ensembles les applications tu sont associ es aux appartenances u t et les abstractions x t repr sentent les d finitions d ensembles x t Le calcul h rite alors de tous les paradoxes entachant la th orie na ve des ensembles mais dans ce cas pr cis ce qui est un inconv nient pour les ensembles est un avantage pour
168. our constater l int r t que suscite la contrainte de ne parler que d objets concrets ou d abstractions portant sur des objets concrets Dans l enseignement en particu lier en math matiques plus d un tudiant se sent troubl par la donn e d objets incoh rents dans le cadre de la r gle du ex falso la question revient souvent Comment peut on avoir le droit de supposer des choses fausses Manifeste ment l nonc faux ne fait pas sens dans leur esprit ils n ont rien manipuler rien toucher Il est fr quent dans l enseignement des math matiques de faire ap pel des exemples illustrant des notions abstraites trop th r es pour tre saisies telles quelles Ces exemples fournissent aux tudiants un guide concret un tuteur le long duquel se d veloppera un savoir g n ral La formalisation de cette pratique p dagogique est un passage oblig dans l tude scientifique de l apprentissage En d gageant rigoureusement les propri t s de l int gration du savoir abstrait il de vient possible de l appliquer en dehors de son milieu naturel afin de ne plus le limiter aux tre humains De m me que la formalisation de la notion de calcul a permis de la rendre ind pendant de l esprit humain et ainsi de concevoir des machines universelles du moins Turing compl tes la formalisation d une partie de l apprentissage et la construction d une s mantique formelle adapt e c est dire une
169. ous ne pouvons fournir un exemple tel que o F soit prouvable F tant une formule contradictoire Ainsi les syst mes p dagogiques sont non seulement intuitionnistes mais galement positifs c est dire exempts de n gation Dans un premier temps nous tudions l aspect purement logique des syst mes p dagogiques L ventail des syst mes tudi s se limitent aux cas proposition nels Nous commen ons par consid rer le plus simple des syst mes de d duction naturelle le calcul propositionnel minimal auquel nous ajoutons la contrainte p dagogique de diff rentes mani res Puis nous ajoutons ces syst mes les r gles r gissant la n gation afin de mettre en vidence les propri t s formelles de la contrainte p dagogique face la pr sence de formules absurdes Ensuite nous abordons des syst mes plus complexes dans lesquels la n gation est d finissable le calcul propositionnel du second ordre nous am ne la pr sentation de plu sieurs variantes p dagogiques et l enrichissement de la contrainte initiale les cons quence sur la d finissabilit des connecteurs logiques est tudi e Enfin la contrainte p dagogique est appliqu e aux calculs propositionnels d ordre sup rieurs et les diff rentes variantes de calculs p dagogiques sont tudi s en d tails Dans tous les cas des plus simples aux plus complexes les liens avec les calculs usuels sont mis en vidences des traductions des syst mes usuels
170. p et 1 DTR AT par et 2 4 TH Y8 B T par Vi et 3 5 TH B T par W et 4 6 TH A T par v et 4 7 T A gt y7 B gt 7 At A 7_ par P Hyp 5 et 6 8 T A 7 B 7 AH A par P Hyp 5 et 6 N TASy Boy Arey par gt e 7 et 8 10 TAR A gt 7 B71 97 par 3 et 9 11 TAF YRA 7 B gt 7 77 par Vi et 10 12 TH A Vy A 7 B 79 7 par vi et 11 13 TH A par hypoth se 14 THVy 4A 7y B 7 7 par gt e 12 et 13 15 TH AVB par d finition et 14 Dans le cas de P CP la r gle usuelle ne fonctionne plus Si du jugement T Fe A on veut d river le jugement I Fe AV B la proposition 2 3 10 impose la for mule B d tre motivable mais dans la r gle usuelle la formule B est arbitraire ventuellement non motivable Il faut alors alt rer les r gles d introductions afin 40 2 4 D finition des connecteurs logiques de garantir que la formule introduite est motivable ce que permettent les r gles p dagogiques d introduction de la disjonction Vi et Vir THA Ho B P Vj1 est valide dans P CP Tr AVB Proposition 2 4 6 La r gle D monstration Cette preuve est analogue celle de la proposition 2 4 5 Cepen dant aux lignes 5 et 6 nous devons motiver dans P CP les formules A et B pour appliquer la r gle P Ve la place de la r gle Ve mais A est une formule moti vable dans P CP d apr s la proposition 2 3 9 et B est
171. par une substitution ouverte peut toujours tre motiv e par une substitution close qui pr ciserait l exemple comme on peut toujours choisir un num ral divisible par 2 par exemple 12 pour compl ter une motivation consistant en la donn e d un entier pair quelconque Pouvoir toujours compl ter les motiva tions incompl tes est une propri t souhaitable nous d montrons ci dessous que F CP poss de cette propri t Lemme 2 2 1 Pour toute formule F si o est une motivation de F dans F CP alors pour toute substitution u adapt e ao F la substitution Oc est une motivation de F dans F CP D monstration Par r currence sur n le nombre d l ments de l ensemble VI 0 F n 0 dans ce cas la formule F est close donc u o F o F le jugement o F est d rivable par hypoth se donc le jugement 1 0 F est d rivable 22 2 2 Calcul propositionnel du second ordre faiblement p dagogique n n 1 soient W l ensemble n l ments et a la variable tels que Vl c F W U a par hypoth se le jugement o F est d rivable et nous d rivons le jugement Va o F par la r gle V par hypoth se de r currence le jugement uw Vo o F est d rivable et nous avons uw Ya o F Va uw Oo F car a W par d finition finalement nous d rivons le jugement u oa F par la r gle Ye 2 2 2 Non nullit syntaxique des jugements Dans 31 Nelson introduit le concept d implication
172. plicable AC gr ce l isomorphisme de Curry Howard Nous avons juste be soin de d finir ce qu est une motivation dans le cadre des calculs typ s Une motivation est essentiellement une substitution qu il nous faut alors d finir sur les types mais aussi sur les termes puisqu ils sont annot s par des types D finition 4 2 1 Une substitution o est une application des types dans les types d termin e par un ensemble de variables not Dom o et par une application f des variables dans les types Pour tout type F l image de F par o not e o F est d finie par r currence sur F comme suit FST ao KaTy F a oF f a si a Dom o eto F a sinon F A gt B 0 F 0 A 0 B L ensemble Dom o est appel le domaine de la substitution o D finition 4 2 2 Pour tout terme t et pour toute substitution o l application dea at not e a t est d finie par r currence sur t comme suit t o ot t t az ot t t Ar4u o t dt 4u t u ot oa ud v Les types simples ne contiennent aucune sorte de quantification sur les variables en revanche les variables sont quantifi es par la abstraction il nous faut donc d finir ce que sont les A variables libres et quantifi es D finition 4 2 3 Pour tout terme t l ensemble VI t des variables libres de t est un ensemble de A variables d fini par r currence sur t t 0 VIE t ae VI t r t z u VI t Vi u x t w Vi t
173. poth se de r currence le jugement T F 77A 1 Dy m47 Ay ma FB par P Hyp et le lemme 3 5 2 2 Dy mAy Ay ma Fi mA par P Hyp et le lemme 3 5 2 3 Ty mAy Ay ma Hp y par gt e 1 et 2 4 Ty m4 Ay Fp ma par gt i et 3 5 Dy m4 A Fp L par Vi et 4 6 Py mA pA gt Ll par gt i et 5 7 Ty tyAy Fi 4 L 1 par hypoth se de r currence et P Af 94 3 5 Traductions 8 Dy A Fp Ly par gt e 6 et 7 9 T4 m4 Fp T par P Ax et le lemme 3 5 2 10 1446 par Ve 8 et 9 11 T4 A y Hp y par P Hyp et le lemme 3 5 2 JS SAP gt y par gt i et 11 13 Dy yAy Fp y par gt e 10 et 12 14 Ty m4 par gt i et 13 ainsi le jugement I Fi m44 est d rivable d apr s le lemme 3 5 5 le juge ment l F5 0 A A nous avons 0 A A ainsi nous d rivons le jugement T Hp A a l aide de la r gle Ext Pour d montrer la seconde moiti de la propri t de pr servation de la d ducti bilit par y traduction nous faisons appel aux deux lemmes qui vont suivre pour tout pr dicat P nous notons P le pr dicat y 1 P et O1 P le pr dicat y L O P Proposition 3 5 12 Soit n un l ment de 2 w et T un ensemble de formules Pour tout pr dicat P k d ordre n le jugement THE P P est d rivable D monstration Par r currence sur P P T lejugement I FE T T est ais ment d rivable P
174. pposons que le jugement Va a soit d rivable Le ju gement Vy Va y a est d rivable d apr s la proposition 2 2 11 ce qui est absurde compte tenu de la consistance de F CP Ce r sultat peut para tre tonnant compte tenu de la d rivabilit de H L Va a On constate alors que la quantification universelle ne commute pas avec l implication pour toutes formules F et G telles que a VI G la formule Va F G n est pas quivalente la formule F Va G M me si L ne d finit pas l absurde dans F CP nous ne savons pas si il existe une formule B telle que Vy B y Si une telle formule existe alors elle est quivalente la formule Va T a 1 H Ya B par hypoth se 2 A B aH Ya B a par P Hyp et 1 3 otre B y par Ve et 2 4 Va f gt a gt 6 gt y par gt i et 3 5 2 y6 Va 8 a By par Ye et 4 6 F Va T a T gt y par Ve et 5 7 H2 Yvy 8 T y y ais ment d rivable 8 H Va T gt a y par instantiation de 7 et 6 30 2 3 Calcul propositionnel p dagogique du second ordre 9 F Vy Va T a y par vi et 8 La m thode utilis e pour montrer que Va a ne d finit pas l absurde ne peut mal heureusement pas tre appliqu e Va T a contrairement Va a la formule Va T a est d composable sous la forme B U V avec U 4 Va T gt a ona par exemple Va T
175. py Py uP P V A le jugement T FP u V69 4 u VG A est ais ment d ri vable par a quivalence nous pouvons supposer que q ainsi nous avons u VB0 A VB u A donc nous avons une d rivation du ju gement HP vO AN V3 u A le jugement T F u A 1 A est alors ais ment d rivable par hypoth se de r currence le jugement PP uy Ay u A est d rivable ainsi le jugement I FP pA uA est d rivable l aide de la r gle Ext le jugement T P Y6 uy Ay VB u A est alors ais ment d rivable nous avons ny VBA V0 uy A ainsi nous avons une d rivation du jugement T H uw VB A poe 89 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur w VB A nous avons alors une d rivation du jugement FP uy Py Hel P 6 A analogue au cas pr c dent P AB analogue au cas P A gt B De m me il est souhaitable que la y traduction et l galit extensionnelle com mutent Lemme 3 5 7 Soient n un l ment de 2 w et T un ensemble motivable dans P CP Soient P k et Q k deux pr dicats Soient y une variable fraiche pour T U P Q Si le jugement IT F5 P Q est d rivable alors le jugement PhS Py x Q est d rivable D monstration Par r currence sur kK k x supposons que le jugement T H P e Q soit d rivable soit une variable fraiche pour F U P Q par d finition
176. querait l incoh rence du calcul A nsi la m thode de p dagogisation ayant engendr F CP ne convient pas En revanche la m thode qui a servi pour construire le calcul P CP convient parfaitement nous allons l appliquer AC 114 5 2 A calcul p dagogique du second ordre Soient un contexte F un type o une substitution u une A substitution et id un identifiant On note H2 o F les jugements de la forme HZ t o F De m me les ensembles de jugements H 0 F avec x F T sont not s 2 o T On d note l ensemble des jugements H u z o F avec x F T par F p o F Voici maintenant la d finition de la version p dagogique de C D finition 5 2 1 Le calcul p dagogique du second ordre abr g en P XC est d fini par sa morphologie constitu par l ensemble des jugements de la forme T ip F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles gt i gt e Vi et a ainsi que des trois r gles suivantes pees i p P Fiap os T PTE xv Fer HoT rH g F P Hyp Fit Ya A Fip oU rE awa PY On dit qu un jugement T a t F est d rivable quand il existe une d rivation dans P XC dont la derni re r gle utilis e produit ce jugement La notion de motivation est imm diatement transposable dans P C D finition 5 2 2 Soit C un calcul dont la morphologie est constitu par l ensemble des jugements de l
177. r s le lemme 3 4 6 a U P est motivable par o dans P CP ainsi a V P est o UTM dans P CP P B A analogue au cas pr c dent P AB analogue au cas P A gt B Les deux lemmes qui suivent sont li s au cas de la r gle a Lemme 3 4 16 Soient n un l ment de 2 w et o une substitution triviale dans P CP Pour tout pr dicat P et pour tout pr dicat U d rivable dans P CP si P est o a Q U UTM dans P CP alors a y P est o y U UTM dans P CP D monstration Par r currence sur P P T nous avons a y P T donc a y P est o y y U UTM dans P CP P deux cas se pr sentent a nous avons a y P y donc a y P est o y y U UTM dans P CP B a nous avons a y P et 8 Dom o car P est o a U UTM dans P CP donc a y P est o 7 U UTM dans P CP P A B imm diat par r currence sur A et B P VBF A supposons que P soit o a U UTM dans P CP soit V un pr dicat d rivable dans P CP par a quivalence on peut supposer que a Dom o U a ainsi A est o a U 8 V UTM dans P CP par hypoth se de r currence a 7 A est o y y U B V UTM le jugement FF low yW a P est d rivable dans P CP car o y U a 6 P o a a U P ainsi a y P est o y U UTM dans P CP P A analogue au cas pr c dent P AB imm diat par r currence sur A et B 78 3 4 Calculs
178. r Publications N Y 1963 D Prawitz Natural Deduction a Proof theoretical Study Almquist and Wiksell Stockholm 1965 A S Troelstra and D Van Dalen Constructivism in Mathematics an In troduction Studies in Logic and the Foundations of Mathematics North Holland 1988 volume 2 V Valpola Ein System der negationslosen Logik mit ausschliesslich reali sierbaren Pradicaten Acta Philosophica Fennica 9 1955 pp 1 247 J Van Heijenhoort From Frege to G del a source book in mathematical lo gic 1879 1931 Harvard University Press Cambridge Massachusetts 1967 P G J Vredenduin The Logic of Negationless Mathematics Compositio Ma thematica 11 1953 pp 204 277 133
179. r toute formule F close et o UTM dans P CP le jugement F F est d rivable si et seulement si le jugement F F est d rivable D monstration la formule F est close et UTM dans P CP donc le jugement H F est d rivable lt supposons que le jugement Hp F soit d rivable P CP est un sous syst me de CP donc le jugement F est d rivable 3 5 Traductions Nous introduisons ici une traduction inspir e d une part de la A traduction de Friedman 10 et d autre part des traductions n gatives de G del Kolmogorov Kuroda servant a plonger le calcul propositionnel classique dans la logique mini male Notre but est de montrer que les calculs CP et P CP sont quivalents modulo notre traduction Nous commen ons par d finir les calculs propositionnels classiques d ordre sup rieur D finition 3 5 1 Pour tout n l ment de 2 w le calcul propositionnel classique d ordre n abr g en CCP est d fini par sa morphologie constitu par l ensemble des jugements de la forme T F F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles Ax Hyp gt i gt e Vi Ve a et Ext ainsi que de la r gle suivante ese ae TRF Oo 83 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur Le calcul CCP est galement appel le calcul propositionnel classique d ordre sup rieur On
180. re A gt B B est d rivable donc nous avons une d rivation du jugement 7 T A B ThrA gt B THA a rH B ras 1 HEH VE Vat VE gt a gt p F gt F gt 8 imm diat 2 FH T A B T A T 8B par v et 1 par hypoth se de r currence le jugement Ht T A gt 63 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur TT A B par hypoth se de r currence Hi P A gt PB par gt e 2 eb 3 TT A par hypoth se de r currence eH T B par 4 4et5 THA ag VT reya M 1 HH Wak VE Var R gt a F Va a ais ment d rivable 2 HH T Aaf Aja T Va Aa A a par Ve et 1 3 HH T A T gt Ya A par 5 et 2 4 H T A par hypoth se de r currence 5 HeH T Vaf A par gt e 3 et 4 T F Va A repoa Lo Lee VE NE T Va da SU ais ment d rivable 2 Hitt T Ya Aa Aja T Aa A U par Ve et 1 3 H T Va A gt T a U A par et 2 4 HIT Ya A par hypoth se de r currence 5 HH T a U A par 3 et 4 rH A A B rH B A est d rivable nous avons A a B par hypoth se donc nous avons F A a T B par la r gle a ainsi nous d rivons le jugement H T B par la r gle a Dr A A B rH B A est d rivable nous avons A B par hypoth se donc nous avons A T
181. re plus le calcul La XXil solution propos e est de remplacer la r gle Ve TE Va A DE nur D par la r gle P V Trk Ya A FoU FH a U A dans laquelle on demande ce que la variable quantifi e soit instanci e par une formule motivable On obtient alors le calcul propositionnel p dagogique du second ordre L alt ration de la r gle Ve est naturelle en consid rant qu un jugement y H F permet de d river un jugement F Vy y F si on remplace y par une formule dans le premier jugement les r gles P Ax et P Hyp lui imposent d tre motivable ainsi la variable y doit tre instanci e par une formule motivable dans le second jugement pour conserver les bonnes propri t s des syst mes p dagogiques Dans le syst me obtenu l absurdit dispara t compl tement dans le sens o aucune formule apparaissant dans une d rivation ne peut contenir une sous formule non motivable on dit que les formules sont h r ditairement motivables Ce syst me a la particularit de pouvoir motiver trivialement toutes les formules motivables une motivation triviale est une substitution rempla ant les variables propositionnelles par des formules prouvables en particulier toute formule motivable est motivable par la substitution rempla ant toutes les variables par T Ce r sultat est mettre en parall le avec remarque de Heyting dans 20 sugg rant que dans un syst me formel sans n gation seules les proposition
182. rence sur P que le jugement H5 7 T P est Du T y T T T et le jugement Ly T est d rivable avec la r gle Ax a d apr s le lemme 3 5 1 le pr dicat a est motivable dans P CP par la aibsttution y T P A B 1 FS y T A par hypoth se 2 FS ly T B par hypoth se 3 M TI B MATT A Fp MATTB par P Hyp 1 et 2 4 y T B Fp DATI A B par i et 3 5 6 Pp ATI By gt MATI A B par i 4 FS YNT A B par gt e 3 et 2 P Va A par hypoth se de r currence le jugement H y T A est d ri vable Nous avons y a ainsi nous d rivons le bobine Es HATI Va A avec la r gle Vi P a A par hypoth se de r currence le jugement F5 y T A est d ri vable Nous avons 7 a ainsi nous d rivons le jugement H5 y T Ve A avec la r gle V nous avons A Aa A a donc le jugement FF y T Va Aa A a est d rivable par la r gle g ainsi la formule P est moti vable par y T dans P CP P AB soit K gt le genre du pr dicat A par hypoth se de r currence le jugement H y7 T Va A a est d rivable et B est motivable dans P CP donc le jugement 7 T A B est d rivable avec la r gle P V ainsi le pr dicat P est motivable par y T dans P CP 85 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur Les deux lemmes suivants servent prouver que notre double pseudo
183. rme t est utile dans C quand U Aa z Val F Le terme t est inutile dans C quand il n est pas utile On se rend compte imm diatement qu il existe des termes inutiles dans C en particulier ceux qui font intervenir des types absurdes Proposition 5 4 4 Il existe un terme inutile dans XC D monstration Le jugement F Art x L L est ais ment d rivable comme AC est coh rent il n existe aucun terme u tel que le jugement H2 u L soit d rivable donc le terme x x est inutile dans AC En revanche comme nous le supposions tous les termes apparaissant dans les d rivations de P XC sont utiles On commence par prouver l utilit dans P C de tous les termes clos typables Lemme 5 4 5 Pour tout jugement d rivable Fe t F tel que le terme t soit clos la propri t U t F est v rifi e D monstration Par r currence sur la longueur de F nous pr sentons la r currence par cas sur F F T par hypoth se le jugement Fip t F est d rivable donc U t F F a analogue au cas pr c dent F A gt B A est motivable dans P C d apr s la proposition 5 2 1 comme A est clos il existe un A terme u tel que le jugement ip u A est d rivable donc le jugement FS tu B est d rivable de plus U tu B par hypoth se de r currence ainsi U t F F Va A le jugement se t Va A est d rivable par hypoth se donc le ju gement i tT a T A est d rivable d
184. rmel de mani re tautologique dans notre propre syst me de raisonnement Ce mode de repr sentation a l inconv nient d tre fond sur notre propre syst me intuitif de repr sentation alors que paradoxalement le syst me formel est destin pallier les imperfections de l intuition On est alors conduit valider le syst me formel sur la base d un m ta syst me strictement plus puissant notre propre syst me de raisonnement qui doit tre valid par un m ta m ta syst me encore plus puissant qui doit lui aussi tre valid par etc Le principe m me de ce mode de repr sentation bien que math matiquement correct est ontologiquement mal fond En particulier il permet de justifier certaines r gles du syst me par leur simple pr sence dans le m ta syst me prenons l exemple de la r gle du tires exclu qui permet de d duire la formule V A pour toute formule A s mantiquement elle signifie que tout mod le est soit un mod le de A soit un mod le de A Ceci entre en d saccord avec l existence de formules ind cidables dans le cadre de syst mes suffisamment expressifs par exemple l arithm tique de Peano il existe une formule G admettant un mod le et telle que G admette galement un mod le quand une telle formule G correspond l nonc de la validit d une formule dans un mod le donn il n est plus possible de prouver que ce mod le satisfait A ou A Bien s r on peut tudi
185. rrence sur x k x nous avons P P et o P o P par d finition donc o P a P k 0 gt oP o Va Pa Vaf o Pa Va o Pa par hypoth se de r currence Va o Pa car a Dom c oP Comme la transformation P constitue une formule repr sentant P du point de vue de la motivabilit il est n cessaire qu elle ne change pas le sens des pr dicats en particulier par rapport la G quivalence 60 3 2 Calculs propositionnels faiblement p dagogiques d ordre sup rieur Lemme 3 2 2 Soit k un genre Pour tout pr dicats P k et Q k si P 5 Q alors P g Q D monstration Par r currence sur k x nous avons P P et Q Q donc P Q pets tv 1 P Q par hypoth se ao 0 g par os ND 3 Pa Qa par Bapp 1 et 2 4 Pa Qa par hypoth se de r currence 5 Va Pa s Va Qa par By et 4 Ainsi P Q Voici donc comment on d finit les motivations des pr dicats D finition 3 2 3 Soient n un l ment de 2 w et C un calcul dont la morpho logie est constitu e par l ensemble des jugements de la forme F F Pour tout ensemble de pr dicats une motivation de A dans C est une substitution o telle que les jugements H oT soient d rivables Quand un ensemble de pr dicats admet une motivation dans C on dit qu il est motivable dans C De plus une motivation d un pr dicat P dans C est une motivation du singleton P dans C Chaque motivatio
186. rs conduits contraindre la relation de quivalence pour ne pas qu elle puisse d composer des pr dicats motivables en plusieurs pr dicats ventuellement non motivables D finition 3 3 1 Soit C un calcul dont la morphologie est compos e des juge ments de la forme TH avec n un l ment de 2 w et id un identifiant textuel Pour tous les pr dicats P et Q la relation de B quivalence entre P et Q not e P Q est d finie par les r gles Gr Brar Gea By 2 Papp Bsym el Bixans ainsi que de la r gle suivante Fis o Va A me o B a A B p a B A P Gred Quand la relation P p Q est v rifi e on dit que les pr dicats P et Q sont p quivalents Compte tenu de toutes ces observations nous sommes en mesure de d finir des calculs p dagogiques d ordre sup rieur dans lesquels nous verrons cela plus loin tout sous pr dicat P tel que la formule P soit absurde dispara t des formules apparaissant dans les d rivations 66 3 3 Calculs propositionnels p dagogiques contraints d ordre sup rieur D finition 3 3 2 Pour tout n l ment de 2 w le calcul propositionnel p dago gique contraint d ordre n abr g en PC CP est d fini par sa morphologie constitu par l ensemble des jugements de la formeT Fps F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles P Ax P Hyp i e Vi et a a
187. s P CPM toutes les formules sont motivables par T Le lemme 2 3 9 nous permet de montrer qu il en est de m me dans P CP la diff rence que dans P CP il n y a que les formules motivables qui le sont par T c est dire toutes les sous formules des formules contenues dans les d rivations de P CP 36 2 4 D finition des connecteurs logiques Proposition 2 3 10 Pour tout jugement T F F d rivable les jugements H G7 sont d rivables pour toute sous formule G d une formule appartenant T U F D monstration Soit G une sous formule d une formule dans F U F D apr s la proposition 2 3 9 la formule G est HTM dans P CP il existe une substitution o triviale dans P CP telle que Be a G soit d rivable D apr s le lemme 2 3 5 le jugement F Tipom oyG est d rivable Par la proposition 2 3 2 2 7 G est d rivable Ainsi F2 Gr est d rivable Ce r sultat nous permet d affirmer l instar de Heyting 20 mais pour des raisons totalement diff rentes que seules les propositions vraies apportent du sens dans les logiques propositionnelles sans n gation On notera qu la diff rence de Heyting nous pensons que les logiques propositionnelles sans n gation ont un contenu tr s riche et sont aussi expressives que les logiques propositionnelles usuelles ce que nous v rifierons dans la section 2 5 Comme toutes les formules motivables sont motivables par une substitution commune par exemple la subst
188. s libres a par les pr dicats T d finis ci dessous D finition 3 4 4 Pour tout genre k le pr dicat T est d fini par r currence sur K Keer TieT K t gt 0 7 A To Nous observons que le pr dicat T est de genre k Pour toute formule F nous crivons Fr la formule F dans laquelle toute variable libre a est remplac e par T Une substitution triviale est une substitution dont toutes les formules constitutives sont d montrables Dans le chapitre 2 nous avons introduit la notion de formules h r ditairement trivialement motivables c est a dire des formules dont toutes les sous formules sont motivables par une substitution triviales I est fr quent pour prouver un th or me sur une propri t simple de faire appel a des propri t s plus complexes c est notre cas ici car pour montrer que toutes les sous formules dans les d rivations des calculs P CP sont motivables par T il faut prouver un r sultat plus fort que toutes les formules dans les d rivations sont uniform ment trivialement motivables Une formule est uniform ment moti vable quand toutes ses sous formules sont motivables par des motivations dont les objets associ s aux m mes variables sont identiques ceci signifie qu une moti vation uniforme associe les m mes exemples aux m mes variables quelque soit la sous formule Comme les motivations uniformes sont tr s proches de la structure des formules elles permettent de mener des preuve
189. s plus naturelles D finition 3 4 5 Soient n l ment de 2 w et C un calcul dont la morphologie est constitu e par l ensemble des jugements de la forme T F F Pour tout pr dicat P et pour toute substitution o triviale dans C on d finit par r currence sur P la propri t d tre uniform ment trivialement motivable par a abr g en o UTM dans C P T Pesto UTM dans 70 3 4 Calculs propositionnels p dagogiques d ordre sup rieur P a sia Dom o alors P est o UTM dans C P A B sico motive P dans C et si A et B sont o UTM dans C alors P est o UTM dans C P Va A sia motive P dans C et si A est o q a U UTM dans C pour toute formule U d rivable dans C alors P est o UTM dans C P da A sia motive P dans C et si A est o a a U UTM dans C pour toute formule U d rivable dans C alors P est o UTM dans C P AB sio motive P dans C et si A et B sont o UTM dans C alors P est o UTM dans C On d montre ci dessous que la composition de deux substitutions triviales est une substitution triviale Proposition 3 4 1 Soit n un l ment de 2 w Pour toutes substitutions o et u triviales dans P CP telles que pour tout a Dom o la substitution u soit adapt e aux formules o a la substitution u est triviale dans P CP D monstration Soit a Dom yu a deux cas se pr sentent Dom a par hypoth se le jugement F o a est d rivable posons Dom u Hf 1 lt i
190. s propositionnels p dagogiques d ordre sup rieur 1 r P F5 P par P Hyp et le lemme 3 5 2 2 T P H Py par P Hyp et le lemme 3 5 2 3 T P Py Fp y par gt e 1 et 2 4 T P H T n P par et 3 a p P par gt et 4 donc le one T F P 6 P est d rivable ainsi le jugement FS 0 P P est darable P Va A nous avons O Va A Vat A et Yat A Va A 1 l n Vat A 4 Vat A Fp Ya A par P Hyp et 3 5 2 2 T Ya A Aly Va A Fi 2 T par P Ax et 3 5 2 3 T Va A Ay Ya A Hn A par P V 1 et 2 4 T Vat A mAy Ya A Fp yA par P Hyp et 3 5 2 5 T Ya A mAy Ya A Fp 7 par gt e 3 et 4 6 P Wa A 4 Fp Va A par gt i et 5 7 T m Ya A mA Fp mva A par P Hyp et 3 5 2 8 T m Yat A mAy Fp Y par gt e 6 et 7 9 T Ya A Fp tage par et 8 10 T Va A Fp 4 A par hypoth se de r currence 11 T Wa A Fp A par Ce 9 et 10 12 T Ya A F5 Va A par Vi et 11 13 T F5 r Va A gt Va A par gt i et 12 donc le seneni rT Hi O P Py est d rivable comme dans le cas pr c dent le jugement TF Py 6 P est d rivable ainsi le jugement T Hi O P Py est d rivable P da A nous avons a A Aa A et O Aa A Aa 0 Va A O a par hypoth se de r currence le jugement T Hp O A est d rivabl
191. s vraies cr ent du sens La signification de cette remarque se trouve alors pr cis formellement par la propri t qu ont les formules d tre h r ditairement trivialement motivables Cette fois ci le A calcul associ normalise On peut galement plonger le calcul usuel dans le calcul p dagogique laide d une traduction des formules la contrainte p dagogique n occasionne alors aucune perte d expressivit Afin d achever l tude des syst mes p dagogiques propositionnels il ne restait plus qu consid rer les calculs propositionnels d ordre sup rieur Comme dans le cas du second ordre le premier syst me construit fut le calcul propositionnel d ordre sup rieur faiblement p dagogique obtenu partir du calcul intuitionniste usuel et des r gles P Ax et P Hyp Dans ce syst me tous les th or mes du calcul usuel sont des th or mes du calcul faiblement p dagogique Mais on a vu que certains th or mes du second ordre ne sont pas des th or mes p dagogiques du second ordre La raison est que chaque th or me l ordre n est un th or me p dagogique l ordre n 1 il y a toujours un cart d exactement un ordre ainsi tous les th or mes du second ordre sont des th or mes p dagogiques au troisi me ordre mais pas en dessous Comme dans le cas du calcul p dagogique minimal naif ce qui est vrai pour les th or mes est faux pour les jugements la P V xxiii Pr sentation sy
192. semble F N M est habit A Z N d apr s le lemme 1 2 5 nous avons M et par hypoth se nous avons B Ny donc A gt B N ainsi par hypoth se de r currence sur TH A B l ensemble F N M est habit Comme la formule T est dans M elle se comporte comme une formule r futable plus pr cis ment si T est d rivable sous un ensemble non vide d hypoth ses alors l une des hypoth ses est dans M mais dans certain cas une telle hypoth se ne peut advenir sans contradiction dans le cas par exemple ou elle est la formule T T Le jugement T TH T n est donc pas d rivable 9 CHAPITRE 1 Calculs propositionnels p dagogiques du premier ordre Proposition 1 2 7 Le jugement T TH T n est pas d rivable D monstration Nous avons T Me donc d apr s le lemme 1 2 6 nous avons T T Nr Comme T Me nous avons T T N done T T Mt d apr s le lemme 1 2 5 ce qui est absurde 1 2 2 Tentative am lior e Le comportement du calcul N CPM ne poss de pas des propri t s souhaitables puisque toutes les formules sont motivables dans N CPM on s attend ce que tous les jugements d rivables dans CPM le soient galement dans N CPM Le probl me est caus par la r gle N Ax en effet cette r gle contraint beaucoup trop les contextes des jugements qu elle permet de d river elle les contraint tre vide Pourtant il suffira
193. st cens e repr senter peut causer des d g ts mat riellement et humainement tr s co teux La vivacit correspond une propri t dynamique du programme un programme ne faisant rien est trivialement s r mais n est d aucune utilit on souhaite alors que les programme v rifie fatalement certaines propri t s un moment donn de son ex cution L expression des propri t s de vivacit n cessite g n ralement la for malisation de la mani re dont s ex cute le programme en utilisant par exemple des traces d ex cution mais les syst mes formels usuels ne disposent d aucun moyen de repr sentation de la mani re dont un programme s ex cute ils ne rendent compte que de ce que calcule le programme La plupart des syst mes formels comme la m thode B ou le calcul des constructions inductif ne disposent que d outils garan tissant la s ret celle ci merge naturellement de tout syst me formel suppos cor rect les autres propri t s tant tr s difficilement exprimables Certains syst mes de certification comme TLA permettent de rendre compte des propri t s de viva cit Mais aucun syst me ne dispose de m thodes int gr es concernant la coh rence des sp cifications Faire appel un syst me formel positif afin de certifier les pro grammes offre la garantie de la coh rence des sp cifications puisque les formules y apparaissant sont justifi es par un objet les satisfaisant Cet objet fournit un o
194. t Aau ot Ad o q u t uA o t oa uo A Puis nous d finissons les substitutions sur les A termes D finition 5 1 12 Une A substitution o est une fonction de domaine fini Dom c valeurs dans l ensemble des termes Pour toute A substitution on note VI o l union des ensembles Vl o x pour tout x Dom o D finition 5 1 13 Pour toute substitution o et pour tout A terme t on dit que o est adapt e at quand l ensemble VI o N Vaq t est vide D finition 5 1 14 Pour tout terme t et pour toute substitution o adapt e t l application de o at not e a t est d finie par r currence sur t comme suit t o oat 0 TE E o x si x Dom o x sinon t Ar4u ot ALOU t w ot 0 u0v t Aau Of a u t uA o t o uA Le syst me fonctionnel associ au calcul CP doit contenir une notion de contexte pour qu il reste en accord avec la structure des systemes de d duction naturelle a la Gentzen Parwitz 112 5 1 A calcul du second ordre D finition 5 1 15 Un contexte propositionnel du second ordre est un ensemble fini de couples x A ou x est une variable et A un type tel que pour tout x A ET et pour touty BET six y alors A B dans ce chapitre nous les appelons contextes quand aucune ambiguit n est craindre Un X jugement propositionnel du second ordre est un triplet not T H t F avec T un contexte t un A terme F un type et id un identifiant textuel Dans
195. t bom y Dom o alors wo F p Oo F D monstration Par r currence sur F F T nous avons p o T T et T pOa T donc p o T pOa T F a trois cas se pr sentent a Dom o nous avons a Dom u Dom o done u o a wOo a par d finition de a Dom u Dom o nous avons a Dom o donc oa a poa wa et ainsi 0 np c a par d finition de a Dom u UDom c nous avons woa a et Dom fpOo Dom p U Dom c donc 1 c a a et ainsi o a Oao a F A B par hypoth se de r currence nous avons u o A Hp O o A et u 0 B uOo B donc p o A B pOao A B F Va A deux cas se pr sentent a Dom u nous avons u 0 Va A Va A et pOo Va A Va A donc u 0 Va A u o Va A a g Dom uO nous avons 4 0 Va A Va u o A et par hypoth se de r currence nous avons u 0 O A donc u o Va A Va u o A ainsi u o Va A u o Va A 19 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre Il est fr quent d avoir recours a des variables libres de toute contrainte qui ne sont ni quantifi es et qui n ont aucune propri t impos e de telles variables sont dites fraiches D finition 2 1 8 Une variable fraiche pour une formule F est une variable n ap paraissant pas dans F Par extension une variable fra che pour un ensemble de formules T est une variable fra che pour chacun des l ments de T L ense
196. t hypoth tico d ductif intuitif D finition 1 1 3 Le calcul propositionnel minimal abr g en CPM est d fini par sa morphologie constitu par l ensemble des jugements de la formeT F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles suivantes TE TU 0 m TFF F Ep Tl Ab B Tk A gt B TRA gt gt e Tr A B TF B On dit qu un jugement TH F est d rivable quand il existe une d rivation dans CPM dont la derni re r gle utilis e produit ce jugement Enfin nous proposons un exemple de d rivation afin de rendre plus explicite le fonctionnement du calcul La d rivation choisie est celle du th or me F a a 2 8 correspondant la r gle du modus ponens Exemple d rivation du jugement F a gt a 6 L 1 a a gt BF a gt p par Hyp 2 aa gt BF a par Hyp 3 a a Bk 8 par 1 et 2 a 4 at a gt 8 b par et 3 5 Fna a B gt B par 3 et 4 1 2 Calcul propositionnel p dagogique minimal 1 2 Calcul propositionnel p dagogique minimal 1 2 1 Tentative initiale L id e initiale pour p dagogiser CPM est de remplacer la r gle Hyp Fer Tr r yp par la r gle P Hyp Fer For TEF P Hyp avec g une substitution op rant sur les formules contenues dans I Il nous faut alors d finir ce qu est une substitution D finition 1 2 1
197. t P k pour tout ensemble T motivable dans P CP et pour toute variable y fraiche pour P le jugement VFS O P Py est d rivable D monstration Par r currence sur P P T nous avons T T et 0 T T y 7 ainsi le jugement LP top T est ais ment d rivable nous d rivons alors le jugement rhe 0 P Py l aide de la r gle P Aff P a nous avons a O a et O a 0 0 a ainsi le jugement FS O P Py est d rivable d apr s le lemme 3 5 3 P A B nous avons 0 A gt By n 4 gt B et A gt B A gt By 1 T 4 gt B A B 4 gt B H A gt B par P Hyp et 3 5 2 2 T A gt B Ay By A gt B Fp A4 par P Hyp et 3 5 2 3 T A gt B A B A B E y par gt e Let 2 4 T A gt B Ay B7 A gt B Fp 7B par P Hyp et 3 5 2 5 T A gt B p Ay By A gt B EST par e 3 et 4 6 T A gt B 4 BF A gt B par et 5 7 T A gt B Ay B Fp A gt B par P Hyp et 3 5 2 8 T A gt B A mB Fp Y par gt e et 7 9 T A gt B A4 Fp B par gt i et 8 10 T A gt B A F B B par hypoth se de r currence 11 T A gt B 4 Fp By par 9 et 10 12 T yA B Fp 4 gt B par gt i et 11 13 PES A gt B A gt B par i et 12 donc le jugement T Ff 0 P Py est d rivable 87 CHAPITRE 3 Calcul
198. t d rivable Nous d rivons le jugement W F7 avec la r gle V puis nous d rivons le jugement F avec la r gle Ve lt supposons que le jugement F soit d rivable Alors le jugement F est d rivable Nous d rivons le jugement F l aide de la proposition 2 5 6 Ainsi F CP est un calcul qui a la m me puissance expressive que CP compte tenu de la traduction des formules F en F 49 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre 2 5 3 Traduction de CP dans P CP Dans F CP la formule F est une traduction fid le de la formule F mais elle peut contenir des occurrences de la formule L ce qui rend cette traduction inapplicable dans le cas de P CP En remplacement nous d finissons la formule F par la formule Vy F7 On remarque d abord que la traduction de F en F pr serve les th or mes Proposition 2 5 10 Pour toute formule F le jugement H F est d rivable si et seulement si le jugement ES F est d rivable D monstration Deux cas sont consid rer supposons que le jugement H F soit d rivable D apr s la proposition 2 5 8 le jugement Fe FT est d rivable Nous d rivons le jugement Fe F avec la r gle Vi lt supposons que le jugement a F soit d rivable Alors le jugement F est d rivable Nous d rivons le jugement F avec la r gle Ve puis nous d rivons le jugement F l aide de la proposition 2 5 6 Dans
199. t des formules ainsi T U F est un ensemble de formules ie Port T Fa F sont des formules donc d apr s le lemme 1 3 1 les l ments de I sont des formules ainsi I est un ensemble de formules LATE PEAR sont des formules donc U A B est un ensemble de formules PE PE r Ha B T U A B sont des formules donc T U B est un ensemble de formules ie Li par hypoth se de r currence L est une formule ce qui est absurde P Ax par hypoth se de r currence les l ments de o sont des P Hyp par hypoth se de r currence les l ments de o T par hypoth se de r currence les l ments de F U A B e par hypoth se de r currence les l ments de 14 1 3 propos de la n gation Enfin on d montre de m me que les formules dans les d rivations de CPC sont des formules Lemme 1 3 3 Pour tout L jugement d rivable TE F tous les l ments de l ensemble TU F sont des formules D monstration Par r currence sur la d rivation de FF F La d monstration est analogue celle du lemme pr c dent donc nous ne traitons que le cas de la r gle LL Pak ee Pied ce qui est absurde Le par hypoth se de r currence L et F sont des formules L absence du symbole L dans les d rivations de CPI et CPC a une cons quence importante sur les versions p dagogiques respectives de ces syst mes les r gles Li et Le
200. t en elle m me la garantie de l existence du sens des formules et d cident alors qu il n est pas n cessaire de fouiller plus en avant tandis que d autres consid rent que XV Pr sentation synth tique la pr sence d une contradiction ontologique est inadmissible et qu il faut alors abandonner la s mantique fautive au profit d une nouvelle dont la pertinence se raient garantie par certaines propri t s plus contraintes que la simple coh rence formelle L un des principaux probl mes de la s mantique bas e sur les mod les est qu elle pr tend donner un sens aux formules l aide d objets discursifs de m me nature Comme on peut difficilement justifier une proposition par elle m me il devient n cessaire d introduire de nouveaux objets non discursifs rendant compte du sens des formules Le principe du tiers exclu en plus d tre dans certains cas la source d incoh rences ontologiques a la propri t d intervenir dans des preuves de formules du type 2x P x telles qu aucun objet x v rifiant la propri t P ne puisse tre exhib On a alors introduit des syst mes formels ne v rifiant pas le principe du tiers exclu ceux ci sont dits constructifs car si on les utilise pour d montrer une formule 4z P x alors on peut toujours exhiber un objet x tel que P x La preuve d une telle formule se r v le tre le mode d emploi pour construire cet objet x les preuves constructives sont isomorphes des
201. t id le jugement H2 F s crit galement F De plus pour tous contextes I et A le contexte UA est not I A En particulier pour toute formule A le jugement T U A F3 F est not T A F F Dans une formule chaque quantificateur lie une variable une formule de mani re ce que cette variable n ait d occurrences significatives qu l int rieur de la formule sous le quantificateur toute occurrence de la variable quantifi e lext rieur de la formule sous le quantificateur correspond une variable distincte lidentit des symboles tant consid r comme un hasard syntaxique Nous allons introduire les d finitions permettant de distinguer les variables quantifi es des variables non quantifi es D finition 2 1 3 Pour toute formule F l ensemble VI F des variables libres de F est un ensemble de variables propositionnelles d fini par r currence sur F FHT V F Q F a VI F a F A B VI F VI A UVI B F Va A VI F VI A a Par extension pour tout contexte T nous notons VI T l ensemble Jr VIG Quand VI F 9 nous disons que la formule F est close D finition 2 1 4 Pour toute formule F l ensemble Vq F des variables quan tifi es de F est un ensemble de variables propositionnelles d fini par r currence sur F F T ange le F a Vqa F F A gt B Vq F Va A U Va B F Va A Vq F a U Va A Le propre d une variable quantifi e uni
202. tante propositionnelle T la L formule vraie est une L formule la constante propositionnelle L la L formule absurde est une L formule les variables propositionnelles a 3 y sont des L formules si A et B sont des L formules alors A B est une L formule Pour toute L formule F la L formule F L est appel e la n gation de F et elle est not e F On d finit ensuite les contextes constitu s de formules et les 11 CHAPITRE 1 Calculs propositionnels p dagogiques du premier ordre substitutions sur les L formules afin de disposer de tous les objets n cessaires la d finition de calculs sur l implication et la n gation D finition 1 3 2 Les l contextes et les l jugements sont d finis partir des L formules de mani re analogue aux contextes et au jugements voir la d finition 1 1 2 D finition 1 3 3 Les substitutions sont d finis partir des L formules de mani re analogue aux substitutions voir la d finition 1 2 1 en ajoutant que l image de la constante L par une L substitution o est L Il y a essentiellement deux mani res de d crire le comportement de la n gation la premi re correspond la n gation dans les calculs intuitionnistes et la seconde la n gation dans les calculs classiques Dans les calculs intuitionnistes la r gle Li est la seule r gissant le symbole L LE TFF H et elle correspond la formalisation de la r gle du ex falso Elle no
203. th se 5 WYB AY par d finition A 5 WAY par P Ve et 2 o ue A par hypoth se de r currence E V8 u A par V et 4 Par a quivalence nous pouvons supposer que 3 VI U Nous avons alors VB u A p VG A Ainsi nous avons une d rivation de T Es u VB A T Supposons que I Ee u VB A soit d rivable Par a quivalence nous pou vons supposer que 8 VI T U Nous avons alors VB u A u VB A 46 2 5 Traductions 1 The u WG A par P Hyp 2 TH VS u A par d finition 3 T H5 u A par We et 2 4 TH A7 par hypoth se de r currence 5 T 2 u YB A par V 4 et 8 amp VIL 6 PFS y V8 A par d finition Nous pouvons maintenant d montrer que la 7 traduction plonge CP dans P CP et galement dans F CP puisque toutes les d rivations dans P CP sont valides dans F CP Lemme 2 5 5 Pour tout jugement d rivable T F le jugement T7 Es F est d rivable avec y une variable fra che pour T U F D monstration Par r currence sur la d rivation de T H F les cas des r gles et Vi sont imm diats et les cas des r gles Ax et Hyp sont analogues FET Ax d apr s le lemme 2 5 3 les jugements 7 T F 7 sont d ri vables Ainsi le jugement F7 H2 T7 est d rivable avec la r gle P Ax T H Va A T a U A Ve est d rivable D apr s le lemme 2 5 3 le jugement Fe y T U7 est d rivable Ainsi le j
204. tilise un jeu de r gles d inf rence un peu plus simple que celui de Nelson au prix d une nouvelle complication chaque d monstration se mue en un couple 01 02 de d monstrations men es dans un syst me interm diaire a2 servant d river direc tement le th or me recherch c servant garantir la non nullit des implications d riv es en d montrant la cl ture existentielle de la conjonction de toutes les sup positions apparaissant dans c1 Krivtsov proposa une traduction des syst mes in tuitionnistes usuels dans ses syst mes sans n gation Dans le cas de l arithm tique sa traduction est bas e sur le fait que l implication usuelle B est quivalente la formule Vx AV x 0 BV x 0 qui peut tre crite A gt B puisque la formule AV x 0 est d montrable pour x 0 Il met ainsi en vidence que l aban don de la n gation ne gr ve en rien l expressivit des syst mes formels Cependant une traduction syst matique des th or mes usuels ne permet pas d obtenir coup s r un th or me pertinent dans un syst me sans n gation sans compter le sens modifi des connecteurs logiques quantifi s Valeriya Mezhlumbekova 27 s est inspir e des travaux de Nelson afin de cons truire une arithm tique sans n gation Elle reprend et modifie le syst me de Nelson bas sur l implication quantifi e et elle l enrichit avec des fonctionnelles du syst me T de G del Elle d montre alors qu
205. tion htm Table des mati res Remerciements Introduction Pr sentation synth tique I Syst mes formels p dagogiques 1 Calculs propositionnels p dagogiques du premier ordre 1 1 Rappels sur le calcul propositionnel minimal 1 2 Calcul propositionnel p dagogique minimal 1 2 1 Tent tive initiale o ss Avie pere el de ef em he a ee Ad 1 2 2 Tentative am lior e 1 3 propos de la n gation ooa oaa hee ee ee eA 1 3 1 Calculs propositionnels classiques et intuitionnistes 1 3 2 P dagogisation de la n gation 2 Calculs propositionnels p dagogiques du second ordre 2 1 Rappels sur le calcul propositionnel du second ordre 2 2 Calcul propositionnel du second ordre faiblement p dagogique 2 2 1 Pr sentation du calcul 54e Re be oe gS 2 2 2 Non nullit syntaxique des jugements 2 2 3 La r gle d affaiblissement 2 2 4 Va a ne d finit pas l absurde nee 4 444 use 2 3 Calcul propositionnel p dagogique du second ordre 2 3 1 Pr sentation du calcul 4504 8 a ee a ke A A Mr 2 3 2 Non nullit syntaxique des implications 2 4 D finition des connecteurs logiques 24 1 JOOMORCHON Le M Yea dia ea eee Da ee De ae Bs DAD DIJON a s UNS eke bien ee A ae A A a ne ill vil xi TABLE DES MATIERES DAS TEXISGENCE voei me a Se eee Se Ae
206. titution triviale dans C un contexte I est h r ditairement trivialement motivable HTM dans C quand l ensemble de toutes les sous formules des l ments de T est TM dans C Pour toute formule F nous crivons Fr la formule F dans laquelle toutes les variables libres sont remplac es par T On montre tout d abord dans les deux lemmes qui suivent que le calcul P CP partage des propri t s avec F CP Lemme 2 3 1 Pour tout jugement T Ee F d rivable et pour toute substitution o triviale dans P CP adapt e aux l ments de T U F si o est une motivation de T dans P CP alors o est une motivation de F dans P CP D monstration La d monstration est analogue celle du lemme 2 2 3 Quelques pr cautions doivent tre prises lors de l utilisation de la r gle P V la place de la r gle Ve comme la substitution est suppos e triviale dans P CP elle peut tre utilis e sans danger lors de l application de la r gle P V Lemme 2 3 2 Soit F une formule motivable dans P CP par la substitution o Pour toute substitution u triviale dans P CP la substitution 1 o est une moti vation de F dans P CP D monstration La d monstration est analogue celle du lemme 2 2 1 Quelques pr cautions doivent tre prises lors de l utilisation de la r gle P V la place de la r gle Ye comme la substitution u est suppos e triviale dans P CP elle peut tre utilis e sans danger lors de
207. tout identifiant id le jugement 0 H4 t F s crit galement t F De plus pour tous contextes I et A le contexte TUA est not I A En particulier pour tout type A le jugement TU A i t F est not T A H t F Nous avons alors tous les p requis n cessaires a la d finition du A calcul simplement typ D finition 4 1 4 Le calcul simplement typ abr g en AC est d fini par sa morphologie constitu e par l ensemble des jugements de la forme T H t Dre sa syntaxe constitu e par l ensemble des d rivations d finies par r currence l aide des r gles suivantes mhar z Fer THaiF Em Ll 2A PEEB rHt 4 B PER rHarit A B T Hi tu B s On dit qu un jugement T H1 t F est d rivable quand il existe une d rivation dans AC dont la derni re r gle utilis e produit ce jugement Les d rivations y sont analogues celles du calcul CPM except qu elles servent typer des A termes Exemple d rivation du jugement H a a 3 3 l a y a BHiy a par Hyp 2 x a y a fBHix a par Hyp 3 za y a gt Br yxB par gt e 1 et 2 4 x a Ht y 8 yx a B B par gt i et 3 5 H Azt Ay yx a a B B par et 4 103 CHAPITRE 4 calcul p dagogique simplement typ 4 2 calcul p dagogique simplement typ La m thode de p dagogisation introduite dans le chapitre 1 est directement ap
208. typables par F dans AC puisse tre typ par F7 nous devons les modifier selon la transformation CPS suivante bas e sur la traduction CPS en appel par nom de Plotkin 33 D finition 5 5 2 Pour tout jugement d rivable T H t F nous d finissons la traduction CPS t du terme t par r currence sur la d rivation de T H t F les variables k et m utilis es dans cette d finitions sont deux variables distinctes fra ches pour t Ax o Ak ko PR os T x Fer 5 ie ES eer Hyp x Ak xk Pc Arif B JA f E A B T AY py Toast Ae gt i Act f Ak 110 F ae ea et oan THS fg F DEA aE VID ka E Teena ved O Aho TH f Va A TF fU a U A TH t G CGT E te DF F aje tat Sy fg Ak JR En v ee Val a U A EEX mA mU K 124 5 5 Traduction CPS Les traductions CPS ont la propri t de ne pas alt rer la relation de G quivalence deux A termes sont quivalents si et seulement si leurs traductions CPS le sont De plus l valuation des termes est correctement simul e par l valuation de leurs traductions CPS L tude complete de ces propri t s d passe le cadre de cette th se nous encourageons le lecteur se r f rer aux travaux men s dans 1 9 30 et 35 Le r sultat principal de cette section est contenu dans la proposition 5 5 6 pour tout jugement d rivable H t F le jugement 7 se t FT est d rivable Compte tenu des propri
209. u til suppl mentaire de certification qui permet de construire les sp cifications par raffinement et de v rifier chaque tape l ad quation de la sp cification avec le dispositif r el piloter il constitue un prototype formel de l appareil sp cifier De plus l absence d absurdit permet d imposer une forme affaiblie de vivacit que nous appelons l utilit supposons qu un programme v rifie une propri t l existence de t moins rendant compte des sp cifications est conserv e quel que soit l tat d ex cution du programme c est dire que l existence de t moins cor XIX Pr sentation synth tique respond l existence d un raffinement de l environnement d ex cution tel que le programme v rifie la propri t on obtient dans tous les cas la garantie que tout tat du programme peut tre atteint dans un environnement d ex cution ad quat Dans le cas de la vivacit on demande ce qu un tat du programme soit fatale ment atteint tandis que dans le cas de l utilit on demande ce qu un tat du programme puisse tre atteint Dans les syst mes positifs les programmes sont utiles quel que soit la propri t exprim e Les syst mes p dagogiques L origine des syst mes p dagogiques remontent au milieu des ann es 1980 Dans le m moire de DEA de Lo c Colson 5 on peut lire dans la conclusion la description informelle de ce qui deviendra vingt ans plus tard l objet
210. ugement T7 Fe a U7 A7 avec la r gle P V Ainsi d apr s le lemme 2 5 4 le jugement 7 H2 a U A est d rivable THA A B rH B d apr s le lemme 2 5 1 nous avons A B et ainsi nous d rivons 7 Fe BY avec la r gle a par hypoth se de r currence le jugement 7 Es Va A a par hypoth se de r currence T7 a A est d rivable Il nous reste d montrer la r ciproque du plongement de CP dans P CP via la y traduction D finition 2 5 2 Pour toute formule F nous d finissons la formule F comme tant la formule y L F7 Nous montrons alors que les deux formules F et F sont quivalentes CP Proposition 2 5 6 Pour toute formule F le jugement F F est d rivable D monstration Par r currence sur F F T le jugement T T est d rivable 47 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre F a le jugement a a V L est ais ment d rivable F A B d rivons le jugement H A B A B 1 A B Att A par Hyp 2 A B ATH At A par hypoth se de r currence 3 A B Att A par 1et2 4 A B AtFA B par Hyp 5 A B ATFB par 3 et 4 6 A B A F B Bt par hypoth se de r currence 7 A gt B A H Bt par 5et6 8 A gt BH A B par et 7 9 F A gt B A B t par et 8
211. uitivement une fonction sert en tant que programme est utile d s qu on est capable de faire appel son contenu algorithmique pour calculer des objets Pour un A terme cela signifie qu il existe des A termes qu on puisse lui passer en arguments Notons qu un A terme n a apparemment qu un seul param tre celui qui est quantifi par une abstraction ou une A abstraction Cependant les fonctions plusieurs param tres sont repr sentables en consid rant qu une suite d abstractions d finit une suite de param tres par exemple le A terme Aa Ar x peut repr senter une fonction deux param tres a et x Pour 120 5 4 Utilit cela il faut tendre l utilit la lumi re de cette repr sentation en exigeant que toute fonction utile appliqu e a l argument t moin de cette utilit produise une fonction galement utile La d finition de l utilit dans les calculs du second ordre n est pas imm diate car ces syst mes sont impr dicatifs on peut instancier une variable quantifi e par n importe quel type ainsi le terme Aa 1x x d arit deux en apparence se r v le ne pas avoir d arit pr cise en effet si on l applique son propre type Va a a puis lui m me on obtient par r duction le m me A terme Aa Ax x Cette difficult nous a pouss d finir l utilit l aide d un point fixe celui de la propri t d finie ci dessous D finition 5 4 1 Soit
212. une formule motivable dans P CP par hypoth se R gle d limination Dans le cas de F CP la r gle d limination de la disjonction est d rivable THAVB T AHC T BHC TREC Proposition 2 4 7 La r gle Ve est valide dans F CP D monstration Supposons que les jugements FH AVB T AHC etT B HC soient d rivables 1 T AH C par hypoth se 2 TH A gt C par et 1 B C par hypoth se B C par et 3 2Vy A 7 B 7 7 par hypoth se ww Q oe Sa a ee aa NI rs a Age Fas Les os 2 f B gt C C par gt e 2 et 6 C par 4 et 7 O0 Il en est de m me dans le cas de P CP THAVB TAHC T BHC Ve est valide rH C Proposition 2 4 8 La r gle dans P CP D monstration Cette preuve est analogue celle de la proposition 2 4 7 Cepen dant la ligne 6 nous devons motiver dans P CP la formules C pour appliquer la r gle P Ve la place de la r gle Ye mais C est une formule motivable dans P CP d apr s la proposition 2 3 9 Al CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre 2 4 3 Existence Tout comme la conjonction le quantificateur existentiel est un op rateur sans histoire dans les calculs F CP et P CP les r gles usuelles d introduction et d liminations y sont d rivables D finition 2 4 3 Pour toute formule A la formule A est d finie par la formule
213. une variable propositionnelle quelconque Ce calcul bien qu il autorise des occurrences de la formule L semble appartenir la famille des syst mes paraconsistents qui sont des syst mes dits non explosifs dans lesquels aucune formule ne peut impliquer toutes les autres formules Cette propri t de paraconsistence est pour l instant de l ordre de la conjecture en effet la bonne d finition de la n gation dans le calcul faiblement p dagogique est la formule Va T car on montre que si la formule Va G a est motivable 5 est alors la d finition internalis e de l absurde alors elle est motivable par la sub stitution rempla ant la variable 5 par Va T a Malgr le fait que ce calcul soit strictement plus faible que le calcul intuitionniste usuel il existe une traduction permettant de plonger le calcul usuel dans le calcul faiblement p dagogique ainsi le calcul p dagogique ne souffre d aucune perte d expressivit Il subsiste cepen dant un probl me ce calcul n est pas associ un A calcul viable car certaines preuves tel que la d rivation du th or me L n admettent aucune forme normale les programmes y sont alors tr s mal repr sent s Pour obtenir un calcul p dagogique du second ordre ayant de bonnes propri t s en particulier l absence d occurrences de formules non motivables dans les d rivations auquel est associ un A calcul normalisant il est n cessaire de contraindre enco
214. ur T U F D monstration Par r currence sur la d rivation de I F F Fer Ax d apr s le lemme 3 5 2 les jugements 7 y T I sont d ri vables ainsi le jugement T Hp T est d rivable par la r gle P Ax TUF Hyp d apr s le lemme 3 5 2 les jugements F7 7 T Py sont d ri vables ainsi le jugement T Hp F est d rivable par la r gle P Hyp Tr AB TAB d rivable le jugement T F A B est d rivable l aide de la r gle nous avons alors une d rivation du jugement I 5 gt B4 TRASB TRA TFB Ders A gt B et T Fp A sont d rivables le jugement F5 B est alors d rivable l aide de la r gle gt i par hypoth se de r currence le jugement T A F5 B est par hypoth se de r currence les jugements 93 CHAPITRE 3 Calculs propositionnels p dagogiques d ordre sup rieur TH Ya A PF fa U Ve par hypoth se de r currence le jugement T F5 Va A est d rivable ainsi nous avons une d rivation du jugement I Fp Va Ay d apr s le lemme 3 5 2 le jugement FP y T U est d rivable ainsi nous d rivons le jugement I H a U A l aide de la r gle P V d apr s le lemme 3 5 6 le jugement T F5 a U 4 a U A est d rivable nous d rivons alors le jugement I Fp a U A _ avec la r gle Ext TH A ag VIT TF Var A Vi par hypoth se de r currence le jugement T F5 A
215. us permet de construire le calcul propositionnel intuitionniste D finition 1 3 4 Le calcul propositionnel intuitionniste abr g en CPI est d fini par sa morphologie constitu par l ensemble des L jugements de la forme rR F sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles Ax Hyp gt i et gt e ainsi que de la r gle suivante TRF Li On dit qu un L jugement IT F F est d rivable quand il existe une d rivation dans CPI dont la derni re r gle utilis e produit ce L jugement De m me dans les calculs classiques la r gle Le est la seule r gissant le symbole alg Pare L 1 CEE aS et elle correspond la formalisation de la r gle d limination de la double n gation Elle nous permet de construire le calcul propositionnel classique D finition 1 3 5 Le calcul propositionnel classique abr g en CPC est d fini par 12 1 3 propos de la n gation sa morphologie constitu par l ensemble des L jugements de la forme eS sa syntaxe constitu par l ensemble des d rivations d finies par r currence l aide des r gles Ax Hyp gt i et gt e ainsi que de la r gle suivante Fire IE On dit qu un L jugementT F est d rivable quand il existe une d rivation dans CPC dont la derni re r gle utilis e produit ce L jugement Notons que CPC est suffisamment puissant pour que la conj
216. ut pr dicat P et pour toute substitution o adapt e P l application deo P not e o P est d finie par r currence sur P comme suit PS eer ET Petey ae ala sia Dom a a sinon P A gt B 0 P 0 A o B P Va A o P Va o q A P a A oP a 0 q A P AB o P 0 A o B Pour viter toute confusion nous crivons ro F les applications de substitutions de la forme y 0 F Ci dessous nous d montrons que la composition des substitutions est correctement d finissable Lemme 3 1 1 Soient F une formule o une substitution adapt e F et u une substitution adapt e o F Notons u la substitution p o Ht bom y Dom o alors wo F u Oo F D monstration Analogue la preuve du lemme 2 1 1 Nous savons distinguer les variables libres des variables li es mais certaines va riables libres doivent parfois repr senter des objets les plus g n raux possibles cet effet nous introduisons la notion de variables fra ches d ordre sup rieur 56 3 1 Rappel sur les calculs propositionnels d ordre sup rieur D finition 3 1 12 Une variable fraiche pour un pr dicat P est une variable n ap paraissant pas dans P Par extension une variable fraiche pour un ensemble de pr dicats A est une variable fratche pour chacun des l ments de A L ensemble des variables fra ches d un contexte T est not Fr T Les variables quantifi es ne repr sentent que des positions
217. vable D monstration Par r currence sur la d rivation de T F H oT PET le lemme 2 2 10 ainsi nous d rivons T T avec la r gle P Ax 2 B aE a P Hyp cas analogue P Ax T A H B rH A gt B ainsi nous d rivons T H A B par la r gle gt par d finition A B A B donc nous avons une d rivation de H A B THA B THA r B T A B sont d rivables par d finition A B A gt B donc nous avons une d rivation de F A B ainsi nous d rivons T B par la r gle e THA ag VI T H Va A a dans ce cas nous avons une d rivation du jugement L et d apr s la proposition 2 2 4 le jugement L est d rivable ce qui est absurde compte tenu de la concistance de F CP AZ a par hypoth se de r currence le jugement T A est d rivable et ainsi nous d rivons T Va A par application de la r gle Yi par d finition Va A Va A donc nous avons une d rivation de DF Va A T H Va A T a U A est d rivable deux cas se pr sentent a dans ce cas nous avons une d rivation de L ce qui est absurde A a par d finition Ya A Va A ainsi nous avons une d rivation de T H Va A et nous d rivons T a U A avec la r gle Ye d apr s le lemme 2 2 8 nous avons a U A a U A donc nous avons une d rivation de T a U A PRA A B rH B P A
218. versellement est de repr senter de ma ni re uniforme n importe quelle formule Nous avons donc besoin de substitutions D finition 2 1 5 Une substitution o est une fonction de domaine fini Dom o valeurs dans l ensemble des formules Pour toute substitution c on note VI o l union des ensembles VI c a pour tout a Dom o 18 2 1 Rappels sur le calcul propositionnel du second ordre Chaque variable devra pouvoir tre substitu e une formule du moment qu il n y a aucune confusion entre les variables libres et les variables quantifi es ainsi chaque substitution devra tre adapt e la formule laquelle elle est appliqu e D finition 2 1 6 Pour toute substitution o et pour toute formule F on dit que o est adapt e F quand l ensemble VI o N Va F est vide D finition 2 1 7 Pour toute formule F et pour toute substitution o adapt e F l application de o F not e o F est d finie par r currence sur F comme suit F T oF T Pogas ala sia Dom a a sinon F A gt B 0 F 0 A o B F Ya A oF Vaw A Pour viter toute confusion nous crivons u o F les applications de substitutions de la forme w o F Pour all ger la manipulation des applications de substitutions nous introduisons une fonction de composition des substitutions Lemme 2 1 1 Soient F une formule o une substitution adapt e F et u une substitution adapt e o F Notons u la substitution pW o H
219. x l est motivable dans F CP donc T est motivable d apr s gt i par hypoth se de r currence T A B est d rivable par hypoth se de r currence T A et 7 Vi deux cas se pr sentent Ve par hypoth se de r currence le jugement T Va A a par hypoth se de r currence I A est d rivable 29 CHAPITRE 2 Calculs propositionnels p dagogiques du second ordre d apr s le lemme 2 2 9 nous avons A By et ainsi nous d rivons T By par la r gle a La proposition 2 2 11 traite des jugements cependant on peut le restreindre en un r sultat sur les th or mes Proposition 2 2 12 Le jugement F est d rivable si et seulement si le jugement H Yy F est d rivable D monstration Nous traitons s par ment les deux sens de l quivalence cas imm diat par le lemme 2 2 11 lt supposons que le jugement V7 F soit d rivable nous d rivons y L F par la r gle Ve et comme y L F F nous avons une d rivation de HER Comme la formule peut toujours tre remplac e par une variable fraiche elle perd compl tement ce qui la distingue d une constante ind finie on ne peut plus prouver dans F CP que L implique toutes les formules En particulier Va L a n est pas un th or me de F CP Proposition 2 2 13 Le jugement Va l a n est pas d rivable D monstration Su
220. ypoth se le jugement T ae t F est d rivable et le type U est motivable d apr s le lemme 5 3 5 le jugement a U T 4 a U t a U F est d rivable nous avons a VI T donc nous avons une d rivation du jugement D S la U t a U F On d duit des lemmes 5 3 2 et 5 3 5 la stabilit de P AC par 3 r duction Proposition 5 3 6 Pour tout jugement d rivable T Le t F et pour tout A terme u tel que t g u le jugement T roe u F est d rivable D monstration Par r currence sur la d rivation de t gt u nous ne traitons que les cas des r gles 63 B red et Bired les autres cas tant imm diats ou analogues au cas 6 u g u ATAU g As a Tz A on u B est d rivable par hypoth se de r currence le jugement F x A u B est d rivable ainsi le jugement T x A oe Azu B est d rivable l aide de la r gle Ba posons F A B par hypoth se le jugement Oe ie Sars Brea imm diat d apr s le lemme 5 3 2 imm diat d apres le lemme 5 3 5 Aa u A g a A u BArea 5 4 Utilit L isomorphisme de Curry Howard permet de transporter des propri t s des syst mes formels dans les syst mes fonctionnels En particulier le fait que dans le calcul P CP toutes les formules apparaissant dans les d rivations soient motivables a comme contrepartie dans P AC une propri t des termes typables que nous appelons l utilit Int

Th`ese

Contents

Download Pdf Manuals

Related Search

Related Contents