propositional logic and

2024-06-20 来源：爱问旅游网

SubstitutionsofΣ01-Sentences

explorationsbetweenintuitionisticpropositionallogicandintuitionisticarithmetic

AlbertVisser

DepartmentofPhilosophy,UtrechtUniversityHeidelberglaan8,3584CSUtrecht,TheNetherlands

email:Albert.Visser@phil.uu.nl

December14,2002

DedicatedtoAnneTroelstraontheoccasionofhis60thbirthday.

Abstract

Thispaperisconcernedwithnotionsofconsequence.Ontheonehand

westudyadmissibleconsequence,speciﬁcallyforsubstitutionsofΣ01-sentencesoverHeytingArithmetic(HA).Ontheotherhandwestudypreservativityrelations.Thenotionofpreservativityofsentencesoveragiventheoryisadualofthenotionofconservativityofformulasoveragiventheory.

WeshowthatadmissibleconsequenceforΣ01-substitutionsoverHAcoincideswithNNIL-preservativityoverintuitionisticpropositionallogic(IPC).HereNNIListheclassofpropositionalformulaswithnonestingsofimplicationstotheleft.

TheidenticalembeddingofIPC-derivability(consideredasapreorderand,thus,asacategory)intoaconsequencerelation(consideredasapreorder)hasinmanycasesaleftadjoint.ThemaintoolofthepresentpaperwillbeanalgorithmtocomputethisleftadjointinthecaseofNNIL-preservativity.

InthelastsectionweemploythemethodsdevelopedinthepapertogiveacharacterizationtheclosedfragmentoftheprovabilitylogicofHA.

Keywords:ConstructiveLogic,PropositionalLogic,Heyting’sArithmetic,Schema,Admis-sibleRule,ConsequenceRelation,ProvabilityLogicMSC2000codes:03B20,03F40,03F45,03F55

Contents

1Introduction

1.1PropositionalLogic.1.2Arithmetic......1.3Provabilitylogic..1.4HistoryandContext1.5Acknowledgements..............................................................................................................................3345671.6Prerequisites....

.........................

2FormulasofPropositionalLogic

3Semi-consequence

3.1BasicDeﬁnitons...........................3.2PrinciplesInvolvingImplication...................4Preservativity

4.1BasicDeﬁnitions...........................4.2ExamplesofPreservativityRelations....

............4.2.1TheLogicofaTheory....................4.2.2AdmissibleConsequence...................4.2.3AResultofPitts.......................4.3BasicFacts..............................4.4ASurveyofResultsonPreservativity...

............4.4.1DerivabilityforIPC......................4.4.2AdmissibleConsequenceforIPC..............4.4.3AdmissibleRulesforΣ-SubstitutionsoverHA.......5ApplicationsofKripkeSemantics5.1SomeBasicDeﬁnitions........................5.2TheHenkinConstruction......................5.3MoreDeﬁnitions...........................5.4ThePushDownLemma.......................

6RobustFormulas7TheNNIL-Algorithm

8BasicFactsandNotationsinArithmetic8.1ArithmeticalTheories........................8.2ABriefIntroductiontoHA∗.....................9ClosurePropertiesofΣ-Preservativity9.1ClosureunderB1...........................9.2AClosureRuleforImplication...................10OnΣ-Substitutions

77889101011121212131515151616161717171921

27272830303235

11TheAdmissibleRulesofHA12ClosedFragments

12.1Preliminaries.........12.2TheClosedFragmentforHA∗12.3TheClosedFragmentofPA.12.4TheClosedFragmentofHA.12.5ComparingThreeFunctors.12.6Questions...........AAdjointsinPreorders

BCharacterizationsandDependenciesCModalLogicforΣ-Preservativity

........................................................................................................................

3637374242444545495052

1Introduction

Thispaperisastudybothofconstructivepropositionallogicandofconstruc-tivearithmetic.Inthecaseofarithmeticthefocusisnotonprooftheoreticalstrengthbutonthe‘logical’propertiesofarithmeticaltheories.

Iwillﬁrstexplainthecontentsofthepartofthepaperthatisconcernedpurelywithpropositionallogic.Thispartisindependentofthearithmeticalpartandcouldbestudiedonitsown.Afterthat,Iwillexplainthearithmeticalpart.

1.1PropositionalLogic

Intuitionisticpropositionallogic,IPC,diﬀersfromclassicalpropositionallogicinthatitadmitsnaturalhierarchiesofformulas.TheﬁrstlevelofoneofthesehierarchiesisformedbytheNNIL-formulas.‘NNIL’standsfornonestingsofimplicationstotheleft.Thus(p→(q→(r∨(s→t))))isaNNIL-formulaand((p→q)→r)isn’t.NNILformulasaretheanaloguesofpurelyuniversalsentencesintheprenexnormalformhierarchyforclassicalpredicatelogic,inviewofthefolowingcharacterization:moduloIPC-provableequivalencethisclasscoincideswithROBtheclassofformulasthatarepreservedundertakingsub-Kripke-models.1

fact,thereisawayofstrengtheningthecharacterization,thatmakesNNILanatural

subclassofthepurelyuniversalformulasofaspeciﬁctheoryinpredicatelogic.WecanreformulateKripkesemanticsinafamiliarwayasatranslationofIPCintoasuitabletheoryinpredicatelogic,sayT,ofKripkestructures.OnecancharacterizetheformulasofIPC,moduloT-provableequivalence,aspreciselythepredicatelogicalformulasinonefreevariablethatareupwardspersistentandpreservedunderbisimulation.TheNNIL-formulasare,moduloprovableequivalence,preciselythepredicatelogicalformulasinonefreevariablethatareupwardspersistent,preservedunderbisiuationandpreservedundertakingsubmodels.Thus,theNNIL-formulasare,moduloprovableequivalence,preciselythepurelyuniversalformulasofTthatcorrespondviathetranslationtoIPC-formulas.See[VvBdJdL95].

1In

HereROBstandsforrobust.Thecharacterizationcanbeprovedinatleasttwoways.Oneproofispresentedin[VvBdJdL95].TheideaofthisproofisduetoJohanvanBenthem.VanBenthem’sproofisanalogoustotheclassicalproofofL󰀎o´s-Tarskitheorem.Seealso[vB95].Anotherproofiscontainedinthepreprints[Vis85]and[Vis94].Thissecondproofistheonepresentedinthispaper(seesection7).Thebasicideaoftheproofisthat,givenanar-bitrarypropositionalformulaA,onecomputesitsbestrobustapproximationfrombelow,sayA∗.ThecomputationwillterminateinaNNIL-formula.SinceNNIL-formulasaretriviallyrobust,itfollowsthatrobustformulascanalwaysberewrittentoIPC-equivalentNNIL-formulas.

Reﬂectingontheproof,oneseesthatitisbestunderstoodintermsofthefollowingnotions.WedeﬁneIPC,ROB-preservativityasfollows:•A£IPC,ROBB:⇔∀C∈ROB(C󰀬IPCA⇒C󰀬IPCB).

TheclaimthatA∗isthebestrobustapproximationofA,canbeanalysedtomeanthefollowing:A£IPC,ROBB⇔A∗󰀬IPCB.Thus(·)∗istheleftadjointoftheidenticalembeddingof󰀬IPCconsideredasapreorder(andthusasacategory)into£IPC,ROBconsideredasapreorder.Asaspin-oﬀofourproofweobtainan‘axiomatization’of£IPC,ROB.

Preservativitycanbeviewedasdualtoconservativityofsentencesoveragiventheory.Notethatintheconstructivecontextpreservativityandconser-vativitycannotbetransformedintoeachother(moduloprovableequivalence).Anotherimportantnotionofconsequenceisadmissibleconsequence,dis-cussedinthenextsection.Inthepresentpaperwewillstudythetwoconse-quencenotions,preservativity&admissibility,intandem.

1.2Arithmetic

AΣ01-formulaisaformulainthelanguageofarithmeticconsistingofablockofexistentialquantiﬁersfollowedbyaformulacontainingonlyboundedquan-tiﬁers.AΠ01-formulaisaformulainthelanguageofarithmeticconsistingofablockofuniversalquantiﬁersfollowedbyaformulacontainingonlyboundedquantiﬁers.Wewilloftenwrite‘Σ-formula’and‘Π-formula’forΣ01-formula,re-spectivelyΠ01-formula.Intheclassicalcontext,Σ-formulasandΠ-formulasareinterdeﬁnableusingonlyBooleanconectives:aΠ-formulaisthenegationofΣ-formulaandaΣ-formulaisthenegationofaΠ-formula.Constructively,underminimalarithmeticalassumptions,aΠ-formulaisstillprovablyequivalenttothenegationofaΣ-formula,bute.g.overHeyting’sArithmetic,wehavethatifaΣ-sentenceisprovablyequivalenttoanyBooleancombinationofΠ-sentences,thenitiseitherprovableorrefutable.2

Itisacommonobservation,thatifwehaveprovedsomeBoolean(or,per-haps,‘Brouwerian’)combinationofΣ-sentencesinHeytingArithmetic,(HA),thenweoftenknowthatabetterBooleancombinationofthesameΣ-sentences

waytoprovethisisbyusingcorollary9.2incombinationwiththedisjunctionprop-ertyofHeyting’sArithmetic.

2One

isalsoprovable.MoreoverthisbetterBooleancombinationcanbefoundinde-pendentlyofthespeciﬁcΣ-sentencesunderconsideration.

Suppose,forexample,thatwehavefoundthatHA󰀬¬¬S→S.Then,usingtheFriedmantranslation,wemayshowthatonealsohas:HA󰀬S∨¬S.Inwhichsenseis(S∨¬S)betterthan(¬¬S→S)?Well,wehave

p∨¬p󰀬IPC¬¬p→pbutnot¬¬p→p󰀬IPCp∨¬p.

Sotheformof(S∨¬S)ismoreinformativethantheformof(¬¬S→S).Canwedostillbetterthan(S∨¬S)?Yesandno.Yes,sinceHAhasthedisjunctionpropertywedohaveeitherHA󰀬SorHA󰀬¬S.Thus,foraspeciﬁcS,wecanﬁndafurtherimprovement.No,ifwedemandthattheimprovementdependonlyontheformoftheBooleancombinationofΣ-sentences,inotherwords,ifwewanttheimprovementtobeuniformforarbitrarysubstitutionsofΣ-sentences.

Analyzingtheseideas,onearrivesatthefollowingexplicationofwhatoneislookingfor.LetPbeasetofpropositionalvariables.ΣPisthesetofassignmentsofΣ-sentencestothepropositionalvariables.LetfbesuchanassignmentofΣ-sentences.WewritefAfortheresultofsubstitutingthefp’sforpinA.IfwewanttostressthefactthatweliftedfonPtoafunctiononthefulllanguageofpropositionallogicoverP,wewrite[f]fortheresultofthelifting.Thus[f]isasubstitutionofΣ-sentences.WedeﬁnetherelationofHA,Σ-admissibleconsequenceasfollows.LetA,BbeIPC-formulas.•A∼HA,ΣB⇔∀f∈ΣP(HA󰀬fA⇒HA󰀬fB).

ConsiderapropositionalformulaA.Let’scallA’sdesiredbestimprovementA∗.WewillshowthatA∗alwaysexistsandsatisﬁesthefollowingclaim:

A∼HA,ΣB⇔A∗󰀬IPCB.

Astheattentivereaderwillhaveguessed,(·)∗ofsubsection1.1isidenticalto(·)∗ofsubsection1.2.Thus,wealsohave:∼HA,Σ=£IPC,ROB.

1.3Provabilitylogic

Pureprovabilitylogichas,inmyopinion,twogreatopenproblems.TheﬁrstoneistocharacterizetheprovabilitylogicsofWilkieandParis’theoryI∆0+Ω1andofBuss’theoryS12.Thisproblemhasbeenextensivelystudiedin[Ver93]and[BV93].ThesecondproblemistocharacterizetheprovabilitylogicofHA.Thisproblemisstudiedin[Vis81],[Vis82],[Vis85]and[IemXX].

InthepresentpaperwewillpresentfullcharacterizationsfortwofragmentsoftheprovabilititylogicofHA.TheﬁrstisthecharacterizationofallformulasoftheformPA→PB,validintheprovabilitylogicofHA,whereAandBarepurelypropositional.ThischaracterizationisduetoRosalieIemhoﬀ.Seeher

paper[Iem99].ThesecondoneisthecharacterizationoftheclosedfragmentoftheprovabilitylogicofHA.Thisismyoldresult,reportedﬁrstin[Vis85].3

Intheappendixofthepresentpaper,IformulateaconjectureabouttheprovabilitylogicofHA.PartofthisconjectureisthatthislogicisbestformulatedinthericherlanguagecontainingabinaryconnectiveforΣ-preservativity.

1.4HistoryandContext

Theresultsreportedinthispapertookalongtimefromconceptiontopublica-tion.Themainpartofthisresearchherewasdonebetween1981and1984.Theprimaryobjectsofthisresearchwere(i)thecharacterizationoftheclosedfrag-mentofHAand(ii)generalizingtheresultsofDickdeJonghonpropositionalformulasofonevariable(see[dJ82]).4Theresultsofthisresearchwerereportedinthepreprint[Vis85].Forvariousreasons,however,thepreprintwasneverpublished.In1994Icompletelyrewrotethepaper,resultinginthepreprint[Vis94].However,again,thepaperwasnotpublished.Thepresentversion,writtenin2000,isanextensiveupdateofthe1994preprint.

Toputthepresentpaperinabroadercontextofresearch,letmebrieﬂysumupsomerelatedwork.

Firsttherearemanyresultsonlogicsoftheories(seesubsubsection4.2.1).ForsimplepropositionallogicthereisDeJongh’stheoremsayingthatthepropositonallogicofHAandrelatedtheoriesispreciselyIPC.Seee.g.[Smo73],[Vis85],[dJV96]forsomeproofs.Inthecaseofe.g.HA+MP+ECT0,wegetastrongerlogic.Seee.g.[Gav81].Aprecisecharacterizationofthislogicisstilllacking.FordeJongh’stheoremforPredicateLogic,see[dJ70],[Lei75],[vO91].Negativeresultsforthecaseofintuitionisticpredicatelogicarecontainedin[Pli77],[Pli78]and[Pli83].Forthestudyofschemesintheclassicalpredicatecalculus,thereaderisreferredto[Yav97].

Secondly,wehaveprovabilitylogic.Heretheschematiclanguagesarelan-guagesofmodallogic.Thereaderisreferredtotheexcellenttextbooks[Smo85]and[Boo93].Fortheworkinthispaper,thedevelopmentofinterpretabilitylogicisofparticularinterest.Seethesurveypapers[JdJ98]and[Vis98a].Ourcen-tralnotionΣ-preservativityiscloselyrelatedtothenotionofΠ01-conservativity,studiedininterpretabilitylogic.Thisconnectionturnsouttobereallyuseful:theexpertisegeneratedbyresearchintoKripkemodelsforinterpretabilitylogic,isnowusedbyRosalieIemhoﬀinthestudyoftheprovabilitylogicofHAandofadmissiblerules.See[IemXX]and[Iem99].

problemtocharacterizetheclosedfragmentoftheprovabilitylogicofPAwasFried-man’s35thproblem.See[Fri75].ItwassolvedindepentlybyvanBenthem,MagariandBoolos.

4ThefullgeneralizationofdeJongh’sresultshadtowaittill1998(see[Vis99]).Thecruciallemma,wasprovedbySilvioGhilardi,followingaratherdiﬀerentlineofenquiry.See[Ghi99].Ghilardi’slemmacharacterizestwoclassesofpropositionalformulas,theprojectiveformulasandtheexactformulasaspreciselythosewiththeextensionproperty—apropertyformulatedintermsofKripkemodels.GuramBezhanishvilishowedmethatGhilardi’slemmacanalsobeobtainedbyapplyingtheworkofR.Grigolia.See[Gri87].

3The

Thirdly,theworkonaxiomschemescanbegeneralizedtothestudyofadmissiblerules,exactformulas,uniﬁcationandthelike.Wereferthereaderto[Lei80],[dJ82],[Ryb92],[dJC95],[dJV96],[Ryb97],[Ghi99],[Iem99].Acloselyrelatedsubjectisuniforminterpolation.See[Pit92],[GZ95a],[GZ95b]and[Vis96].

Fourthlyandﬁnally,thereistheissueofformulaclasses,likeNNIL,andtheircharacterization.Thesemattersaretakenupine.g.[Lei81],[vB95],[VvBdJdL95]5,[Bur98]and[Vis98b].

1.5Acknowledgements

InvariousstagesofresearchIbeneﬁtedfromthework,thewisdomand/ortheadviceof:JohanvanBenthem,GuramBezhanishvili,DirkvanDalen,RosalieIemhoﬀ,DickdeJongh,KarstKoymans,JaapvanOosten,PietRodenburg,VolodyaShavrukov,RickStatman,AnneTroelstraandDomenicoZambella.LevBeklemishevspottedasillymistakeinthepenultimateversionofthepaper.Iamgratefultotheanonymousrefereeforhis/herhelpfulcomments.IthankSanderHermsenformakingthepicturesforthispaper.

1.6Prerequisites

Someknowledgeof[TvD88a],[TvD88b]iscertainlybeneﬁcial.AtsomeplacesIwillmakeuseofresultsfrom[Vis82]and[dJV96].

2FormulasofPropositionalLogic

Inthissectionweﬁxsomenotations.WealsointroducethecentralformulaclassNNIL.

P,Q,...willbesetsofpropositionalvariables.p󰁃,󰁃q,󰁃r,...willbeﬁnitesetsofpropositionalvariables.WedeﬁneL(P)asthesmallestsetSsuchthat:•P⊆S,󰀝,⊥∈S,

•IfA,B∈S,then(A∧B),(A∨B),(A→B)∈S.

sub(A)isthesetofsubformulasofA.Byconventionwewillcount⊥asasubformulaofanyA.pv(A)isthesetofpropositionalvariablesoccurringinA.Wedeﬁneameasureofcomplexityρ,whichcountstheleft-nestingof→,asfollows:

•ρp:=ρ⊥:=ρ󰀝:=0

•ρ(A∧B):=ρ(A∨B):=max(ρA,ρB)•ρ(A→B):=max(ρA+1,ρB)

5This

papermaybeconsideredasacompanionpaperofthepresentpaper.

NNIL(P):={A∈L(P)|ρA≤1}.InotherwordsNNIListheclassofformulaswithoutnestingsofimplicationstotheleft.AnexampleofaNNIL-formulais:(p→(q∨(s→t)))∧((q∨r)→s)).ItiseasytoseethatmoduloIPC-provableequivalenceeachNNIL-formulacanberewrittentoaNNIL0-formula,i.e.afor-mulainwhichasantecedentsofimplicationsonlysingleatomsoccur.FormoreinformationaboutNNIL,see[dJV96]and[VvBdJdL95].Forageneralizationoftheresultof[VvBdJdL95]tothecaseofpredicatelogic,see[Vis98b].

3Semi-consequence

Inthissectionweintroducethebasicnotionofsemi-consequencerelation.‘£’willrangeoversemi-consequencerelations.Let󰀬standforderivabilityinIPC.

3.1BasicDeﬁnitons

LetBbealanguage(forpropositionalorpredicatelogic)andletTbeatheoryinB.Asemi-consequencerelationonBoverTisabinaryrelationonthesetofB-formulassatisfying:A1A2A3

A󰀬TB⇒A£B

A£BandB£C⇒A£CC£AandC£B⇒C£(A∧B)

Thename‘semi-consequencerelation’isadhocinthispaper.Wetake:•A≡B:⇔A£BandB£A.

Ifwedon’tspecifythetheorycorrespondingtothesemi-consequencerelation,itisalwayssupposedtobeoverIPC.Afurthersalientprincipleis:•B1A£CandB£C⇒(A∨B)£C.

ArelationsatisfyingA1-A3andB1iscalledanearly-consequencerelation.Notethat󰀬Tisanearly-consequencerelationoverT.󰀁󰀂󰀁󰀂WewilluseX󰀬Y,X£Yforrespectively󰀁X󰀬YandX£Y,󰀂whereXandYareﬁnitesetsofformulas.Here󰀁∅:=󰀝󰀂and∅:=⊥.Wetreatimplicationssimilarly,writing(X→Y)for(X→Y).WewriteX,YforX∪Y;X,AforX∪{A},etcetera.

Nearly-consequencerelationsoverTcanbealternativelydescribedinGenzenstyleasfollows.Nearly-consequencerelationsarerelationsbetween(ﬁnietesetsof)formulassatifyingthefollowingconditions.A1󰀂ThinCut

X󰀬TY⇒X£YX£Y⇒X,Z£Y,U

X£Y,AandZ,A£U⇒X,Z£Y,U

Wetakethepermutationrulestobeimplicitinthesetnotation.WeleaveittothereadertochecktheequivalenceoftheGenzenstyleprincipleswithA1-A3plusB1.

Wewillbeinterestedinadjointsinvolvingsemi-consequencerelations.SomebasicfactsconcerningadjointsandpreordersaregiveninappendixA

3.2PrinciplesInvolvingImplication

Principlesinvolvingimplicationplayanimportantroleinthepaper.Infact,themainreasonforthecomplexityofe.g.theadmissiblerulesofIPC,theadmissiblerulesofHAandtheadmissiblerulesofHAforΣ-substitutionsisthepresenceofnestedimplicationsandtheinterplayofimplicationsanddisjunctions(intheantecedent).

Regrettably,theprinciplesinvolvingimplicationneededtocharacterizead-missibleconsequenceandΣ-preservativityarenevergoingtowinabeautycon-test.

Theprincipesintroducedbelow,allowustoreducethecomplexityofformu-las.E.g.ifaformulaoftheform(C→D)→(E∨F)isprovableinIPC(HA),thenalso((C→D)→C)∨((C→D)→E)∨((C→D)→F)isprovableinIPC(HA).Theremovalofthedisjunctionfromtheconsequentmakesfurthersimpliﬁcationpossible.

Atthispoint,wewilljustintroducetheprinciplesinfullgenerality.Theywillbecomemoreunderstandableinthelightoftheirveriﬁcations(forvariousnotionsofconsequence)ine.g.theorem6.2andtheorem9.1.

Tointroducetheprinciplesweneedsomesyntacticaloperations.Wedeﬁnetheoperations[·](·)and{·}(·)onpropositionalformulasasfollows.•

–[B]p:=p,[B]󰀝:=󰀝,[B]⊥:=⊥,–[·](·)commuteswith

∧

and

∨

inthesecondargument,

–[B](C→D):=(B→(C→D)).•

–{B}p:=(B→p),{B}󰀝:=󰀝,{B}⊥:=⊥,–{·}(·)commuteswith

∧

and

∨

inthesecondargument,

–{B}(C→D):=(B→(C→D)).

Notethat[·](·)and{·}(·)donotpreserveprovableequivalenceinthesecondargument.Notealsothat󰀬B→([B]C↔C)and󰀬B→({B}C↔C).Deﬁne[B]X:={[B]C|C∈X}.

Wewillstudythefollowingprinciplesforimplicationforsemi-consequencerelationsonL(P).B2

LetXbeaﬁnitesetofimplicationsandlet

Y:={C|(C→D)∈X}∪{B}.

TakeA:=

󰀁

X.Then(A→B)£[A]Y

B2󰀂

LetXbeaﬁnitesetofimplicationsandlet

Y:={C|(C→D)∈X}∪{B}.

TakeA:=

󰀁

X.Then(A→B)£{A}Y.

B3A£B⇒(p→A)£(p→B).

ItiseasytoseethatB2󰀂canbederivedfromB2overA1-A3.NotethatbothB2,B2󰀂andB3arenon-ordinaryschemes.B2andB2󰀂involveﬁniteconjunctionsanddisjunctionsandB2andB3containvariablesrangingoverpropositionletters.(ItiseasytoseethatonecanreplaceB2󰀂byanequivalentschemethatmakesnospecialmentionofpropositionletters.Seealso[Iem99].)Thefactthatpropositionlettersarenot‘generic’inB2andB3,reﬂectsourinterestincertainspecialsubstitutions,likesubstitutionsofΣ-sentences.Ifwespellouttheconclusionofe.g.B2,weget:

󰀄

(A→B)£{[A]C|(C→D)∈XorC=B}.WegiveanexampleofauseofB2.Suppose£satisﬁesB2.Let

E:=((p→q)∧(r→(s∨t))),F:=(E→(u∨(p→r))).

ThenwehaveF£(p∨r

∨

u∨(E→(p→r))).

Remark3.1RosalieIemhoﬀhasshownthatB2󰀂cannotbereplacedbyﬁnitely

manyconventionalschemes.Thisisanimmediateconsequenceofthemethodsdevelopedin[Iem99].IconjecturethatasimilarresultholdsforB2.

WesaythatarelationsatisfyingA1,A2,A3,B1,B2,B3isaσ-relation.WesaythatarelationsatisfyingA1,A2,A3,B1,B2󰀂isanα-relation.Wetake󰀁σtobethesmallestσ-relation,i.o.w󰀁σisthesemi-consequencerelationaxiomatizedbyA1,A2,A3,B1,B2,B3.Similarly,󰀁αisthesmallestα-relation.

4Preservativity

Inthissectionweintroducepreservativityrelationswhicharespecialsemi-consequencerelations.Infact,wewilltreatsomesemi-consequencerelationsthatarenotpreservativityrelations:wewillalsoconsiderrelationslikeprovablydeductiveconsequence.Treatmentofthesefurtherrelationsispostponedtillsection12.

4.1BasicDeﬁnitions

ConsideragainanylanguageBofpropositionalorpredicatelogic.IfA∈L(P)andf:P→B,thenfAistheresultofsubstitutingfpforpinAforeachp∈P.IfwewanttostressthatwearespeakingoffasL(P)→Bwewilluse[f].LetX⊆B,letTbeanytheoryinBandletFbeasetoffunctionsfromPtoB.Wewrite:

•forA,B∈B,A£T,XB:⇔∀C∈X(C󰀬TA⇒C󰀬TB)•forA,B∈L(P),A£T,X,FB:⇔∀f∈FfA£T,XfB.

IfY⊆BandF=YP,wewillwrite£T,X,Yfor£T,X,F.IfXorFaresingletonswewillomitthesingletonbrackets.IfB=L(P)andT=IPC,wewilloftenomit‘T’intheindex.Wewillcall£T,X,F,T,X,F-preservativity,etcetera.Wewillcallthe£T,X,Fandthe£T,Xpreservativityrelations.Wewillcallthe£T,Xpurepreservativityrelations.

Clearly£T,Xisasemi-consequencerelationoverTand£T,X,Fisasemi-consequencerelationoverIPC.Belowwewillprovideanumberofmotivatingexamplesforourdeﬁnitions.

Remark4.1Itisinstructivetocomparepreservativitywithconservativity(ofsentencesoveratheory).Deﬁne:

•ForA,B∈B,A£∗T,XB:⇔∀C∈X(B󰀬TC⇒A󰀬TC)

SoA£∗T,XBmeansthatT+BisconservativeoverT+Aw.r.t.X.ForclassicaltheoriesTwehave:󰀂

A£T,XB⇔¬B£∗T,¬X¬A,where¬X:={¬C|C∈X}.

Thus,intheclassicalcasepreservativityisasuperﬂuousnotion.Inthecon-structivecase,however,thereductiongivenin󰀂doesnotwork.Notethat

conservativityasarelationbetweensentencesoveratheoryisanaturalexten-sionofthenotionofconservativitybetweentheories.Thereisnoanalogueofthisforpreservativity.

ItshouldbenotedthatΠ02-conservativitybetweentheoriesisacentralcon-ceptualtoolfortheorycomparison.Theonlyothernotionsoftheorycompari-sonofcomparableimportancearerelativeinterpretabilityandveriﬁablerelativeconsistency.Π01-conservativityforREextentensionsofPeanoArithmetic,PA,inthelan-guageofPAisequivalenttorelativeinterpretabilityforthesetheories.Intheconstructivecase,relativeinterpretabilityplaysamuchmoremodestrole.Manytranslationsthatdonotcommutewiththelogicalconnectives,playasigniﬁcantrole.Moreover,themetamathematicalpropertiesofrelativeinterpretabilityaremuchdiﬀerent.WecertainlydonothaveanythingresemblingtheconnectionbetweenrelativeinterpretabilityandΠ1-conservativity.Π01-conservativityofsentencesoverHeyting’sArithmetic,HA,isreducibletoΣ-preservativityoverHAby:•

A£∗B⇔¬B£HA,Σ0¬A.HA,Π01

Asanauxiliarynotiontoprovemetamathematicalresults,Σ-conservativityover

HAisthemoreusefulnotion,aswillbeillustratedinterestofthepaper.

4.2ExamplesofPreservativityRelations

Inthissubsectionweprovideexamplesofpreservativityrelationsandwereviewsomeresultsfromtheliteratureconcerningtheseexamples.

4.2.1TheLogicofaTheory

IfwetakeX:=B,then£T,Xissimplyequalto󰀬T.Moreinterestinglyweconsider£T,B,F.Itiseasytoseethat:

A£T,B,FB⇔∀f∈FfA󰀬TfB.

Wedeﬁne:

•ΛT,F:={A|∀f∈FT󰀬fA}.

•ΛT:=ΛT,BP.ThetheoryΛTisthepropositionallogicofT.Itiseasytoseethat:

A£T,B,FB⇔ΛT,F󰀬(A→B)ΛT,F󰀬A⇔󰀝£T,B,FA

DeJongh’sCompletenessTheoremforΣ-substitutionstellsusthatΛHA=ΛHA,Σ=IPC.TherearemanydiﬀerentproofsofDeJongh’stheorem,seee.g.[Smo73]or[Vis85]or[dJV96].4.2.2

AdmissibleConsequence

IfwetakeX:={󰀝},then,forA,B∈B,weﬁnd

A£T,󰀅B⇔(T󰀬A⇒T󰀬B).

Thus£T,󰀅istherelationofdeductiveconsequenceforT.Moreover,forA,B∈L(P),

A£T,󰀅,FB⇔∀f∈F(T󰀬fA⇒T󰀬fB).Weﬁndthat£T,󰀅,FisadmissibleconsequenceforTw.r.t.F.Wedeﬁne:•A∼T,FB:⇔A£T,󰀅,FB,•A∼TB:⇔A∼T,BB.

Wewillprovidemoreinformationaboutadmissibleconsequenceinsubsec-tion4.4.4.2.3

AResultofPitts

SupposeQ⊆P.LetR:=P\\Q.Consider£IPC,L(Q).Bytheorem5.3below,incombinationwithlemma4.2(2)below,£IPC,L(Q)isanearly-consequencere-lation.AndrewPitts,inhis[Pit92],showsthatforeveryA∈L(P),thereisaformula(∀RA)∈L(Q),suchthatforallB∈L(P):A£IPC,L(Q)B⇔∀RA󰀬B.ForasemanticaltreatmentofPitt’sresultsee[GZ95a]or[Vis96].Ofrelatedinterestisthepaper[GZ95b].

4.3BasicFacts

Wecollectsometechnicalfactsaboutpreservativity.AformulaAofBisT-primeif,foranyﬁnitesetofB-formulasZ,A󰀬TZ⇒∃B∈ZA󰀬TB.NotethatifAisT-prime,thenA󰀅T⊥.AclassofformulasXisweaklyT-disjunctiveifeveryA∈XisequivalenttothedisjunctionofaﬁnitesetofT-primeformulasY,withY⊆X.

ForanyclassofformulasX,letdisj(X)betheclosureofXunderarbitrarydisjunctions.Inthenextlemmawecollectanumberofnoteworthysmallfactsonpreservativity.

Lemma4.21.£T,Xisasemi-consequencerelationoverT.£T,X,Fisa

semi-consequencerelationoverIPC.2.SupposeXisweaklyT-disjunctive,then£T,Xand£T,X,Farenearly-consequencerelations.3.SupposeXisclosedunderconjunction,then:

C∈XandA£T,XB⇒(C→A)£T,X(C→B).

4.Letrange(F)betheunionoftherangesoftheelementsofF.Supposethatrange(F)⊆XandthatXisclosedunderconjunction,then£T,X,FsatisﬁesB3.5.SupposeA∈X.ThenA£T,XB⇔A󰀬TB.

6.SupposeX⊆YandF⊆G,then£T,Y⊆£T,Xand£T,Y,G⊆£T,X,F.7.£T,disj(X)=£T,Xand,hence,£T,disj(X),F=£T,X,F.

8.Letid:P→L(P)betheidenticalembedding.Then£IPC,X,id=£IPC,X.9.IfThasthedisjunctionproperty,then∼Tand∼T,FsatisfyB1.

Proof

Wetreat(2)and(3).(2)SupposeXisweaklyT-disjunctiveandA£T,XCandB£T,XC.LetEbeanyelementofX.SupposeYisaﬁnitesetofT-primeformulasinXsuchthatEisequivalenttothedisjunctionofY.Wehave:

󰀄

E󰀬TA∨B⇒Y󰀬TA∨B

⇒

⇒⇒⇒⇒

∀F∈YF󰀬TA∨B

∀F∈YF󰀬TAorF󰀬TB∀F∈YF󰀬TC󰀄

Y󰀬TCE󰀬TC13

B1for£T,X,FisimmediatefromB1for£T,X.

(3)SupposethatXisclosedunderconjunctionandthatA£B.LetC,E∈XandsupposethatE󰀬(C→A).Then(E∧C)󰀬Aand,hence,(E∧C)󰀬B.ErgoE󰀬(C→B).PThenextlemmaisquiteusefulbothtoverifyleftadjointnessandtoshowthatcertainclassesofformulasareequalmoduloIPC-provableequivalence.Lemma4.3Let£beasemi-consequencerelationoverIPCandletΨ:L(P)→L(P),letX⊆L(P).Supposethat1.A£ΨA,2.ΨA󰀬IPCA,3.range(Ψ)⊆X,4.£⊆£IPC,X.Then,wehave:

•A£B⇔A£IPC,XB⇔ΨA󰀬IPCB,

•X=range(Ψ)moduloIPC-provableequivalence.

Proof

Undertheassumptionsofthelemma.Wehave:

A£B

⇒⇒⇒⇒⇒

A£IPC,XBΨA£IPC,XBΨA󰀬IPCBΨA£BA£B

assumption(4)assumption(2),(4)lemma4.2(5)assumption1

ConsideranyB∈X.WehaveB£ΨB.Hence,byassumption(4)andlemma4.2(5),B󰀬IPCΨB.Combiningthiswithassumption(2),weﬁndIPC󰀬B↔ΨB.PWeproveabasictheoremaboutadmissibleconsequence.Deﬁnef󰀕g:=[f]◦g.Itiseasytoseethat󰀕isassociativeandtheidenticalembeddingofPintoL(P)istheidentityfor󰀕.

Theorem4.4Suppose,ΛT,F=IPC.Moreover,supposethatG⊆L(P)Pandthat,foranyg∈Gandf∈F,(f󰀕g)∈F.Then,∼T,F⊆∼IPC,G.

Proof

SupposeA∼T,FBand󰀬gA.Consideranyf∈F.Clearly󰀬TfgA,i.e.󰀬T(f󰀕g)A.Since(f󰀕g)∈F,weﬁnd:󰀬T(f󰀕g)B.Hence,forallf∈F,󰀬TfgBand,hence,󰀬gB.PNotethatitfollowsthat∼IPCismaximalamongthe∼TwithΛT=IPC.

4.4ASurveyofResultsonPreservativity

Inthissectionwegiveanoverviewofresultsconcerningpreservativity.4.4.1

DerivabilityforIPC

TheminimalpreservativityrelationoverIPCis󰀬IPC.ThereisanextensionHA∗ofHA(seeinsubsection8.2),suchthat󰀬IPC=∼HA∗=∼HA∗,Σ.ThisresultwasprovedbydeJonghandVisserintheirpaper[dJV96],adaptingaresultofShavrukov(see[Sha93]or[Zam94]).NotethatbydeJongh’stheoremisalsofollowsthat:£HA,A,A=£HA,A,Σ=󰀬IPC.4.4.2

AdmissibleConsequenceforIPC

∼IPCisthemaximalrelation∼TfortheoriesTwithΛT=IPC.Thiswasshowninsubsection4.3.∼IPCstrictlyextends󰀬IPC.E.g.theindependenceof

premissruleIP

¬p→(q

∨

r)∼IPC(¬p→q)∨(¬p→r)

isadmissiblebutnotderivable.Wehavethefollowingfacts.

1.∼IPCisdecidable.ThisresultisduetoRybakov.Seethepaper[Ryb92]orthebook[Ryb97].Theresultfollowsalso,alongadiﬀerentroute,fromtheresultsin[Ghi99]or,alternatively,fromtheresultsin[Iem99].2.Theembeddingof󰀬IPCinto∼IPChasaleftadjoint,say(·)󰀁.Sowehave:

A∼IPCB⇔A󰀁󰀬IPCB.

ThisresultisduetoGhilardi.Seehispaper[Ghi99].(·)󰀁doesnotcom-mutewithconjunction.

3.Thefollowingsemi-consequencerelationsareidentical:

∼IPC,

∼HA,

∼HA,BΣ,£IPC,EX,󰀁α.

Webrieﬂydiscusstheindividualidentities.

•∼IPC=∼HA.ThisresultisduetoVisser.Seehispaper[Vis99].Theresultcanbeobtainedinadiﬀerentwayviatheresultsof[Iem99]andtheresultsofthispaper.Wewillgivetheargumentinsection11.

•∼IPC=∼HA,BΣ.ThisresultisduetodeJonghandVisser.Seetheirpaper[dJV96],corollary6.6.•∼IPC=£IPC,EX.ThisresultisimmediatefromtheresultsindeJonghandVisser’spaper[dJV96].HereEXisthesetofexactfor-mulas.Seee.g.[dJV96]foradeﬁnition.

Ghilardi’sresultmentionedabovein(2)strengthensthistheorem,since,asitturnsout,therangeof(·)󰀁ispreciselydisj(EX).•∼IPC=󰀁α.ThisresultwasobtainedbyIemhoﬀ.Seeherpaper[Iem99].

4.4.3

AdmissibleRulesforΣ-SubstitutionsoverHA

Obviously∼HA,Σextends∼HA,andthus,ipsofacto,∼IPC.Itfollowsfromresultstobeprovedbelowthat¬¬p→p∼HA,Σp∨¬p.However,wedonothave¬¬p→p∼IPCp∨¬p,aswitnessedbythesubstitutionp→¬q.

Wewillconnect∼HA,Σ,i.e.HA-admissibleconsequenceforΣ-substitutions,withtheformulaclassesNNIL,ROBandf-ROB.NNILisintroducedinsub-section2.ROBandf-ROBaredeﬁnedinsection6below.WeshowthatNNIL=ROB=f-ROB(modIPC).Theresultwasﬁrstprovedinmyunpub-lishedpaper[Vis85].Wewillpresentaversionoftheproofinsection7ofthispaper.Adiﬀerentproof,duetoJohanvanBenthem,iscontainedin[vB95].AversionofvanBenthem’sproofispresentedin[VvBdJdL95].Wewillfurtherprovethefollowingresults:1.∼HA,Σ=£HA,Σ,Σ=£IPC,NNIL=󰀁σ.

2.Theidenticalembeddingof󰀬IPCinto∼HA,Σhasaleftadjoint(·)∗.I.o.w.wehaveA∼HA,ΣB⇔A∗󰀬IPCB.Theseresultswereessentiallyalreadycontainedin[Vis85].

5ApplicationsofKripkeSemantics

Toprepareourselvesforsection6webrieﬂystatesomebasicfactsaboutKripkemodels.

5.1SomeBasicDeﬁnitions

WesupposethatthereaderisfamiliarwithKripkemodelsforIPC.Twogoodintroductionsare[TvD88a]and[Smo73].Ourtreatmenthereismainlyintendedtoﬁxnotations.AmodelisastructureK=󰀯K,≤,󰀃,P󰀰.HereKisanon-emptysetofnodes,≤isapartialorderingand󰀃isarelationbetweennodesandpropositionalatomsinP,satisfyingpersistence:ifk≤k󰀂andk󰀃p,thenk󰀂󰀃p.Wecall󰀃theforcingrelationofK.Weusee.g.PKforthesetofpropositionalvariablesofK,󰀃KfortheforcingrelationofK,etcetera.AmodelKisaP-modelifPK=P.

ConsiderK=󰀯K,≤,󰀃,P󰀰.Wedeﬁnek󰀃AforA∈L(P)inthestandardway.K󰀃Aif,forallk∈K,wehavek󰀃A.

AmodelKisﬁniteifbothKKandPKareﬁnite.ArootedmodelKisastructure󰀯K,b,≤,󰀃,P󰀰,where󰀯K,≤,󰀃,P󰀰isamodelandwhereb∈Kisthebottomelementw.r.t.≤.

Foranyk∈K,wedeﬁneK[k]asthemodel󰀯K󰀂,k,≤󰀂,󰀃󰀂,P󰀰,whereK󰀂:=↑k:={k󰀂|k≤k󰀂}andwhere≤󰀂and󰀃󰀂aretherestrictionsof≤respectively󰀃toK󰀂.(Wewilloftensimplywrite≤and󰀃for≤󰀂and󰀃󰀂.)

5.2TheHenkinConstruction

AsetX⊆L(P)isadequateifitisnon-emptyandclosedundersubformulas(and,hence,contains⊥).AsetΓisX-saturatedif:1.Γ⊆X,2.Γ󰀅⊥,

3.IfΓ󰀬AandA∈X,thenA∈Γ,4.IfΓ󰀬(B

∨

C)and(B

∨

C)∈X,thenB∈ΓorC∈Γ.

LetXbeadequate.TheHenkinmodelHX(P)istheP-modelwithasnodestheX-saturatedsets∆andasaccessibilyrelation⊆.Theatomicforcinginthenodesisgivenby:Γ󰀃p⇔p∈Γ.Wehave,byastandardargument,thatΓ󰀃A⇔A∈Γ,foranyA∈X.NotethatifXandPareﬁnite,thenHX(P)isﬁnite.AdirectconsequenceoftheHenkinconstructionistheKripkeCompletenessTheorem.Letp󰁃⊇pv(A),then:

IPC󰀬A⇔K󰀃A,forall(ﬁnite)p󰁃-modelsK.

5.3MoreDeﬁnitions

LetKbeasetofP-models.MKistheP-modelwithnodes󰀯k,K󰀰fork∈KK,K∈Kandwithordering󰀯k,K󰀰≤󰀯m,M󰀰:⇔K=Mandk≤Km.Asatomicforcingwedeﬁne:󰀯k,K󰀰󰀃p:⇔k󰀃Kp.Inpracticewewillforgetthesecondcomponentsofthenewnodes,pretendingthedomainstobealreadydisjoint.LetKbeaP-model.BKistherootedP-modelobtainedbyaddinganewbottombtoKandbytakingb󰀃p:⇔K󰀃p.Weputglue(K):=BMK.

5.4ThePushDownLemma

WewillassumebelowthatPisﬁxed.Wewilloftennotationallysuppressit.Theorem5.1(PushDownLemma)LetXbeadequate.Suppose∆isX-saturatedandK󰀃∆.Thenglue(HX[∆],K)󰀃∆.

Proof

WeshowbyinductiononA∈Xthatb󰀃A⇔A∈∆.Thecasesofatoms,conjunctionanddisjunctionaretrivial.If(B→C)∈Xandb󰀃(B→C),then∆󰀃(B→C)and,hence,(B→C)∈∆.Conversely,suppose(B→C)∈∆.Ifb󰀁B,weareeasilydone.Ifb󰀃B,then,bytheInductionHypothesis,B∈∆,henceC∈∆and,againbytheInductionHypothesis:b󰀃C.PWesaythat∆is(P-)primeifitisconsistentandif,forevery(C∨D)∈L(P),∆󰀬(C∨D)⇒∆󰀬Cor∆󰀬D.AformulaAisprimeif{A}isprime.Theorem5.2SupposeXisadequateand∆isX-saturated.Then∆isprime.

Proof

∆isconsistentbydeﬁnition.Suppose∆󰀬C∨Dand∆󰀅Cand∆󰀅D.Sup-posefurtherK󰀃∆,K󰀁C,M󰀃∆andM󰀁D.Considerglue(HX(∆),K,M).Bytheorem5.1wehave:b󰀃∆.Ontheotherhand,bypersistence,b󰀁Candb󰀁D.Contradiction.P∼CexhibitednexttoanodemeansthatCisnotforced;thisisnottobeconfusedwith¬Cexhibitednexttoanode,whichmeansthat¬Cisforced.

Theorem5.3ConsideranyformulaA.TheformulaAcanbewritten(moduloIPC-provableequivalence)asadisjunctionofprimeformulasC.MoreovertheseCareconjunctionsofimplicationsandpropositionalvariablesinsub(A).

Proof

Considerasub(A)-saturated∆.Letthesetofimplicationsandatoms󰀁ip(∆)be󰀁

of∆.ItiseasilyseenthatIPC󰀬ip(∆)↔∆.Take:

󰀄󰀃

D:={ip(∆)|∆issub(A)-saturatedandA∈∆}.Trivially:IPC󰀬D→A.OntheotherhandifIPC󰀅A→D,thenbyastandardconstructionthereisasub(A)-saturatedsetΓsuchthatA∈ΓandΓ󰀅D.Quodnon.PRemark5.4NotethatinthedeﬁnitionofDin5.3,wecanrestrictourselvestothe⊆-minimalsub(A)-saturated∆withA∈∆.

6RobustFormulas

Inthissectionwestudyrobustformulas.Wewillverifythat£IPC,ROBisaσ-relation,andthusthat󰀁σ⊆£IPC,ROB.

Weaimatapplicationoflemma4.3to󰀁σintheroleof£,andROBintheroleofX.ThemappingΨneededfortheapplicationoflemma4.3,willbethemapping(·)∗providedinsection7.

ConsiderP-modelsKandM.Wesaythat:•K⊆M:⇔∃f:KK→KM(fisinjectiveandf◦≤K⊆≤M◦f

and∀k∈KK,p∈P(k󰀃Kp⇔f(k)󰀃Mp)).

ModulotheidentiﬁcationoftheelementsofKwiththeirf-imagesinM,clearly‘K⊆M’meansthatKisasubmodelofM.ROBistheclassofformulasthatispreservedundersubmodels.

Asubmodelisfulliftheneworderingrelationistherestrictionoftheoldorderingrelationtothenewworlds.Wedonotdemandofoursubmodelsthattheyarefull.However,allorresultsworkforfullsubmodelstoo.•A∈ROB:⇔Aisrobust:⇔∀M(M󰀃A⇒∀K⊆MK󰀃A).

Wewillletσ,σ󰀂,τ,...rangeoverROB.ItiseasytoseethatNNIL⊆ROB.Insection7wewillseethatmoduloIPC-provableequivalenceeachrobustformulaisinNNIL.

Let’stakeasalocalconventionofthissectionthat£:=£IPC,ROB.ClearlywehavethatP⊆ROBandthatROBisclosedunderconjunction.Soitfollowsthat£satisﬁesA1,A2,A3,B3.ToverifyB1,bylemma4.2(2),thefollowingtheoremsuﬃces.

Theorem6.1ROBisweaklydisjunctive.

Proof

ConsideranyA∈ROB.WewriteAindisjunctivenormalformDAasintheorem5.3andremark5.4.ConsideranydisjunctC(∆)ofDA.Here,asin5.4,∆isa⊆-minimalsub(A)-saturatedsetwithA∈∆andC(∆)istheconjunctionoftheatomsandimplicationsin∆.WeclaimthatC(∆)isrobust.ConsideranymodelsK⊆M󰀃C(∆).Trivially,M󰀃∆.BythePushDownLemma5.1,glue(Hsub(A)[∆],M)󰀃∆.Hence,glue(Hsub(A)[∆],M)󰀃A.Nowclearly,

glue(Hsub(A)(∆),K)⊆glue(Hsub(A)(∆),M).BythestabilityofAwegetglue(Hsub(A)(∆),K)󰀃A.Consider

Γ:={G∈sub(A)|glue(Hsub(A)(∆),K)󰀃G}.

ClearlyΓ⊆∆.Moreover,Γissub(A)-saturatedandA∈Γ.Bythe⊆-minimalityof∆weﬁndΓ=∆.Hence,glue(Hsub(A)(∆),K)󰀃C(∆)andsoK󰀃C(∆).ErgoC(∆)isrobust.PTheorem6.2£isclosedunderB2.

Proof

LetX󰀁beaﬁnitesetofimplicationsandletY:={C|(C→D)∈X}∪{B}.LetA:=X.Wehavetoshow:(A→B)£[A]Y.Theproofisbycontraposition.ConsideranyH∈ROBandsuppose:H󰀅󰀂[A]Y.LetK=󰀯K,b,≤,󰀃,P󰀰bearootedmodelsuchthatK󰀃HandK󰀁[A]Y,i.e.forallE∈Y,wehaveK󰀁[A]E.

LetK󰀂:=K{A}:=󰀯K󰀂,b,≤󰀂,󰀃󰀂,P󰀰,bethefullsubmodelofKonK󰀂:={b}∪{k󰀂∈K|k󰀂󰀃A}.Notethat{k󰀂∈K|k󰀂󰀃A}isupwardsclosedandthaton{k󰀂∈K|k󰀂󰀃A}theoldandthenewforcingcoincide.Moreover,onthisclass,foranyG,wehavethat[A]GisequivalentwithG.

Weclaimthat,forallF,b󰀃󰀂F⇒b󰀃[A]F.TheproofoftheclaimisbyasimpleinductiononF.Thecasesofatoms,disjunctionandconjunctionaretrivial.SupposeFisanimplicationandb󰀃󰀂F.Thencertainly,forallk∈K,(k󰀃A⇒k󰀃󰀂F).Sinceonthekwithk󰀃A,󰀃and󰀃󰀂coincide,weﬁndb󰀃(A→F),i.e.b󰀃[A]F.

Wereturntothemainproof.Rememberthat:b󰀃Handb󰀁[A]C,forallCwith(C→D)∈Xandb󰀁[A]B.Weshowthatb󰀃󰀂Handb󰀃󰀂Aandb󰀁󰀂B.

Itisimmediatethatb󰀃󰀂H,sinceK󰀂isasubmodelofKandHisrobust.RememberthatAistheconjunctionofthe(C→D)inX.Soitissuﬃcienttoshowthat,foreach(C→D)inX,b󰀃󰀂(C→D).Considerany(C→D)∈Xandanyk󰀂≥󰀂bwithk󰀂󰀃󰀂C.Sinceb󰀁[A]C,wehave,bytheclaim,b󰀁󰀂C.Sok󰀂=b.Butthenk󰀂󰀃A,hencek󰀂󰀃󰀂Aand,thus,k󰀂󰀃󰀂(C→D).Wemayconcludethatk󰀂󰀃󰀂Dand,hence,b󰀃󰀂(C→D).

Fromb󰀁[A]Bandtheclaimwehaveimmediatelythat:b󰀁󰀂B.PAlltheproofsinthissectionalsoworkwhenwereplaceROBbyf-ROB,thesetofformulaspreservedbyfullsubmodels.NotethatROB⊆f-ROB.Ourresultinsection7willimply:ROB=f-ROB=NNIL(moduloIPC-provableequivalence).

7TheNNIL-Algorithm

Inthissectionweproducethealgorithmthatisthemaintoolofthispaper.Theexistenceofthealgorithmestablishesthefollowingtheorem.

Theorem7.1ForallAthereisanA∗∈NNIL(pv(A))suchthatA󰀁σA∗andA∗󰀬A.

Beforeproceedingwiththeproofof7.1weinterpolateacorollary.Corollary7.2

1.LetAandA∗beaspromisedby7.1.Thenwehave

A󰀁σB⇔A£IPC,ROBB⇔A∗󰀬IPCB.

2.NNIL=ROB=f-ROB(modIPC)

Proof

Itisimmediatefromthefactthatboth£IPC,ROBand£IPC,f-ROBareσ-relationsthat󰀁σ⊆£IPC,ROBand󰀁σ⊆£IPC,f-ROB.Moreoverwehaverange((·)∗)⊆NNIL⊆ROB⊆f-ROB.Combiningthiswiththeresultoftheorem7.1,wecanapplylemma4.3toobtainthedesiredresults.P7.2(2)wasprovedbypurelymodeltheoreticalmeansbyJohanvanBenthem.Seehis[vB95]or,alternatively,[VvBdJdL95].TheadvantageofvanBenthem’sproofisitsrelativesimplicityandthefactthatthemethodemployedeasilygeneralizes.Theadvantageofthepresentmethodistheextrainformationitproduces,liketheaxiomatizationof£IPC,ROBanditsusefulnessinthearith-meticalcase,seesections9,10,11and12.ItisanopenquestionwhethervanBenthem’sproofcanbeadaptedtothearithmeticalcase.

Remark7.3Combiningcorollary7.2withtheresultsof[VvBdJdL95],weob-tainthefollowingsemanticalcharacterizationof󰀁σ.

A󰀁σB⇔∀M(∀K⊆MK󰀃A⇒M󰀃B).

Weproceedwiththeproofoftheorem7.1.Fortherestofthissectionwewrite£:=󰀁σ.Forconveniencewereproducetheaxiomsandrulesof£here.A1A2A3B1B2

A󰀬B⇒A£B

A£BandB£C⇒A£CC£AandC£B⇒C£(A∧B)A£CandB£C⇒(A∨B)£C

LetXbeaﬁnitesetofimplicationsandlet

Y:={C|(C→D)∈X}∪{B}.

TakeA:=B3

󰀁

X.Then,(A→B)£[A]Y

A£B⇒(p→A)£(p→B)

Proofoftheorem7.1

Weintroduceanordinalmeasureoofcomplexityonformulasasfollows:•I(D):={E∈sub(D)|Eisanimplication}•iD:=max{|I(E)||E∈I(D)}(Here|Z|isthecardinalityofZ)

•cD:=thenumberofoccurrencesoflogicalconnectivesinD

•oD:=ω·iD+cD

Notethatwecountoccurrencesofconnectivesforcandtypesofimplications,notoccurrences,fori.WesaythatanoccurenceofEinDisanouteroccurrenceifthisoccurrenceisnotinthescopeofanimplication.

Theproofoftheorem7.1proceedsasfollows.Ateverystagewehaveaformulaandassociatedwithitcertaindesignatedsubformulas,thatstillhavetobesimpliﬁed.Astepoperatesononeofthesesubformulas,sayA.EitherAwillloseitsdesignationandanumberofitssubformulaswillgetdesignatedorAwillbemodiﬁed,saytoA󰀂,andanumberofsubformulasofA󰀂willreplaceAamongthedesignatedformulas.ThesubformulasBreplacingAamongthedesignatedformulaswillsatisfy:oB2

strictlysmallerones.Thismeansthatwearedoingarecursionoverωω.

Wewillexhibitthepropertiesof£thatareusedineachstepbetweensquarebrackets.

αAtoms:[A1]SupposeAisanatom.TakeA∗:=A.

βConjunction:[A1,A2,A3]:SupposeA=(B∧C).ClearlyoBγDisjunction:[A1,A2,B1]SupposeA=(B∨C).ClearlyoBδImplication:[A1,A2,A3,B2,B3]SupposeA=(B→C).Wesplitthestepintoseveralcases.

δ1Outerconjunctionintheconsequent:[A1,A2,A3]SupposeChasanouterocurrenceofaformulaD∧E.PickanyJ(q)besuchthat:•qisafreshvariable,•qoccurspreciselyonceinJ,

•qisnotinthescopeofanimplicationinJ,•C=J[q:=(D

∧

E)].

LetC1:=J[q:=D],C2:=J[q:=E].AsiseasilyseenCisIPC-provablyequivalenttoC1∧C2.LetA1:=(B→C1)andA2:=(B→C2).ClearlyAisIPC-provablyequivalenttoA1∧A2.WeprovethatoAi23

ConsideranyimplicationFinI(A1).IfF=A1,wemapFtoA.OtherwiseF∈I(B)orF∈I(J)orF∈I(D)(sinceqdoesnotoccurinthescopeofanimplication).InallthreecaseswecanmapFtoitself.SinceA1cannotbeinI(B)orI(J)orI(D),ourmappingisinjective.Thecasethati=2issimilar.

∗

SetA∗:=(A∗1∧A2).δ2Outerdisjunctionintheantecedent:[A1,A2,A3]Thiscaseiscompletelyanalogoustothepreviousone.

IfAhasnoouterdisjunctionintheantecedentandnoouterconjunctionintheconsequent,thenBisaconjunctionofatomsandimplicationsandCisadisjunctionofatomsandimplications.Itiseasytosee,thatapplicationsofasso-ciativity,commutativityandidempotencytotheconjunctionintheantecedentorto󰀁thedisjunction󰀂intheconsequentdonotraiseo.Sowecansafelywrite:B=XandC=Y,whereXandYareﬁnitesetsofatomsorimplications.Thisleadsustothefollowingcase.

δ3Bisaconjunctionofatomsandimplications,Cisadisjunctionofatomsandimplications[A1,A2,A3,B2,B3]δ3.1Xcontainsanatom:[A1,A2,B3]

δ3.1.1󰀁Xcontainsapropositionalvariable,sayp:[A1,A2,B3]ConsiderD:=(X\\{p})andE:=(D→C).Clearly󰀬A↔(p→E)andoEδ3.2Xcontainsnoatoms:[A1,A2,A3,B2]Thiscase—thelastone—isthetrulydiﬃcultone.Tomotivateitstreatment,let’ssolvethediﬃcultiesonebyone.Weﬁrstlookatanexample.

Example7.4Consider(p→q)→r.B2givesus((p→q)→r)£(p∨r).However,wedonothave:(p∨r)󰀬((p→q)→r).Wecanrepairthisbynotingthat((p→q)→r)󰀬(q→r)and(q→r)∧(p∨r)󰀬((p→q)→r).Sothefullsolutionofourexampleisasfollows.

Wehave((p→q)→r)£((q→r)∧(p∨r)),by:

a)((p→q)→r)£(p∨r)b)((p→q)→r)󰀬(q→r)c)((p→q)→r)£(q→r)

d)((p→q)→r)£((q→r)∧(p∨r))

B2IPCA1a,c,A3

Moreover,((q→r)∧(p∨r))󰀬((p→q)→r)and

((q→r)∧(p∨r))∈NNIL(pv((p→q)→r)).

Weimplementthisideaforthegeneralcase.Therewillbeaproblemwitho,butwewillpostponeitsdiscussionuntilwerunintoit.AisoftheformB→C,whereBisaconjunctionofaﬁnitesetofimplicationsXandCisadisjunctionofaﬁnitesetofatomsorimplicationsY.ForanyD:=(E→F)∈X,let:

󰀃

B↓D:=((X\\{D})∪{F}).Clearlyo((B↓D)→C)LetZ:={E|(E→F)∈X}∪{C}.PutA0:=[B]Z.WewillshowthatourproblemreducestothequestionwhetherA∗0exists.Soforthemomentwepretenditdoes.Wehave:

A£A0B2

∗

A0£A0assumption

∗

A£A01,2,A2∀D∈XA󰀬((B↓D)→C)IPC∀D∈XA£((B↓D)→C)4,A1

∗

∀D∈X((B↓D)→C)£((B↓D)→C)IH

∗

∀D∈X5,6,A2󰀁A£((B↓D)→∗C)∗

A£({((B↓D)→C)|D∈X}∧A0)3,7,A3󰀁

Itisclearthat({((B↓D)→C)∗|D∈X}∧A∗0)∈NNIL(pv(A)).Weshowthat:󰀃

{((B↓D)→C)∗|D∈X}∧A∗0󰀬A.󰀁

Itissuﬃcienttoshow:{((B↓D)→C)|D∈X}∧[B]E󰀬A,foreachE∈Z.IncaseE=C,weareimmediatelydoneby:[B]C󰀬B→C.Suppose(E→F)∈X󰀁forsomeF.ReasoninIPC.Suppose{󰀁((B↓D)→C)|D∈X},[B]EandB.WewanttoderiveC󰀁.Wehave(((X\\{E→F})∧F)→C),[B]EandB.FromBweﬁnd(X\\{E→F})and(E→F).FromBand󰀁[B]E,wederiveE.FromEand󰀁(E→F)wegetF.Finallyweinferfrom(((X\\{E→F})∧F)→C),(X\\{E→F})andFthedesiredconclusionC.HereendsourdiscussioninsideIPC.

SotheonlythinglefttodoistoshowthatA∗0exists.IfiA0=0,weareeasilydone.SupposeiA0>0.IfforeachEinZwithiE>0,wewouldhavei([B]E)Westudysomeexamples.Theseexamplesshowthatwecannotgenerallyhopetogeti([B]E)∗

andhasiR25

2)3)4)5)6)7)8)

Example7.5Consider(p→q)→(r→s).TakeE:=C=(r→s).Wehave[B]E=[p→q](r→s)=(p→q)→(r→s).Sonosimpliﬁcationisobtained.However[B]EisIPC-provablyequivalentto((r∧(p→q))→s),whichhasloweri.ByA1,A2wecanput([B]E)∗:=((r∧(p→q))→s)∗.Wecouldhaveappliedthereductionbeforegoingto[B]E.Wedidnotchoosetodosoforreasonsofuniformityoftreatment.

Example7.6Consider(((p→q)→r)→s).TakeE:=(p→q).Weﬁnd[B]E=[(p→q)→r](p→q)=(((p→q)→r)→(p→q)).[B]EisIPC-provablyequivalentto((p∧(q→r))→q),whichhasloweri.

Consider[B]EforE∈Z={E|(E→F)∈X}∪{C}.[B]Eistheresultofreplacingouterimplications(G→H)ofEby(B→(G→H)).IfthereisnoouterimplicationinE,weﬁndthat[B]E=Eandi([B]E)=0.Inthiscase[B]EisimplicationfreeandhenceafortioriinNNIL.Wecanput([B]E)∗:=E.SupposeEhasanouterimplication.

Consideranyouterimplication(G→H)ofE.Weﬁrstshow:i(B→(G→H))≤i(B→C).WedeﬁneaninjectionfromI(B→(G→H))toI(B→C).AnyimplicationoccurringinI(B)orI(G→H)canbemappedtoitselfinI(B→C).Noneoftheseimplicationshasasimage(B→C),since(G→H)∈I(B)∪I(C).Sowecansend(B→(G→H))to(B→C).

Thenextstepistoreplace(B→(G→H))byanIPC-provablyequivalentformulaKwithlowervalueofi.LetB󰀂betheresultofreplacingalloccurrencesof(G→H)inBbyHandletK:=((G∧B󰀂)→H).ClearlyKisprovablyequivalentto(B→(G→H)).Weshowthati(K)Wedeﬁneanon-surjectiveinjectionfromI(K)toI(B→(G→H)).Con-sideranimplicationMinI(K).IfM=Kwesenditto(B→(G→H)).SupposeM=K,i.e.M∈I(B󰀂)∪I(G)∪I(H).AsubformulaNofI(B)∪I(G)∪I(H)isapredecessorofMifMistheresultofreplacingalloccurrencesof(G→H)inNbyH.ClearlyMhasatleastonepredecessorandanypredecessorofMmustbeanimplication.SendMtooneofitsshortestpredecessors.Clearlyourfunctionisinjective,sincetwodiﬀerentimplicationscannotshareapredecessor.Finally(G→H)cannotbeintherangeofourinjection.Ifitwere,wewouldhaveM=H,butthenHwouldbeashorterpredecessor.Acontradiction.

Replaceeveryouterimplicationin[B]Ebyanequivalentwithlowervalueofi.TheresultisthedesiredQ.

Remark7.7Thealgorithmgivenwithourproofisnon-deterministicallyspec-iﬁed.Howeverbycorollary7.2theresultisuniquemoduloprovableequivalence.Ididn’ttrytomakethealgorithmoptimallyeﬃcient.

In[Vis85]asimpleadaptationoftheNNILalgorithmisgivenfor£IPC,󰀅.HerethealgorithmcomputesnotavalueinNNIL,butavaluein{󰀝,⊥}.Thusweobtainanalgorithmthatchecksforprovability.Itiseasytousethepresentalgorithmforthispurposetoo,sincethereisap-timealgorithmtodecideIPC-provabilityofNNIL0formulas,i.e.formulaswithonlypropositionalvariables

infrontofarrows.TheoutputsofouralgorithmareinNNIL0.IthasbeenshownbyRichardStatman(see[Sta79])thatcheckingwhetheraformulaisIPC-provableisp-spacecomplete.Thisputsanabsoluteboundonwhatanalgorithmlikeourscando.

Example7.8[Samplecomputations]Weusesomeobviousshort-cuts.

(¬¬p→p)→(p∨¬p)

(p→(p∨¬p))∧([¬¬p→p]¬¬p∨[¬¬p→p]p∨[¬¬p→p]¬p)¬¬p∨p∨¬p

((⊥→p)∧([¬p]p∨[¬p]⊥))∨p∨¬pp∨¬p

((p→q)→r)→s

(r→s)∧([(p→q)→r](p→q)∨[(p→q)→r]s)(r→s)∧(((p∧(q→r))→q)∨s)(r→s)∧((p→((q→r)→q))∨s)

(r→s)∧((p→((r→q)∧([q→r]q∨[q→r]q)))∨s)(r→s)∧((p→q)∨s).

≡≡≡≡

≡≡≡≡≡

8.1

BasicFactsandNotationsinArithmetic

ArithmeticalTheories

ThearithmeticaltheoriesTconsideredinthispaperareREtheoriesinA,thelanguageofHA.Thesetheoriesallextendi-S12,theintuitionisticversionofBuss’theoryS12.Anothersalienttheoryisintuitionisticelementaryarithmetic,i-EA:=i-I∆0+Exp,theconstructivetheoryof∆0-inductionwiththeaxiomexpressingthattheexponentiationfunctionistotal.i-EAisﬁnitelyaxiomatiz-able;westipulatethataﬁxedﬁniteaxiomatizationisemployed.WewillusePTfortheformalizationofprovabilityinT.Inthepresentpaper,wearemostlyinterestedinextensionsofHA,sowewilnotworrytoomuchaboutdetailsconcerningweaktheories.

SupposeAisaformula.PTAmeansProvT(t(󰁃x)),whereProvTisthearith-metizationoftheprovabilitypredicateofTandwhere󰁃xisthesequenceofvariablesoccuringinAandt(󰁃x)istheterm‘theG¨odelnumberoftheresultofsubstitutingtheG¨odelnumbersofthenumeralsofthe󰁃x’sforthevariablesinA’.Supposee.g.that11,12and15code,respectively,‘(’,‘)’and‘=’,that∗isthearithmetizationofthesyntacticaloperationofconcatenationandthatnumisthearithmetizationofthenumeralfunction.Underthesestipulationse.g.PT(x=x)means:ProvT(11∗num(x)∗15∗num(x)∗12).6

notationalconventionintroducesascopeambiguity.Fortunatelybystandardmeta-mathematicalresults,weknowthataslongasthetermsweemploystandforT-provablytotalrecursivefunctionsthediﬀerentreadingsareprovablyequivalent.Inthispaperwewillonlyemploytermsforp-timecomputablefunctions,sotheambiguityisharmless.

6Our

SupposeTextendsi-EA.WewriteTnforthetheoryaxiomatizedbytheﬁnitelymanyaxiomsofi-EA,plustheaxiomsofTwhicharesmallerthanninthestandardG¨odelnumbering.WewriteProvT,nfortheformalizationofprovabilityinTn.WeconsiderProvT,nasaformofrestrictedprovabilityinT.Thefollowingwellknownfactisquiteimportant:

Theorem8.1SupposeTisanREextensionofHAinthelanguageofHA.ThenTisessentiallyreﬂexive(veriﬁablyinHA).I.e.forallnand,forallA-formulasAwithfreevariables󰁃x,T󰀬∀󰁃x(PT,nA→A).And,usingUCfor‘theuniversalclosureof’,evenHA󰀬∀x∀A∈FORAPTUC(PT,xA→A).

Proof

(Sketch)Theproofisroughlyasfollows.Ordinarycut-eliminationforcon-structivepredicatelogic(ornormalizationincasewehaveanaturaldeductionsystem)canbeformalizedinHA.ReasoninHA.Letanumberxandafor-mulaAbegiven.Introduceameasureofcomplexityonarithmeticalformulasthatcountsboththedepthofquantiﬁersandofimplications.FindysuchthatboththeaxiomsofTxandAhavecomplexityABriefIntroductiontoHA∗

InthissubsectionwedescribethetheoryHA∗.Thistheorywillbeemployedintheproofoftheorem10.2.Insection12wewillstudytheclosedfragmentofHA∗.

ThetheoryHA∗wasintroducedin[Vis82].HA∗istoBeeson’sfp-realizability,introducedin[Bee75],asTroelstra’sHA+ECT0istoKleene’sr-realizability.Thismeansthatforasuitablevariantoffp-realizabilityHA∗isthesetofsen-tencessuchthattheirfp-translationsareprovableinHA.ThetheoryHA∗isHAplustheCompletenessPrincipleforHA∗.TheCompletenessPrinciplecanbeviewedasanarithmeticallyinterpretedmodalprinciple.TheCompletenessPrincipleviewedmodallyis:CC[T]

󰀬A→PA󰀬A→PTA.

TheCompletenessPrincipleforaspeciﬁctheoryTis:

WehaveHA∗=HA+C[HA∗].7Webrieﬂyreviewsomeoftheresultsof[Vis82]and[dJV96].

naturalwaytodeﬁneHA∗isbyaﬁxedpointconstructionas:HAplustheComplete-nessPrincipleforHA∗.HereitisessentialthattheconstructionisveriﬁableinHA.

7The

•LetAbethesmallestclassclosedunderatomsandallconnectivesexceptimplication,satisfying:A∈Σ1andB∈A⇒(A→B)∈A.NotethatmoduloprovableequivalenceinHAallprenexformulas(oftheclassicalarithmeticalhierarchy)areinA.HA∗isconservativew.r.t.AoverHA.NotethatNNIL0(Σ)⊆A.•ThereareinﬁnitelymanyincomparableTwithT=HA+C[T].HoweverifT=HA+C[T]veriﬁablyinHA,thenT=HA∗.•LetKLS:=Kreisel-Lacombe-Shoenﬁeld’sTheoremonthecontinuityoftheeﬀectiveoperations.WehaveHA∗󰀬KLS→PHA∗⊥.ThisimmediatelygivesBeeson’sresultthatHA󰀅KLS[Bee75].

•EveryprimeREHeytingalgebraHcanbeembeddedintotheHeytingalgebraofHA∗.ThismappingisprimitiverecursiveintheenumerationofthegeneratorsofHw.r.twhichHisRE.Themappingsendsthegen-eratorstoΣ-sentences[dJV96].WeinsertsomebasicfactsontheprovabilitylogicofHA∗.Thesematerialswillbeonlyneededinsection12.Clearly,HA∗satisﬁestheL¨obconditions.L1L2L3L4

󰀬A⇒󰀬PA

󰀬P(A→B)→(PA→PB)󰀬PA→PPA󰀬P(PA→A)→PA

i-KisgivenbyIPC+L1,L2.i-Lisi-K+L3,L4.Wewritei-K{P}fortheexten-sionofi-KwithsomeprincipleP.Notethati-L{C}isvalidforprovabilityinterpretationsinHA∗.

AprinciplecloselyconnectedtoCistheStrongL¨obPrinciple:SL

󰀬(PA→A)→A

AsaspecialcaseofSLwehave󰀬¬¬P⊥.

Theorem8.2i-L{C}isinterderivablewithi-K{SL}.

Proof

L4isimmediatefromSL.Weshow“i-K{SL}󰀬C”.Reasonini-K{SL}.SupposeA.IteasilyfollowsthatP(A∧PA)→(A∧PA),and,hence,bySL,thatA∧PA.WemayconcludethatPA.

Weshow“i-L{C}󰀬SL”.Reasonini-L{C}.Suppose(PA→A).Itfollows,byC,that:(PA→A)∧P(PA→A).Hence,byL¨ob’sPrinciple,(PA→A)∧PAandthusA.P29

9ClosurePropertiesofΣ-Preservativity

InthissectionweverifytwoclosurepropertiesofΣ-preservativityoverHAinHA.

9.1ClosureunderB1

WewillshowthatHAveriﬁesthatΣ-preservativityisclosedunderB1foranysubstitutions.Weproducebothproofsknowntous.Theﬁrstoneemploysq-realizability.ThisformofrealizabilityisatranslationfromAtoA,duetoKleene.Itisdeﬁnedasfollows:•xqP:=P,forPatomic

•xq(A∧B):=((x)0qA∧(x)1qB)•xq(A∨B):=(((x)0=0→(x)1qA)•xq∃yA(y):=(x)0qA((x)1)•xq∀yA(y):=∀y∃z({x}y󰀑z1.HA󰀬xqA→A

2.foranyA∈Σandanyset{y1,...,yn}withFV(A)⊆y1,...,yn,wecanﬁndanindexesuchthatHA󰀬A→∃z({e}(y1,...,yn)󰀑z∧zqA)3.SupposeB1,...,Bn,Chavefreevariablesamong{y1,...,ym}andthat{x1,...,xn}isdisjointfrom{y1,...,ym}.SupposeB1,...,Bn󰀬HAC.Then,forsomee,wehave:

x1qB1,···,xnqBn󰀬HA∃z({e}(x1,...,xn,y1,...,ym)󰀑z

∧

((x)0=0→(x)1qB))

∧

•xq(A→B):=∀y(yqA→∃z({x}y󰀑zzqB))∧(A→B)

zqA(y)))

ThefollowingfactscanbeveriﬁedinHA.

zqC).

Theproofsareallsimpleinductions.Fordetailsthereaderisreferredto[Tro73],188–202.WewillnowshowthatΣ-preservativitysatisﬁesB1.ItiseasilyseenthatourproofisveriﬁableinHA.Wereasonasfollows:

α)β)γ)δ)󰀄)η)ζ)θ)ι)κ)λ)

A£HA,ΣCB£HA,ΣC

S∈ΣandHA󰀬S→(A∨B)

xqS󰀬HA∃z({e}(x)󰀑z∧zq(A∨B))S󰀬HA∃z({e}(f)󰀑z∧zq(A∨B))S∧∃z({e}(f)󰀑z∧(z)0=0)󰀬HAAS∧∃z({e}(f)󰀑z∧(z)0=0)󰀬HABS∧∃z({e}(f)󰀑z∧(z)0=0)󰀬HACS∧∃z({e}(f)󰀑z∧(z)0=0)󰀬HACS󰀬HA∃z({e}(f)󰀑z∧(z)0=0)∨

∃z({e}(f)󰀑z∧(z)0=0)

S󰀬HAC

assumptionassumptionassumption

γ,eprovidedby(3)δ,fprovidedby(2)󰀄󰀄η,αζ,β󰀄θ,ι,κ

ThesecondproofemploysatranslationduetoDickdeJongh.Forlateruseourdeﬁnitionisslightlymoregeneralthanisreallyneededfortheproblemathand.LetCbeanA-sentenceandletnbeanaturalnumber.Wewrite,locally,PnforPHA,n.Deﬁneatranslation[C]n(·)asfollows.•[C]nP:=PforPatomic•[C]n(·)commuteswith∧,∨,∃•[C]n(A→B):=([C]nA→[C]nB)

∧

Pn(C→(A→B))

•[C]n∀yA(y):=∀y[C]nA(y)∧Pn(C→∀yA(y))

Let’sﬁrstmakeafewquickobservations,thatmakelifeeasier.Wewrite[C]nΓ:={[C]nD|D∈Γ}.Wehave:‡i)HA󰀬[C]nA→Pn(C→A)

‡ii)HA󰀬[C]n((A→B)∧(A󰀂→B󰀂))↔

([C]nA→[C]nB)∧([C]nA󰀂→[C]nB󰀂)∧Pn(C→((A→B)∧(A󰀂→B󰀂))).

Similarlyforconjunctionsofmorethantwoimplications.

‡iii)HA󰀬[C]n∀y∀zA(y,z)↔(∀y∀z[C]nA(y,z)∧Pn(C→∀y∀zA(y,z))).

Similaryforlargerblocksofuniversalquantiﬁers.‡iv)HA󰀬[C]n∀y(A(y)→B(y))↔

∀y([C]nA(y)→[C]nB(y))∧Pn(C→∀y(A(y)→B(y))).‡v)HA󰀬[C]n∀y‡vii)Γ󰀬HA,nA⇒[C]nΓ󰀬HA[C]nA(veriﬁablyinHA).(‡v)isimmediatefromthewellknownfactthat

HA󰀬∀y(‡vi)isimmediatefrom(‡v).

Proofof(‡vii)TheproofisbyinductionontheproofwitnessingΓ󰀬HA,nA.Wetreattwocases.

FirstcaseΓ=∅andAisaninductionaxiom,sayforB(x),ofHAn.Clearly[C]nAisHA-provablyequivalentto:

((

[C]nB0∧

∀x([C]nBx→[C]nB(x+1))∧

Pn(C→∀x(Bx→B(x+1))))→(∀x[C]nBx∧Pn(C→∀xBx)))∧

Pn(C→A).

Wehave:HA󰀬PnA,and,hence,HA󰀬Pn(C→A).Soitfollowsthat:

HA󰀬Pn(C→∀x(Bx→B(x+1)))→Pn(C→∀xBx).

Moreover(asaninstanceofinductionfor[C]nBx):

HA󰀬([C]nB0∧∀x([C]nBx→[C]nB(x+1)))→∀x[C]nBx.

Combiningtheseweﬁndthepromised:HA󰀬[C]nA.

SecondcaseSupposethatA=(D→E)andthatthelaststepintheproofwasby:

Γ,D󰀬HA,nE⇒Γ󰀬HA,nD→E.FromΓ,D󰀬HA,nE,wehave,bytheInductionHypothesis,[C]nΓ,[C]nD󰀬HA,n[C]nEand,hence,[C]nΓ󰀬HA,n[C]nD→[C]nE.Moreover,forsomeﬁniteΓ0⊆Γ,wehaveΓ0,D󰀬HA,nE.LetBbetheconjunctionoftheelementsofΓ0.Weﬁnd:[C]nΓ󰀬HA,nPn(C→B)and󰀬HA,nPn(B→(D→E)).Hence,[C]nΓ󰀬HA,nPn(C→(D→E)).Wemayconclude:

[C]nΓ󰀬HA,n([C]nD→[C]nE)

∧

Pn(C→(D→E)).

argumentcanbeveriﬁedinassumptionassumptionassumptionγ

δ,(‡vii)󰀄,(‡vi),(‡i)theorem8.1α,ζ

theorem8.1β,ιη,θ,κ

Hereendsourproofof(‡vii).

Wenowproveourprinciple.AsiseasilyseentheHA.

α)A£HA,ΣCβ)B£HA,ΣC

γ)S∈ΣandHA󰀬S→(A∨B)δ)forsomenS󰀬HA,n(A∨B)󰀄)[󰀝]nS󰀬HA([󰀝]nA∨[󰀝]nB)η)S󰀬HA(PnA∨PnB)ζ)HA󰀬PnA→Aθ)HA󰀬PnA→Cι)HA󰀬PnB→Bκ)HA󰀬PnB→Cλ)HA󰀬(S→C)

9.2AClosureRuleforImplication

ToformulateournextclosureruleitisconvenienttoworkinaconservativeextensionofHA.LetA+beAextendedwithnewpredicatesymbols(includingthe0-arycase)forΣ-formulas.LetfbesomeassignmentofΣ-formulasofAoftheappropriatearitiestothenewpredicatesymbols.WeextendftoA+intheobviousway.Deﬁne[·]◦[·]](·):A+→Aasfollows:n(·)and[•[[A]]P:=[A]◦nP:=fPforPatomic•[[A]](·)and[A]◦n(·)commutewith∧,

∨

and∃

•[[A]](B→C):=f(A→(B→C)),[A]◦n(B→C):=Pnf(A→(B→C))•[[A]]∀xB(x):=f(A→∀xB(x)),[A]◦n∀xB(x):=Pnf(A→∀xB(x))

Wehave,forBinA+,extendingthenumberingof‡-principlesofsubsection9.1:

‡viii)ThefollowingimplicationsarederivableinHA:[fA]n(fB)→[A]◦nB,

◦

[A]nB→[[A]]Band[[A]]B→(A→B).‡ix)[A]◦nBisprovablyequivalenttoaΣ-formula.

Theproofof(‡viii)isaneasyinductiononB.(‡ix)istrivial.

Theorem9.1󰀁SupposeXisaﬁnitesetofimplicationsinA+andletBbein

Y:={C|(C→D)∈X}∪{B}.Wehave,veriﬁablyA+.SayA:=X.Let󰀂

inHA,f(A→B)£HA,Σ[[A]]Y.

Beforegivingtheproofoftheorem9.1,weﬁrstdrawacorollary.Corollary9.2ThefollowingfactsareveriﬁableinHA.1.£HA,Σ,ΣisclosedunderB2.2.£HA,Σ,AisclosedunderB2󰀂.

3.Σ8ofappendixCisHA-validforΣ-preservativity.

Weleavetheeasyveriﬁcationofthecorollarytothereader.Weproceedwiththeproofoftheorem9.1.

Proof

Toavoidheavynotationswesuppress‘f’.InthecontextofHAweassumethatanA+-formulaisautomaticallytranslatedviaftothecorrespondingA-formula.LetSbeaΣ-sentence(ofA).SupposeS󰀬HA(A→B).Itfollowsthat,forsomen,S󰀬HA,n(A→B)and,hence,by(‡vii)[A]nS󰀬HA[A]n(A→B).By(‡ii)and(‡vi)weﬁnd:

󰀃

S󰀬HA({[A]nC→[A]nD|(C→D)∈X}∧Pn(A→A))→[A]nB,andso:

S󰀬HA

󰀃

{[A]nC→[A]nD|(C→D)∈X}→[A]nB.

Itfollowsby(‡viii)that:

󰀃

◦

S󰀬HA{[A]◦nC→[A]nD|(C→D)∈X}→[A]nB.

SinceHAisasubtheoryofPA,weget:

󰀃

◦

S󰀬PA{[A]◦nC→[A]nD|(C→D)∈X}→[A]nB.

󰀂

Byclassicallogic,wegetS󰀬PA[A]◦nY.RememberthatPAis,veriﬁably󰀂◦inHA,conservativeover󰀂HA◦w.r.tΠ2-sentences(see[Fri78]).󰀂Since(S→[A]nY)isΠ2,wegetS󰀬HA[A]nY.Ergo,by(‡viii),S󰀬HA[[A]]Y.PBeforeclosingthissectionweinsertsomeremarksontheproof.

Remark9.31.Theaboveproofwasobtainedafteranalyzinganargument

in[dJ82].2.ThestepinvolvingconservativityofPAoverHAusestheG¨odel-Friedmantranslation.Closerinspectionrevealsthattheargumentathandjustre-quirestheFriedmantranslation.Wegiveasketchoftheproofbelow.ItfollowsthatourresultsgeneralizetoallessentiallyreﬂexiveREexten-sionsTofHAthatareclosedbothundertheFriedmanandthedeJonghtranslation.3.Itseemstomethat,fromasuﬃcientlyabstractperspective,itshouldbecomeclearthatourpresentproofisjustavariantoftheproofof6.2.Thus,{G|Pn(A→G)}inthepresentproofwouldcorrespondtothegreypartoftheKripkemodelinthepicturebelow6.2.[A]n(·)wouldcorrespondtotheoperationofaddingthebottom-nodeinthepicture(viaSmory´nski’soperation)tothegreypart.ThedetourviaPAwouldcorre-spondtothefactthatourKripkemodelargumentisessentiallyclassical.ThespecialbehaviourofΣ-sentencesundertranslationwouldcorrespondwiththefactthatwhetheraΣ-sentenceisforcedornot(inamodelofHA)isdependentjustonthenodeunderconsiderationandnotonothernodes.Letmeposeitasaproblemtofurtherdevelopsuchaperspective.Weprovetheclaimof(2):weshowthatthedoublenegationtranslationcanbeeliminatedfromtheproofof9.1.Wepickuptheprooffromthepointwherewehaveproved:

󰀁◦

a)S󰀬HA{[A]◦nC→[A]nD|(C→D)∈X}→[A]nB.

󰀂H

LetH:=[A]◦ofanarithmeticalformulanY.TheFriedmantranslation(E)

Eis(modulosomedetailstoavoidvariable-clashes)theresultofreplacingallatomicformulasPinEby(P∨H).Oneeasilyshows:b)HA󰀬E⇒HA󰀬(E)Hc)HA󰀬H→(E)H

d)forS∈Σ,HA󰀬(S)H↔(SBy(a),(b)and(d)wehave:

∨

H).

e)S

∨

H󰀁󰀬HA◦

{(([A]nC)∨H)→([A]nD)H|(C→D)∈X}→(([A]◦nB)∨H).

By(e)andpropositionallogicweﬁnd:󰀁

f)S󰀬HA{H→([A]nD)H|(C→D)∈X}→H.Soby(f)and(c):g)S󰀬HAH.

Hence,by(g)and(‡viii),S󰀬HA

󰀂[[A]]Y.

10OnΣ-Substitutions

InthissectionweproveourmainresultsonΣ-substitutions.Giventheresultswealreadyhave,thisisrathereasy.

Theorem10.1£HA,Σ,Σis,veriﬁablyinHA,aσ-relation.

Proof

EverypreservativityrelationsatisﬁesA1-3,and,hence,sodoes£HA,Σ,Σ.More-over,£HA,Σ,ΣsatisﬁesB1invirtueofourresultofsubsection9.1.£HA,Σ,ΣsatisﬁesB2bycorollary9.2.£HA,Σ,ΣsatisﬁesB3bylemma4.2(4).ItiseasytoseethatallthestepsareveriﬁableinHA.PLetRbeanyarithmeticallydeﬁnablerelation.WewriteRHAfortherelationgivenby:mRHAn:⇔HA󰀬mRn.Theorem10.2Thefollowingrelationsarecoextensive:

(a)󰀁σ,(b)£HAHA,Σ,Σ,(c)£HA,Σ,Σ,(d)∼HA,Σ,(e)∼HA,Σ.

Proof

Bytheorem10.1,£HAHA,Σ,Σisaσ-relation.So,(a)⊆(b).SinceHAissound,weﬁnd(b)⊆(c).Bylemma4.2(6),(c)⊆£HA,󰀅,Σ=(e).

Sincetheargumentforlemma4.2(6)isjustuniversalinstantiation,itisveriﬁable

inHA.Hence(b)⊆(d).

BythesoundnessofHA,wehave(d)⊆(e).

Weshowthat(e)⊆(a),i.e.∼HA,Σ⊆󰀁σ.SupposenotA󰀁σB.Then,bycorollary7.2(1),A∗󰀅IPCB.A∗isIPC-provablyequivalenttoadisjunctionof

primeNNIL-formulas.Itfollowsthatforsomesuchdisjunct,sayC,C󰀅IPCB.TheHeytingalgebraHaxiomatizedbyCisprimeandRE.Bytheembeddingtheoremprovedin[dJV96](seesection8.2ofthispaper)thereisanf∈ΣP,suchthatHA∗󰀬fCandHA∗󰀅fB.SincefC∈NNIL(Σ),wehavebytheNNIL(Σ)-conservativityofHA∗overHA(provedin[Vis82];seealsosection8.2forthestatementofthefullresult),thatHA󰀬fC.SinceHAisasubtheoryofHA∗,wehaveHA󰀅fB.SinceIPC󰀬C→A,itfollowsthatHA󰀬fAandHA󰀅fB.Wemayconclude:notA∼HA,ΣB.PRemark10.3(1)ApropositionalformulaAisHA,Σ-exactiﬀthereisasub-stitutionf∈ΣP,suchthatHA󰀬fB⇔A󰀬IPCB,i.o.w.ifAaxiomatizesthe‘theoryoff’,i.e.ΛHA,{f}.Seealso[dJV96].Theproofoftheorem10.2estab-lishesalsothattheprimeNNIL-formulasarepreciselytheHA,Σ-exactformulas.(2)Bytheorem10.2,∼HA,Σisaσ-relation.Note,however,thatitisnotHA-provablyaσ-relation.ThereasonisthatclosureunderB1isnotveriﬁable.Toprovethis,supposeHAveriﬁesB1.LetRbethestandardRossersentence.SoRsatisﬁesHA󰀬R↔PHA¬R≤PHAR.LetR⊥:=PHARHA

theotherhand,from(a),(b)andtheassumedveriﬁableclosureunder∼HA,Σ,weﬁndthat(e)HA󰀬PHA(R∨R⊥)→PHA⊥.Combining(d)and(e),wegetHA󰀬PHAPHA⊥→PHA⊥.Quodnon,byL¨ob’sTheorem.

11TheAdmissibleRulesofHA

TheresultsofRosalieIemhoﬀ[Iem99]implythefollowingtheorem.

Theorem11.1(Iemhoﬀ)∼IPC=󰀁α.Inotherwords:theadmissiblerulesofIPCareaxiomatizedbyA1,A2,A3,B1,B2󰀂.FromIemhoﬀ’sresult,wederivethefollowingtheorem.Theorem11.2Thefollowingrelationsarecoextensive:

(a)󰀁α,(b)£HAHA,Σ,A,(c)£HA,Σ,A,(d)∼HA,(e)∼HA,(f)∼IPC.

Proof

Weﬁrstshowthat(a)⊆(b).Itisclearlysuﬃcienttoshowthat£HA,Σ,AisHA-veriﬁablyanα-relation.ClosureunderA1-3istrivial.Moreover,£HA,Σ,A

satisﬁesB1invirtueofourresultofsubsection9.1.£HA,Σ,AsatisﬁesB2bycorollary9.2.

BythesoundnessofHA,wehave(b)⊆(c)and(d)⊆(e).

Bylemma4.2(6),(c)⊆£HA,󰀅,A=(e).Sincelemma4.2(6)isveriﬁableinHA,wealsohave(b)⊆(d).

Since,bydeJongh’stheorem,ΛHA=IPC,weﬁnd,bytheorem4.4,that(e)⊆(f).

Finally,bytheorem11.1,(f)⊆(a).

P12ClosedFragments

Inthissectionwestudytheclosedfragmentsoftheprovabilitylogicsofthreetheories.TheﬁrstisthetheoryHA∗.ThesecondisPeanoArithmetic,PA.ThethirdisHA.Wewillﬁrstintroducesomedeﬁnitionsanprovesomebasicfacts.

12.1Preliminaries

Considerthelanguageofmodalpropositionallogicwithoutpropositionalvari-ables.Let’scallthislanguageL2,0.SoL2,0isgivenasfollows.•A::=⊥|󰀝|(A∧A)|(A∨A)|(A→A)|PA.

LetTbeanytheoryextending,say,i-S12,theintuitionisticversionofBuss’S2.WhatisrelevanthereisjustthatarithmetizationofmetamathematicsshouldbepossibleinTandthatTveriﬁestheL¨obconditions.WecanmaptheformulasofL2,0,sayviaeT,tothelanguageofT,bystipulatingthateTcommuteswithallthepropositionalconnectivesincluding󰀝and⊥andthat

eTPA:=PTeTA:=ProvT(gn(eTA)).

TheclosedfragmentCToftheprovabilitylogicofTisthesetofAinL2,0suchthatT󰀬eTA.

Animportantclass,DF,ofclosedformulasisformedbythedegreesoffalsityPα⊥,whereαrangesoverω+:=ω∪{∞}.Here:•P0⊥:=⊥,•Pn+1⊥:=PPn⊥,•P∞⊥:=󰀝,

Wewilloftenusetheevidentmappingsdf:α→Pα⊥and󰀐:Pα⊥→α.

Tolinktheclosedfragmentstotheframeworkofthispaper,wewillstudypurelypropositionaltheoriesassociatedtothesefragments.Thelanguageofthesepropositionaltheoriesistheusuallanguageofpropositionallogicwithas‘propositionalatoms’thedegreesoffalsity.Theseatomsfunctionmoreasconstantsthanaspropositionalvariables.WecallthislanguageBDF.SoBDFisgivenasfollows.

•A::=Pα⊥|(A∧B)|(A∨B)|(A→B).

WewillconsidertheoriesΘinBDF,whichsatisfy(atleast)intuitionisticpropo-sitionallogicandtheupaxiom:up󰀬Pn⊥→Pn+1⊥.

TheminimalsuchtheorywillbecalledUP.SoUPisaxiomatizedbyIPCandup.WewillsaythatΘisDF-irreﬂexiveifPα⊥󰀬ΘPβ⊥⇒α≤β.ItiseasytoshowthatUPisDF-irreﬂexive.NotethatsubtheoriesofDF-irreﬂexivetheoriesareDF-irreﬂexive.

AnarithmeticaltheoryTwillhaveassociatedtoitthepropositionaltheoryΛT,eT:={A∈BDF|T󰀬eTA}.(StrictlyspeakingeThereistherestrictionofeTasdeﬁnedabovetoBDF.)

WewillwritePαT⊥foreT(P⊥).WewillsaythatTisDF-soundif,fornon∈ω,T󰀬PnT⊥.Lemma12.1SupposeTisDF-sound.Then,ΛT,eTisDF-irreﬂexive.

Proof

SupposewehavePα⊥󰀬ΛT,eTPβ⊥.Weassume,toobtainacontradiction,that

ββ+1

β<α.Then,bydeﬁnition,Pα⊥󰀬TPβT⊥󰀬TPT⊥.Itfollowsthat:PTT⊥andβ∈ω.ByL¨ob’sRule,weobtainT󰀬PβT⊥.Butthisisimpossible,byDF-soundness.Ergoα≤β.PThefundamentalstructureinthestudyofclosedfragmentsisω+:=ω∪{∞}={0,1,2,···∞}equippedwiththeobviouspartialorder.ω+withpartialordercanbeextendedtoaHeytingalgebra.TheorderingﬁxestheoperationsoftheHeytingalgebrauniquely.Wehave:•󰀝:=∞,⊥:=0,•(α∧β):=min(α,β).•(α∨β):=max(α,β),

󰀅

∞ifα≤β

•(α→β):=

βotherwise

Parabusdelangagewewilluseω+forbothset,partialorderandHeytingalgebra.Wewillputα+∞=∞+α=∞.Wewillrepeatlyusethefollowingconvenientproperty:α+n≤β+n⇒α≤β.

Themapdf:α→Pα⊥canbeconsideredasafunctorfromω+,consideredasacategory,toatheoryΘconsideredasthecategoryofthepreorder󰀬Θ.Wewillbeinterestedintheorieswheredfhasarightadjoint∂Θ,i.e.wherewehave:

•df(α)󰀬ΘA⇔α≤∂ΘA.

Lemma12.2SupposeΘisDF-irreﬂexiveand∂Θexists.Then,∂ΘPα⊥=α.

Proof

Wehave,forDF-irreﬂexiveΘ,

γ≤∂ΘPα⊥⇔Pγ⊥󰀬ΘPα⊥⇔γ≤α.

PWewillwrite∂Tfor∂ΛT,eT.Wecan‘lift’∂ΘfromBDFtoL2,0usingtheauxiliaryfunction(·)aux:L2,0→BDFasfollows.

•(·)auxcommuteswiththepropositionalconnectivesincluding󰀝and⊥,•(PA)aux:=Pdf∂ΘAaux

Wecannowdeﬁne∆Θ:L2,0→ω+,by∆ΘA:=∂ΘAaux.Weshowthat,forDF-irreﬂexiveΘ,∂Θand∆ΘcoincideonBDF-formulas.

Lemma12.3SupposeΘisDF-irreﬂexive.LetA∈BDF.Then∆ΘA=∂ΘA.

Proof

SupposeΘisDF-irreﬂexive.Firstweshow,byinductiononn,that∆ΘPn⊥=n.Forn=0,thisisimmediate.Wehave:

∆ΘPk+1⊥=

=====

∂Θ(Pk+1⊥)aux

∂ΘPdf∂Θ(Pk⊥)aux∂ΘPdf∆ΘPk⊥∂ΘPdf(k)∂ΘPk+1⊥k+1.

Itnowfollowsthat,forA∈BDF,wehaveAaux=A.Thetheoremfollowsdirectlyfromthis.P39

Finally,deﬁne,forA,BinBDF:•A∼T

prov

B:⇔T󰀬PTeTA→PTeTB.

So∼isaformofprovabledeductiveconsequence.NotethatifTisΣ-sound,

prov

thenΛT,eT={A∈BDF|󰀝∼TA}.Wewillwritetheinducedequivalence

prov

relationof∼as≈prov.

Thefollowingtheoremisthemainlemmaforthesubsequentdevelopment.Theorem12.4LetφbeafunctionfromBDFtoω+.WeputΦA:=PφA⊥.NotethatφandΦareinterdeﬁnable.LetTbeatheorycontainingi-S12.LetΘbeaBDF-theorycontainingIPCandup.Weassumethefollowing.Z1TisDF-sound.

Z2ΘisaT-sound,i.e.Θ󰀬A⇒T󰀬eTA,forA∈BDF.Z3ΦA󰀬ΘA.Z4A∼T

prov

ΦA.

Thenwehave:1.Θ=ΛT,eT.

2.Φistheleftadjointoftheembeddingof󰀬Θinto∼T.Inotherwords,

prov

wehave:ΦA󰀬ΘB⇔A∼TB.3.Thefullsubcategoryof󰀬ΘobtainedbyrestrictiontoDFisequivalentto

prov

∼T.Thissubcategoryisisomorphictoω+.4.Thefullsubcategoryof∼TobtainedbyrestrictiontoDFisaskeleton

prov

of∼T.Thissubcategoryisisomorphictoω+.5.φ(Pα⊥)=αandφ=δΘ.6.Wehave,foranyA∈L2,0:

(a)CT󰀬A↔Aaux,(b)CT󰀬A⇔∆ΘA=∞.

prov

Proof

(undertheassumptionsofthetheorem)

Weprove(1).ByZ2,ΘisT-sound.WeshowthatitisalsoT-complete.SupposeT󰀬eTA.ThenT󰀬PTeTA.ByZ4,T󰀬PTeTΦA.ByZ1,itfollowsthatΦA=󰀝.ByZ3,wemayconcludethatΘ󰀬A.

Weprove(2).NotethatfromZ3,4itfollowsthatΦC≈provC.Wehave:T

ΦA󰀬ΘB

⇒

⇒⇒⇒⇒⇒⇒⇒

eTΦA󰀬TeTB

PTeTΦA󰀬TPTeTBPTeTA󰀬TPTeTBPTeTΦA󰀬TPTeTΦBφA+1≤φB+1φA≤φBΦA󰀬ΘΦBΦA󰀬ΘB

prov

Weprove(3).Theequivalenceoftherestrictionof󰀬ΘtoDFand∼T,isimmediatefromlemmaA.1(5).Since,byZ1,TisDF-sound,clearlyΘisDF-irreﬂexive.Hencetherestrictionof󰀬ΘtoDFisisomorphictoω+.

Weprove(4).Therestrictionof∼TtoDFis,bylemmaA.1(4)andZ1,

prov

equivalentto∼T.Triviallytherestrictionisisomorphictoω+.

Weprove(5).Theﬁrstpartisimmediatefromtheassumptionsofthetheorem.Thesecondpartfollowsby:

dfα󰀬ΘA⇔Φdfα󰀬ΘA

prov

⇔dfα∼TA

prov

⇔dfα∼TΦA⇔α≤φA

Sincerightadjointsareuniquemodulonaturalisomorphism,itfollowsthatφ=δΘ.

Weprove(6).Theproofof(6a)isbyinductiononA,usingthat,forB∈BDF,CT󰀬PB↔PΦB.(6b)isimmediatefrom(6a).PWeclosethissectionwithalemma.Lemma12.5LetB∈BDF.Thenwehave:HA󰀬eHAB↔eHA∗B↔ePAB.

prov

Proof

ItiswellknownthatbothHA∗(seesubsection8.2)andPAareHA-provablyΠ02-conservativeoverHA.ItfollowsthatHA󰀬PHA⊥↔PHA∗⊥↔PPA⊥.ThelemmafollowsbyinductiononB.P41

12.2

TheClosedFragmentforHA∗

Insubsection8.2weintroducedHA∗andit’sprovabilitylogic.WesawthatinthislogicatleasttheprinciplesoftheconstructiveversionofL¨ob’sLogicplustheStrongL¨obPrincipleSLP,󰀬(PA→A)→A,hold.

ThepropositionaltheoryUP∗istheBDF-theory,axiomatizedbytherulesofIPCplus

•up󰀬Pn⊥→Pn+1⊥,

•slp󰀬(Pn+1⊥→Pn⊥)→Pn⊥.

WedeﬁneamappingφHA∗:=[[·]]fromBDFtoω∪{∞}asfollows:•[[⊥]]:=0,[[󰀝]]:=∞,•[[A∧B]]:=min([[A]],[[B]]),•[[A∨B]]:=max([[A]],[[B]]),•[[A→B]]:=([[A]]→[[B]]),

DeﬁnefurtherΦHA∗A:=A♦:=P[[A]]⊥.WewillverifyZ1-4oftheorem12.4forHA∗,UP∗and[[·]].

ClearlyHA∗isDF-sound.SowehaveZ1.Moreover,UP∗isHA∗-sound.thuswehaveZ2.Itiseasytosee,byaninductiononthesubformulasofA,thatforAinBDF:

£UP∗󰀬A↔A♦.

Theonlynon-trivialstepisthecaseofimplicationwhichusesslp.Itfollowsthat[[·]]deﬁnesanequivalencebetweenthecategoryofUP∗andω+.

Itisnoweasilyseenthat£immediatelyimpliesbothZ3andZ4.ItfollowsthatUP∗=ΛHA∗,eHA∗.Moreover,since,evidently(·)♦isnaturallyisomorphictotheidentityfunctoron󰀬UP∗,weﬁndthatprovablydeductiveconsequence

prov

andderivableconsequencecoincideforHA∗,i.e.∼HA∗=󰀬UP∗.

12.3TheClosedFragmentofPA

Friedman’s35thproblemwastogiveadecisionprocedurefortheclosedfrag-mentoftheprovabilitylogicofPA.See[Fri75].ItwasindepentlysolvedbyvanBenthem,BoolosandMagari.Topresentthesolutioninourstyle,weﬁrstintro-ducethetheoryUPc.ThisisclassicalpropositionallogicinthelanguageBDFwiththeprincipleup.ByasimplemodeltheoreticargumentonecanshowthatUPc=ΛPA,ePA.Thisfactwillalsofollowfromtheapplicationoftheorem12.4below.Notethat,trivially,UPcisPA-sound.

ConsideranyAinBDF.InUPcwecanrewriteAtoanormalformnf(A)asfollows.FirstwerewriteAtoconjunctivenormalform,obtainingacon-junctionofdisjunctionsofdegreesoffalsityandnegationsofdegreesoffalsity.Thedisjunctionsofdegreesoffalsityandnegationsofdegreesoffalsitycanbe

rewrittentoimplicationsfromconjunctionsofdegreesoffalsitytodisjunctionsofdegreesoffalsity.Finally,usingup,wecancontractconjunctionsofde-greesoffalsityanddisjunctionsofdegreesoffalsitytosingledegreesoffalsity.󰀁α

Thusweobtainaformulanf(A)oftheformi(Pi⊥→Pβi⊥).Wedeﬁne:ΦPA:=(·)♥:=(·)♦◦nf.Here(·)♦isthefunctorfromsubsection12.2.

WeverifyZ1-4oftheorem12.4forPA,UPcand(·)♦.Z1,2aretrivial.Wehave:

•UPc󰀬A↔nf(A),

•(nf(A))♦󰀬UPcnf(A)󰀬UPcA.

Theseconditemissimplybyinspectingthecomputationof(·)♦onaformulaofthespecialformnf(A).Fromtheabove,wehaveZ3.Moreoverwehave:

PPAePAA󰀬PA

󰀬PA

PPAePAnf(A)PPAePA(nf(A))♦.

(1)(2)

Thesteplabeled(2)isbyasimpledirectcomputation:ﬁrstbringthecon-junctionsoutsidetheboxandthenapplyL¨ob’stheoremtotheconjuncts(ifappropriate).ThuswehaveprovedZ4.

Remark12.6Thereisanalternativewaytoprove(2)oftheaboveargument.

PA󰀬PPAePAA→

→→→→→

PPAePAnf(A)PHAeHAnf(A)PHA∗eHA∗nf(A)PHA∗eHA∗(nf(A))♦PHAeHA(nf(A))♦PPAePA(nf(A))♦

(3)(4)(5)(6)(7)(8)

Step(3)isshownsimplybyclassicallogic.(4)usesﬁrsttheHA-veriﬁableΠ02-conservativityofPAoverHAand,thenlemma12.5.(5)isbylemma12.5.(6)usestheresultsofsubsection12.2.(7)employstheHA-veriﬁableΠ02-∗

conservativityofHAoverHA.(8)isbylemma12.5.

Ofcourse,thissecondargumentisasillywayofproving(2).Itismorediﬃcult,itusesmoretheoryanditislessgeneral(ifwereplacePAbyotherclassicaltheories).However,ituncoversananalogywiththeargumentwearegoingtogiveforthecaseofHA.

WehaveveriﬁedtheassumptionsZ1-4oftheorem12.4.ThetheoremgivesusthedesiredcharacterizationoftheclosedfragmentofPA.

Ourargument,whichisjustaformofpresentingtheclassicalargument,forthevanBenthem-Magari-BoolosresultworksforallDF-soundREextensions

ofBuss’sS1IncontrasttheproofofSolovay’sArithmeticalCompleteness2.

TheoremonlyworksasfarasweknowifExpispresent.

8However,

aswepointedout,theargumentofremark12.6doesnotworkingeneral.

12.4TheClosedFragmentofHA

DeﬁneΦHA:=(·)♣:=(·)♦◦(·)∗.Here(·)∗isthefunctordescribedinsection7.WewillverifyZ1-4oftheorem12.4withUPintheroleofΘ.Z1andZ2areimmediate.Wehave:

(A∗)♦

󰀬UP󰀬UP

A∗A

(9)(10)

(9)usesthefactthatA∗∈NNILandasimpleinductionofthecomplexityofNNIL-formulas.(10)isimmediatefromtheresultsofsection7.ThuswehaveprovedZ3.Finallywehave:

HA󰀬PHAeHAA→

→→→

PHAeHAA∗PHA∗eHA∗A∗

PHA∗eHA∗(A∗)♦PHAeHA(A∗)♦

(11)(12)(13)(14)

Step(11)followsfromtheorem10.2incombinationwiththeresultsofsection7.Step(12)useslemma12.5.(13)employstheresultsofsubsection12.2.(14)is

∗

bytheHA-veriﬁableΠ01-conservativityofHAovrHAandbylemma12.5.ThuswehaveveriﬁedZ4.

Example12.7[Samplecomputations]Oftenthecharacterizationof(·)♣byA♣=P∂UPA⊥,providesaquickwaytocomputeA♣.FirstoneguessesthebestapproximationfrombelowinDFofA,thenoneproves,e.g.usingaKripkemodel,thattheconjecturedapproximationisindeedbest.Intheexamplesbelowweuseouralgorithm.Wewrite≈for≈provHA.1.ConsiderA:=¬P⊥→PP⊥.WeﬁndthatA∗=P⊥

A≈P2⊥.2.ConsiderA=(¬¬PP⊥→PP⊥)→(P⊥PP⊥.WecomputeA∗.

∨

PP⊥.Hence,

¬P⊥).LetB:=¬¬PP⊥→

A≈(PP⊥→(P⊥∨¬P⊥))∧

([B]¬¬PP⊥∨[B]P⊥∨[B]¬P⊥)

≈(PP⊥→(P⊥∨¬P⊥))∧(¬¬PP⊥∨P⊥∨¬P⊥)≈(PP⊥→(P⊥∨¬P⊥))∧(PP⊥∨P⊥∨¬P⊥)

Applying(·)♦,weﬁndthatA≈P⊥.

3.ConsiderA=(¬¬P⊥→P⊥)→(PP⊥∨¬PP⊥).LetB:=¬¬P⊥→P⊥.WecomputeA∗,usingsomeshortcutsinvolvingUP-principles.

A≈(P⊥→(PP⊥∨¬PP⊥))∧

([B]¬¬P⊥∨[B]PP⊥∨[B]¬PP⊥)≈¬¬P⊥∨PP⊥∨¬PP⊥≈P⊥∨PP⊥∨¬PP⊥

Applying(·)♦,weﬁndA≈P2⊥.

12.5ComparingThreeFunctors

Inthislastsubsectionofclosedfragments,wecomparethefunctorsΦHA,ΦHA∗andΦPA.Byourpreviousresults,itsuﬁcestocompare∂HA,∂HA∗and∂PA.Wehave:

α≤∂HAA⇔df(α)󰀬UPA

⇒df(α)󰀬UPcA⇔α≤∂PAA

Ergo,∂HAA≤∂PAA.Byasimilarargument,weﬁnd∂HAA≤∂HA∗A.Nowconsiderthefollowingformulas:

•Eα,β,γ:=(¬¬Pα⊥∧Pβ⊥)∨((¬¬Pα⊥→Pα⊥)∧Pγ⊥)

Thenwehave,forα≤βandα≤γ,that∂HAEα,β,γ=α,∂HA∗Eα,β,γ=β,and∂PAEα,β,γ=γ.Thisshowsthat:

{󰀯α,β,γ󰀰∈ω+3|∃A∈BDF∂HAA=α,∂HA∗A=β,∂PAA=γ}

=+3

{󰀯α,β,γ󰀰∈ω|α≤β,α≤γ}.

12.6Questions

1.WhatarethepossibleΛT,eTforDF-soundREextensionsTofi-S12?ItisclearthattheymustbeRE,DF-irreﬂexiveBDF-theoriesextendingUP.2.CharacterizetheclosedfragmentsofHA+ECT0,HA+MPandHA+ECT0+MP.ItseemstomethatcloserinspectionoftheresultsofthepresentpapershouldrevealthattheclosedfragmentofHA+ECT0isthesameastheclosedfragmentofHA.3.IsthereaToftheappropriatekindwhere∼T

adjoint?

prov

doesnothavealeft

References

[Bee75]

M.Beeson.Thenonderivabilityinintuitionisticformalsystemsoftheoremsonthecontinuityofeﬀectiveoperations.TheJournalofSymbolicLogic,40:321–346,1975.

G.Boolos.Thelogicofprovability.CambridgeUniversityPress,1993.

[Boo93]

[Bur98][BV93]

W.Burr.FragmentsofHeyting-Arithmetic.ToappearintheJSL,1998.

A.BerarducciandR.Verbrugge.Ontheprovabilitylogicofboundedarithmetic.AnnalsofPureandAppliedLogic,61:75–93,1993.

D.H.J.deJongh.ThemaximalityoftheintuitionisticpredicatecalculuswithrespecttoHeyting’sArithmetic.TheJournalofSymbolicLogic,36:606,1970.

D.H.J.deJongh.Formulasofonepropositionalvariableinintu-itionisticarithmetic.InA.S.TroelstraandD.vanDalen,editors,TheL.E.J.BrouwerCentenarySymposium,StudiesinLogicandtheFoundationsofMathematics,vol.110,pages51–64.NorthHolland,Amsterdam,1982.

D.H.J.deJonghandL.A.Chagrova.Thedecidabilityofdepen-dencyinintuitionisticpropositionallogic.TheJournalofSym-bolicLogic,60:495–504,1995.

D.H.J.deJonghandA.Visser.EmbeddingsofHeytingalgebras.In[HHST96],pages187–213,1996.

H.Friedman.Onehundredandtwoproblemsinmathematicallogic.TheJournalofSymbolicLogic,40:113–129,1975.H.Friedman.Classicallyandintuitionisticallyprovablyrecursivefunctions.InG.H.M¨ullerandD.S.Scott,editors,HigherSetTheory,pages21–27.SpringerVerlag,Berlin,Heidelberg,NewYork,1978.

Yu.V.Gavrilenko.Recursiverealizabilityfromtheinuitionisticpointofview.SovietMathematicalDokl.,23:9–14,1981.S.Ghilardi.Uniﬁcationinintuitionisticlogic.TheJournalofSymbolicLogic,64:859–880,1999.

R.Grigolia.FreeAlgebrasofNon-classicalLogics.MetsnierebaPress,Tbilisi,1987.InRussian.

S.GhilardiandM.Zawadowski.Asheafrepresentationanddu-alityforﬁnitelypresentedHeytingalgebras.JournalofSymbolicLogic,60:911–939,1995.

S.GhilardiandM.Zawadowski.UndeﬁnabilityofPropositionalQuantiﬁersintheModalSystemS4.StudiaLogica,55:259–271,1995.

[dJ70]

[dJ82]

[dJC95]

[dJV96][Fri75][Fri78]

[Gav81][Ghi99][Gri87][GZ95a]

[GZ95b]

[H´aj96]

[HHST96][Iem99]

[IemXX]

[JdJ98]

[Lei75][Lei80][Lei81][Mac71]

[Pit92]

[Pli77][Pli78][Pli83][Ryb92][Ryb97]

P.H´ajek,editor.G¨odel’96,LogicalFoundationsofMathematics,

ComputerScienceandPhysics—KurtG¨odel’sLegacy.Springer,Berlin,1996.

W.Hodges,M.Hyland,C.Steinhorn,andJ.Truss,editors.Logic:fromfoundationstoapplications.ClarendonPress,Oxford,1996.R.Iemhoﬀ.OntheadmissiblerulesofIntuitionisticPropositionalLogic.PreprintPP-1990-08,ILLC,PlantageMuidergracht24,NL-1018TVAmsterdam,1999.ToappearinJSL.

R.Iemhoﬀ.AmodalanalysisofsomeprinciplesoftheprovabilitylogicofHeytingArithmetic.InProceedingsofAiML’98,volume2,Uppsala,20XX.

G.JaparidzeandD.deJongh.Thelogicofprovability.InS.Buss,editor,Handbookofprooftheory,pages475–546.North-HollandPublishingCo.,amsterdamedition,1998.

D.Leivant.Absolutenessinintuitionisticlogic,volume73.Math-ematicalCentreTract,Amsterdam,1975.

D.Leivant.Innocuoussubstitutions.JournalofSymbolicLogic,45:363–368,1980.

D.Leivant.Implicationalcomplexityinintuitionisticarithmetic.JournalofSymbolicLogic,46:240–248,1981.

S.MacLane.CategoriesfortheWorkingMathematician.Num-ber5inGraduateTextsinMathematics.Springer,NewYork,1971.

A.Pitts.Onaninterpretationofsecondorderquantiﬁcationinﬁrstorderintuitionisticpropositionallogic.JournalofSymbolicLogic,57:33–52,1992.

V.E.Plisko.Thenonarithmeticityoftheclassofrealizablefor-mulas.Math.ofUSSRIzv.,11:453–471,1977.

V.E.Plisko.Somevariantsofthenotionofrealizabilityforpredicateformulas.Math.ofUSSRIzv.,12:588–604,1978.V.E.Plisko.Absoluterealizabilityofpredicateformulas.Math.ofUSSRIzv.,22:291–308,1983.

V.V.Rybakov.Rulesofinferencewithparametersforintuition-isticlogic.JournalofSymbolicLogic,57:912–923,1992.V.V.Rybakov.Admissibilityoflogicalinferencerules.StudiesinLogic.Elsevier,Amsterdam,1997.

[Sha93]

[Smo73]

[Smo85][Sta79][Tro73]

[TvD88a]

[TvD88b]

[vB95]

[Ver93][Vis81][Vis82][Vis85]

[Vis94]

V.Yu.Shavrukov.Subalgebrasofdiagonalizablealgebrasoftheoriescontainingarithmetic.Dissertationesmathematicae(Rozprawymatematycne),CCCXXIII,1993.

C.Smory´nski.ApplicationsofKripkeModels.InA.S.Troelstra,editor,MetamathematicalInvestigationsofIntuitionisticArith-meticandAnalysis,SpringerLectureNotes344,pages324–391.Springer,Berlin,1973.

C.Smory´nski.Self-ReferenceandModalLogic.Universitext.Springer,NewYork,1985.

R.Statman.Intuitionisticpropositionallogicispolynomial-spacecomplete.TheoreticalComputerScience,9:67–72,1979.A.S.Troelstra.Metamathematicalinvestigationsofintuitionisticarithmeticandanalysis.SpringerLectureNotes344.SpringerVerlag,Berlin,1973.

A.S.TroelstraandD.vanDalen.ConstructivisminMathematics,vol1.StudiesinLogicandtheFoundationsofMathematics,vol.121.NorthHolland,Amsterdam,1988.

A.S.TroelstraandD.vanDalen.ConstructivisminMathematics,vol2.StudiesinLogicandtheFoundationsofMathematics,vol.123.NorthHolland,Amsterdam,1988.

J.F.A.K.vanBenthem.TemporalLogic.InDovGabbayetal.,editor,HandbookofLogicinArtiﬁcialIntelligenceandLogicPro-gramming.OxfordUniversityPress,1995.

L.C.Verbrugge.Eﬃcientmetamathematics.ILLC-disserationseries1993-3,Amsterdam,1993.

A.Visser.Aspectsofdiagonalizationandprovability.Ph.D.The-sis,DepartmentofPhilosophy,UtrechtUniversity,1981.A.Visser.Onthecompletenessprinciple.AnnalsofMathematicalLogic,22:263–295,1982.

A.Visser.Evaluation,provablydeductiveequivalenceinHeyt-ing’sArithmeticofsubstitutioninstancesofpropositionalformu-las.LogicGroupPreprintSeries4,DepartmentofPhilosophy,UtrechtUniversity,Heidelberglaan8,3584CSUtrecht,1985.A.Visser.PropositionalcombinationsofΣ-sentencesinHeyting’sArithmetic.LogicGroupPreprintSeries117.DepartmentofPhi-losophy,UtrechtUniversity,Heidelberglaan8,3584CSUtrecht,1994.

[Vis96][Vis98a]

A.Visser.Uniforminterpolationandlayeredbisimulation.In[H´aj96],pages139–164,1996.A.Visser.AnOverviewofInterpretabilityLogic.InM.Kracht,M.deRijke,H.Wansing,andM.Zakharyaschev,editors,Ad-vancesinModalLogic,vol1,CSLILectureNotes,no.87,pages307–359.CenterfortheStudyofLanguageandInformation,Stanford,1998.

A.Visser.SubmodelsofKripkemodels.LogicGroupPreprintSeries189,DepartmentofPhilosophy,UtrechtUniversity,Heidelberglaan8,3584CSUtrecht,http://www.phil.uu.nl/preprints.html,1998.ToappearinArchiveforMathematicalLogic.

A.Visser.RulesandArithmetics.TheNotreDameJournalofFormalLogic,40(1):116–140,1999.

J.vanOosten.AsemanticalproofofdeJongh’stheorem.ArchiveforMathematicalLogic,31:105–114,1991.

[Vis98b]

[Vis99][vO91]

[VvBdJdL95]A.Visser,J.vanBenthem,D.deJongh,andG.Renardel

deLavalette.NNIL,aStudyinIntuitionisticPropositionalLogic.InA.Ponse,M.deRijke,andY.Venema,editors,ModalLogicandProcessAlgebra,aBisimulationPerspective,CSLILectureNotes,no.53,pages289–326.CenterfortheStudyofLanguageandInformation,Stanford,1995.[Yav97]

R.E.Yavorsky.Logicalschemesforﬁrstordertheories.InSpringerLNCS(Yaroslavl’97volume),volume1234,pages410–418,1997.

D.Zambella.Shavrukov’stheoremonthesubalgebrasofdiago-nalizablealgebrasfortheoriescontainingI∆0+EXP.TheNotreDameJournalofFormalLogic,35:147–157,1994.

[Zam94]

AAdjointsinPreorders

Theconsequencerelationsweconsiderarepreorders.Apreorderisanon-emtysetwthareﬂexivetransitiverelation.Itisaspecialkindofcategory,viz.acategorywhere,betweenanytwoobjects,wehaveatmostonearrow.Inthepresentpaper,wewillusesomefactsfromcategorytheoryandsomefactsspeciﬁcforpreorders.Wecollectmostofthesefactsinthefollowinglemma.Theeasyproofsarelefttothereader.

LemmaA.1Suppose≤isapreorderonCandthat󰀳isapreorderonD.Say,󰀑istheinducedequivalencerelationof≤and≡istheinducedequivalencerelationof󰀳.LetL:D→CbetheleftadjointfunctiontoR:C→D,thatisLd≤c⇔d󰀳Rc,foreveryd∈Dandeveryc∈C.Thenthefollowingholds.

1.LRc≤candd󰀳RLd.

2.LandRareorderpreserving,inotherwords,LandRaremophismsofpreorders,andthusfunctorsofthecorrespondingcategories.3.Rc≡RLRcandLd󰀑LRLd.

4.SupposethatRisasurjectiononobjects.Then,foranyd∈D,d≡RLd.5.SupposeRisasurjectiononobjects.LetXbetherangeofL.Let≤0

bethefullsub-preorderof≤obtainedbyrestricting≤toX.Then,≤0isequivalentto󰀳.Thismeansthat,forx∈X,x󰀑LRxand,ford∈D,d≡RLd.6.L◦Risuniquelydeterminedmodulo󰀑byX:=range(L).

7.Supposewehavesumsonthepreorders≤and󰀳,i.e.therearebinaryfunctions∨and+suchthat

•c1≤c󰀂andc2≤c󰀂iﬀ(c1ThenL(d+e)󰀑Ld∨Le.

∨

c2)≤c󰀂,

•d1󰀳d󰀂andd2󰀳d󰀂iﬀ(d1+d2)󰀳d󰀂.

Let£beasemi-consequencerelationonL(P).Both󰀯L(P),󰀬󰀰and󰀯L(P),£󰀰canbeconsideredaspreorders.A1tellsusthattheidenticalmapping󰀜:A→Aisanembeddingfrom󰀯L(P),󰀬󰀰to󰀯L(P),£󰀰.Inthispaperweareinterestedincaseswhere󰀜hasaleftadjointL.Ifsuchaleftadjointoftheembeddingfunctorexists,wecall󰀯L(P),󰀬󰀰areﬂectivesubcategoryof󰀯L(P),£󰀰.ThefunctorLiscalledthereﬂector.(See[Mac71]formoreonthesenotions.)Notethat󰀜isalsosurjectiveonobjects.

Suppose£isanearly-consequencerelation.B1tellsusthat∨isasumforthecategory£.Sinceleftadjointscommutewithsums,bylemmaA.1(7),wehave:󰀬L(A∨B)↔(LA∨LB)

BCharacterizationsandDependencies

ConsideranyconsistentREtheoryT,extendingHA,inthelanguageofHA.Weintroducesomenotions,closelyrelatedtoΣ-preservativityforT.Deﬁne,suppressingtheindexforT,thefollowingconsequencerelations:

ProvableDeductiveCons.UniformDeductiveCons.

StrongUniformDeductiveCons.UniformProvablyDeductiveCons.

A£pdcBA£udcBA£sudcBA£updcB:↔:↔:↔:↔P(PA→PB)

∀x∃y(PxA→PyB)∀x(PxA→PxB)∀x∃yP(PxA→PyB)

WeprovetheOrey-H´ajekcharacterizationforΣ-preservativityandUniformProvableDeductiveConsequence.

TheoremB.1(Orey-H´ajek)Tprovesthatthefollowingareequivalent:(i)A£ΣB,(ii)∀xP(PxA→B),(iii)A£updcB.

Proof

ReasoninT.“(i)→(ii)”SupposeA£ΣBandconsideranyx.Wehave,bytheorem8.1,P(PxA→A)and(PxA)∈Σ,henceP(PxA→B).

“(ii)→(iii)”FromP(PxA→B),wehavethat,forsomey,Py(PxA→B)andhencePPy(PxA→B).Ergo:P(PyPxA→PyB).Clearly,foranyu,P(PuA→PyPuA).WemayconcludeP(PxA→PyB).Hence,A£updcB.“(i)←(iii)”SupposeA£updcBandP(S→A).Itfollowsthat,forsomex,PPx(S→A).Moreover,P(S→PxS).SoP(S→PxA).Hence,forsomey,P(S→PyB).Ergo,byreﬂection,P(S→B).PTheoremB.2Wehave:T󰀬A£ΣB→A£udcB.

Proof

ReasoninT.SupposeA£ΣB.Consideranyx.WecanﬁndaysuchthatwehavePy(PxA→B).SupposePxA.Clearly,foranyu,PuA→PyPuA.ItfollowsthatPyB.PTheoremB.3(Orey-H´ajekforHA∗)Wehave:

HA∗󰀬A£HA∗,ΣB↔A£udc,HA∗B.

Proof

ImmediatebytheprincipleC,theoremB.1andtheoremB.2.TheoremB.4HA∗󰀬(PHA∗A→B)→A£HA∗,ΣB.

PProof

ReasoninHA∗.SupposePA→B.Itfollowsthat∀x(PxA→B).Hence,∀xP(PxA→B).Thuswemayconclude,A£ΣB.P51

CModalLogicforΣ-Preservativity

Considerthelanguageofmodalpropositionallogicwithaunarymodalopera-torPandabinaryoperator£.WedeﬁnearithmeticalinterpretationsinthelanguageofHAintheusualmanner,interpretingPasprovabilityinHAand£asΣ-preservativityoverHA.WestatetheprinciplesvalidinHAforthislogic,knownatpresent.WiththeexceptionofΣ4andΣ8theseprinciplesarethedualsoftheprinciplesoftheinterpretabilitylogicILM.Foradiscussionofthisduality,see[Vis98a].L1L2L3L4Σ1Σ2Σ3Σ4Σ5Σ6Σ7

󰀬A⇒󰀬PA

󰀬P(A→B)→(PA→PB)󰀬PA→PPA󰀬P(PA→A)→PA󰀬P(A→B)→A£B󰀬A£B

∧

B£C→A£C

󰀬C£A∧C£B→C£(A∧B)󰀬A£C

∧

B£C→(A∨B)£C

󰀬A£B→(PA→PB)󰀬A£PA

󰀬A£B→(PC→A)£(PC→B)

Σ8LetXbeaﬁnitesetofimplicationsandlet

Y:={C|(C→D)∈X}∪{B}.

󰀁

TakeA:=X.Then,󰀂󰀬(A→B)£{A}Y.Here(A→B)£{A}Yisshortfor(A→B)£{A}Yand{C}Disdeﬁnedasfollows:–{C}p:=(C→p),{C}⊥:=⊥,{C}󰀝:=󰀝,

–{C}PE:=PE,{C}(E£F)=(C→(E£F)),{C}(E→F):=(C→(E→F)),–{C}(·)commuteswith

∧

and∨.

TheveriﬁcationofL1-L4,Σ1-Σ3,Σ5−Σ7isroutine.ForΣ4see9.1andforΣ8see9.2.

FromourprinciplesLeivant’sprinciplecanbederived.(ThisisoneoftheStellingenof[Lei75].)Le

󰀬P(A∨B)→P(A∨PB)

Weleavethisasanexercisetothereader.Itisopenwhetherouraxiomsarearithmeticallycomplete.

因篇幅问题不能全部显示，请点此查看更多更全内容

查看全文

全部栏目

propositional logic and