Referential logic of proofs

ReferentialLogicofProofsVladimirN.KrupskiDepartmentofMathematicalLogicandtheTheoryofAlgorithms,FacultyofMechanicsandMathematics,MoscowStateUniversity,Moscow119992,RussiaAbstractWeintroduceanextensionofthepropositionallogicofsingle-conclusionproofsbythesecondordervariablesdenotingthereferenceconstructorsofthetype“theformulawhichisprovedbyx.”TheresultingLogicofProofswithReferences,FLPref,isshowntobedecidable,andtoenjoysoundnessandcompletenesswithrespecttotheintendedprovabilitysemantics.WeshowthatFLPrefprovidesacompletetestofadmissibilityofinferencerulesinasoundextensionofarithmetic.Keywords:prooftheory,explicitmodallogic,singleconclusionlogicofproofs,proofterm,reference,unification,admissibleinferencerule.1IntroductionSinceG¨odel’sincompletenessproof,theformalarithmetic(arecursivelyenu-merableextensionofthefirst-orderPeano’sArithmeticPA)iswidelyusedasaformalprooftheory,i.e.asystemwheretheargumentsaboutformalproofsandprovabilitycouldbeformalized.Howeverforsomeapplicationsoffor-malprooftheoryoutsidetraditionalfoundationsofmathematicstheformalarithmeticisnotefficient.Considerthefollowingexampleconcerningreliabilityoftheautomatedrea-soningsystems.Asoftwareofthiskind(see[21])isaverificationtoolwhichverifiesapropositionϕbyconstructingitsformalproofinaformaltheoryT(thegroundtheorysupportedbythesystem).Aproofdevelopmentprocessusuallyrequiresacorrectnesscheckingandforthispurposesthesystemissuppliedwithaproofcheckingprogram.Reliabilityofthesystemisbased,inEmailaddress:[e-mail](VladimirN.Krupski).PreprintsubmittedtoElsevierScience30June2006part,onthemetaassumptionthatifaproofcheckersucceedsongivencodesofpandϕ,thenpisindeedaproofofϕ:ProofCheck(code(p),code(ϕ))=trueimpliesthatpisaproofofϕ.(1)Theoretically,thisassumptioncanbeformalizedandverifiedinarithmetic.Howeverthestraightforwardformalization,G¨odel’sstyle,isnotfeasible,andwehavetoenhancetheexpressivepowerofthegroundsystem(i.e.,arithmetic)byspecialtoolstomakethiskindofreasoningpractical.AnexampleofsuchatoolinactionisthefollowingderivationoftheSecondG¨odelIncompletenessTheoremfromthearithmeticalsoundnesstheoremforthemodalProvabilityLogicGL[23].GLisknowntobesoundundereveryarithmeticalinterpretationwhere2correspondstotheformalprovabilitypredicateProvable(·)inarithmetic,so¬2⊥istranslatedasthearithmeti-calconsistencystatementConsis=¬Provable(p⊥q)).InthiscasethekeylemmaPA`Provable(pConsisq)→¬Consis(2)canbeobtainedbyproofconversionfromitsmodalprototypeGL`2¬2⊥→¬¬2⊥.ThelattercanbeestablishedbyastraightforwardderivationinGL.Notethatadirectformalizationof(2)inPAisproblematic.HerethemodallogicGLplaysaroleofa“prooftheoreticalinterface”fortheformalarithmetic.InordertoconstructaPA-derivationofsomesentencewhichinvolvesProvable(·)onecantryrestoringitsmodalschemeandthenconstructingaGL-derivationofthescheme.ThecorrespondingPA-derivationcanbeobtainedfromtheGL-derivationoftheschemebytheproofconversionalgorithmfromthesoundnesstheorem.AnothersuchinterfaceisgivenbythemodallogicS4.G¨odel[13]introducedthemodallogicS4asthelogicofprovability.Theintendedinformalmeaningoftheformula2Fwas“Fhasaproof.”HoweveraformalprovabilitysemanticsforS4wasnotproposed.TheprincipaldifficultywascausedbytheverificationpropertyofproofswhichwasincorporatedinS4viathereflexivityaxiom2F→F.Thisaxiomisincorrectwithrespecttothestraightforwardarithmeticalin-terpretationof2Fas“FisprovableinaformaltheoryT”whereTisanytheoryforwhichtheSecondG¨odelIncompletenessTheoremholds,andsoS4isincompatiblewithGL.AnapproachtothisproblemwassketchedbyG¨odelinhisLectureatZilsel’sin1938(whichremainedunpublishedtill1995[14]):toreformulateS4inthelanguagewithatomicpropositions“tisaproofofF”2foracorrespondingsetofproofexpressionsrepresentingthestructureoftheproofs.ThisapproachwasindependentlydevelopedbyS.Artemov.ItresultedinaunifiedarithmeticalprovabilitysemanticsformodallogicS4,intuitionisticlogicandlambda-terms[4,6,7].Artemov’sLogicofProofsLPdescribesthemulti-valuedversionoftheproofpredicate“xisaproofofF”togetherwithoperationsonproofsinducedbypropositionalPA-soundinferencerules.InthelanguageofLPtheS4-modality2(·)issplitintoaninfinitesetofterm-labelledoperators[t](·)wheretisatermcombinedfromproofvariablesandaxiomconstants(i.e.thenotationsfortheproofsofaxioms)usingafinitesetoffunctionsymbolswhichdenotesomeparticularcomputableoperationsonproofs.Thusatermtissomekindofaprogramwhichcomputesaproofgiventheproofsdenotedbyitsatomiccomponents.Theconstructor[·](·)inLP-languagecorrespondstothearithmeticalproofpredicatePrf(·,·).TheverificationpropertyofproofsisexpressedbyLP-axiomsoftheform[t]F→F.(3)LPissoundandcompletewithrespecttoarithmeticalmulti-conclusionproofinterpretationsandprovidesanexactrealizationofS4(i.e.S4`Fiffthereisaway(·)rtolabelallboxesinFbytermsforwhichLP`Fr).So,anS4-proofofaschemecanbeconvertedintoaPA-proofofitsarithmeticalinstantbythecomposedtranslationS4,→LP,→PA.Aswasestablishedin[18],theproofsearchforLPiseveneasierthanoneforS4(LP∈Πp2,whereasS4isPSPACE-complete).AllthisshowsthattheprooflogiclanguageandLPitselfmaybeconsideredasthetop-levelproof