The logic of proofs, semantically

TheLogicofProofs,SemanticallyMelvinFittingDept.MathematicsandComputerScienceLehmanCollege(CUNY),250BedfordParkBoulevardWestBronx,NY10468-1589e-mail:fi[e-mail]:comet.lehman.cuny.edu/fittingMarch31,2004AbstractAnewsemanticsispresentedforthelogicofproofs(LP),[1,2],basedontheintuitionthatitisalogicofexplicitknowledge.ThissemanticsisusedtogivenewproofsofseveralbasicresultsconcerningLP.Inparticular,therealizationofS4intoLPisestablishedinawaythatcarefullyexaminesandexplicatestheroleofthe+operator.Finallyconnectionsaremadewiththeconventionalapproach,viasoundnessandcompletenessresults.1IntroductionTheLogicofProofs(LP)bearsthesamerelationshiptoexplicitproofsinformalarithmeticthatG¨odel-L¨oblogic(GL)bearstoarithmeticprovability.Insteadofthesinglemodaloperator,,ofGL,intendedtorepresentarithmeticprovability,LPhasmanymodal-likeoperators,withformulasoftheformt:Xinformallyread“tisaproofofX.”Theoperators,liket,arecalledproofpolynomials,andbasicmachineryisprovidedforconstructingmorecomplexproofpolynomialsfromsimplerones.AllthiswasintroducedbyArtemov,[1,2],whoalsoestablishedthechieffactsaboutLP.Amonghisresultsare:LPinternalizesitsownnotionofprovability;S4embedsinLPinanaturalway;andthereisanarithmeticcompletenesstheoremforLPanalogoustothatofSolovayforGL.Mostfundamentally,LPanswersalongstandingquestionabouttheintendedprovabilitysemanticsforthemodallogicS4andhenceforintuitionisticpropositionallogic.Givenitsintendedsubjectmatter,itisnotsurprisingthatmostoftheresultsconcerningLPhavebeenestablishedprooftheoretically.AsemanticsforLPwasintroducedin[9].Amongotherthings,ithasbeenusedtoprovidedecidabilityresults,andin[10]toestablishcutelimination.InthispaperIpresentadifferent,butrelated,semanticsforLPthat,Ihope,willhaveaparticularintuitiveappeal,andbesufficientlyflexibletomakeitapplicabletootherLP-likelogics.Onecanthinkofitasappropriateforlogicsofexplicitknowledge,withaproofbeingonekindofexplicitknowledge.IwillgivetwodifferentversionsofasemanticsforLP.Theexactrelationshipbetweenthemisunexpectedlycomplicated,andthiswillbediscussed.Then,usingthissemanticmachinery,Iwillre-establishmostofthebasicresultsconcerningLP.AstotheembeddingofS4intoLP,Iwillexaminethisinconsiderabledetailandwillprovesomenewresultsabouttheroleofthe+operationofLP.Finally,IwillshowtheequivalenceofthesemanticalcharacterizationwiththeusualaxiomaticandGentzencalculusformulations.Theworkpresentedherehaditsoriginsin[5,6].12MelvinFitting2SyntaxFollowing[2],thelanguageofLPisbuiltfromthefollowingbasicmachinery.(Items1,4,and5mayappearwithsubscripts.)1.propositionalvariables,P,Q,...2.propositionalconstant,⊥3.logicalconnective,⊃4.proofvariables,x,y,...5.proofconstants,c,d,...6.functionsymbols!(monadic),·,+(binary)7.operatorsymbolofthetypehtermi:hformulaiProofpolynomials,alsocalledterms,arebuiltupfromproofvariablesandproofconstants,usingthefunctionsymbols.Groundproofpolynomialsarethosewithoutvariables.Formulasarebuiltupfrompropositionalvariablesandpropositionalconstantsusing⊃(withotherconnectivesdefinedintheusualway),andtheadditionalruleofformation:iftisaproofpolynomialandXisaformulathent:Xisaformula.Itisappropriatetoconsidersublanguageswith+or!omitted,though·shouldalwaysbepresent.Theformulat:Xshouldberead:“tisaproofofX.”Proofconstantsintuitivelyrepresentproofsoflogicaltruths—the‘givens.’Proofvariablesinaformulacanbethoughtofasimplicitlyuniversallyquantifiedoverproofs.Theoperation·ismostfundamental.IftisaproofofX⊃YanduisaproofofX,weshouldthinkoft·uasaproofofY.Theoperation!isaproof-checker:iftisaproofofX,weshouldthinkof!tasaverificationthattissuchaproof.Finally,theoperation+combinesproofsinthesensethatt+uprovesallthethingsthattprovesplusallthethingsthatuproves.Ofcourse,thisisallquiteinformalsofar.3SemanticsInthissectionIwillpresenttwodifferentversionsofmodelsforLP.Soundnessandcompletenesswillbeestablishedforboth,buttheexactrelationshipbetweenthemiscomplex,andwillbeinvestigatedstartinginthenextsection.Interestinglyenough,muchdependsontheroleoftheproofconstants.WhileLPwasmotivatedbythestructureofproofsinarithmetic,itcanbeplacedinamoregeneralcontext—itisalogicofexplicitknowledge.Wemightreadt:Xas“IknowXforreasont.”Ifwetakethispointofview,therearetwowayst:Xmightbefalse:first,XissomethingIdon’tknow;second,whileIknowX,thereasonisnott.Thelogicofknowingornotknowingissomethingthathasbeenextensivelyinvestigated,start-ingwith[7].Inthenow-standardapproach,itisnotactualknowledgethatismodeled,butpotentialknowledge.Forinstance,ifIknowXandIknowX⊃Y,ImaynotknowYbecauseIhavenotthoughtaboutit,butIpotentiallyknowY—itissomethingIamentitledtoknow.Thisuseofpotentialknowledgesimplifiesthingsconsiderably.OnecanworkwithaKripkestructure,thinkingofpossibleworldsasstatesofknowledge,andtheaccessibilityrelationasakindofindistinguisha-bilitynotion.IfΓisthewaythingsare,andΔisaccessiblefromΓ,myknowledgeisnotsufficientformetorecognizethattheworldisΓandnotΔ.Then,I(potentially)knowXatΓprovidedXTheLogicofProofs,Semantically3isthecaseatallworldsIcan’tdistinguishfromΓ.Thismakespotentialknowledgeintoamodaloperator,usual