The Logic of Provability

《The Logic of Provability》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、CHAPTERVIITheLogicofProvabilityGiorgiJaparidzeDepartmentofComputerandInformationScience,UniversityofPennsylvaniaPhiladelphia,Pennsylvania19104-6389,USADickdeJonghInstituteforLogic,LanguageandComputation,UniversityofAmsterdamNL-1018TVAmsterdam,TheNetherlandsThischapterisdedic

2、atedtothememoryofGeorgeBoolos.Fromthestartofthesubjectuntilhisdeathon27May1996hewastheprimeinspireroftheworkinthelogicofprovability.Contents1.Introduction,Solovay'stheorems..........................3602.Modallogicpreliminaries..............................3613.ProofofSolovay

3、'stheorems.............................3654.Fixedpointtheorems................................3675.PropositionaltheoriesandMagari-algebras.....................3686.TheextentofSolovay'stheorems..........................3697.Classicationofprovabilitylogics....................

4、......3718.Bimodalandpolymodalprovabilitylogics.....................3749.Rosserorderings...................................37810.Logicofproofs....................................38011.Notionsofinterpretability..............................38312.Interpretabilityandpartialcons

5、ervativity......................38613.Axiomatization,semantics,modalcompletenessofILM..............39714.ArithmeticcompletenessofILM..........................40315.Tolerancelogicandotherinterpretabilitylogics..................41016.Predicateprovabilitylogics.................

6、............41317.Acknowledgements..................................422References........................................422HANDBOOKOFPROOFTHEORYEditedbyS.R.Bussc1995.ElsevierScienceB.V.Allrightsreserved.PreliminaryDraft-April17,1997360GiorgiJaparidzeandDickdeJongh1.Introduc

7、tion,Solovay'stheoremsGodel'sincompletenesstheoremsandChurch'sundecidabilitytheoremforarith-meticshowedthatreasonablystrongformalsystemscannotbecompleteanddecidable,andcannotprovetheirownconsistency.Evenatthetimethoughthesenegativetheoremswereaccompaniedbypositiveresults.Fir

8、stly,formalsystemsfarebetterinreasoninginrestrictedareas,andthisreasoningca