What is a Theory

WhatisaTheory?GillesDowekINRIA-Roquenourt,BP105,78153LeChesnayCedex,Frane.Gilles.Dowekinria.fr~dowekAbstrat.Dedutionmoduloisawaytoexpressatheoryusingompu-tationrulesinsteadofaxioms.Wepresentinthispaperanextensionofdedutionmodulo,alledPolarizeddedutionmodulo,wheresomerulesanonlybeusedatpositiveourrenes,whileothersanonlybeusedatnegativeones.Weshowthatalltheoriesinpropositionalalulusanbeexpressedinthisframeworkandthatutsanalwaysbeeliminatedwithsuhtheories.Mathematialproofsarealmostneverbuiltinpurelogi,butbesidesthededutionrulesandthelogialaxiomsthatexpressthemeaningoftheonnetorsandquantiers,theyusesomethingelse-atheory-thatexpressesthemeaningoftheothersymbolsofthelanguage.Examplesoftheoriesareequationaltheories,arithmeti,typetheory,settheory,...Theusualdenitionofatheory,asasetofaxioms,issuÆientwhenoneisinterestedintheprovabilityrelation,but,aswell-known,itisnotwhenoneisinterestedinthestrutureofproofsandinthetheoremprovingproess.Forinstane,weandeneatheorywiththeaxiomsa=bandb=(wherea,bandareindividualsymbols)andprovethepropositiona=.However,wemayalsodenethistheorybytheomputationrulesa!band!bandthenapropositiont=uisprovableiftanduhavethesamenormalformusingtheseomputationrules.Theadvantagesofthispresentationarenumerous.{Weknowthatallthesymbolsourringinaproofoft=umustourintorinuoroneoftheirreduts.Forinstane,thesymboldneednotbeusedinaproofofa=.Wegetthiswayanalytiityresults.{Inautomatedtheoremproving,weanusethiskindofresultstoreduethesearhspae.Infat,inthisase,wejustneedtoreduedeterministiallythetermsandhektheidentityoftheirnormalforms.Wegetthiswaydeisionsalgorithms.{Sinethenormalformofthepropositiona=disb=dandbanddaredistint,thepropositiona=disnotprovableinthistheory.Wegetthiswayindependeneresultsand,inpartiular,onsistenyresults.{Inaninterativetheoremprover,weanreduethepropositiontobeproved,beforewedisplayittotheuser.Thisway,theuserisrelievedfromdoingtrivialomputations.Todeneatheorywithomputationrules,notanysetofrulesisonvenient.Forinstane,ifinsteadoftakingtherulesa!b,!bwetaketherulesb!a,b!,welosethepropertythatapropositiont=uisprovableiftanduhaveaommonredut.Tobeonvenient,arewritesystemmustbeonuent.Conuene,andsometimesalsotermination,areneessarytohaveanalytiityresults,ompletenessofproofsearhmethods,independeneresults,...Whenwehaverulesrewritingpropositionsdiretly,forinstanexy=0!x=0_y=0onueneisnotsuÆientanymoretohavetheseresults,bututeliminationisalsorequired[7,4℄.Conueneanduteliminationarerelated.Forinstane,withthenononuentsystemb!a,b!,weanprovethepropositiona=introduingautonthepropositionb=b,but,beausetherewritesystemisnotonuent,thisutannotbeeliminated.Conueneanthusbeseenasaspeialaseofuteliminationwhenonlytermsarerewritten[6℄,butinthegeneralase,onueneisnotasuÆientonditionforutelimination.Computationrulesarenottheonlyalternativetoaxioms.Anotheroneistoaddnonlogialdedutionrulestoprediatelogieithertakinganintrodutionandeliminationrulefortheabstrationsymbolinvariousformulationsofsettheory[15,2,10,1,3,9℄orinterpretinglogiprogramsordenitionsasdedutionrules[11,16,17,13℄orinamoregeneralsetting[14℄.Nonlogialdedutionrulesandomputationruleshavesomesimilarities,butwebelievethatomputationruleshavesomeadvantages.Forinstane,nonlogialdedutionrulesmayblurthenotionofutinnaturaldedutionandextraproofredutionruleshavetobeadded(see,forinstane,[5℄).Alsowithsomenonlogialdedutionrules,theontradition?mayhaveautfreeproofandthusonsistenyisnotalwaysaonsequeneofutelimination.Inontrast,thenotionofut,theproofre-dutionrulesandthepropertiesofutfreeproofsremaintheusualoneswithomputationrules.Whenatheoryisgivenbyasetofaxioms,wesometimeswanttondanalternativewaytopresentitwithomputationrules,insuhawaythatuteliminationholds.Fromutelimination,weandedueanalytiityresults,on-sistenyandvariousindependeneresults,ompletenessofproofsearhmethodsandinsomeasesdeisionalgorithms.Manytheorieshavebeenpresentedinsuhaway,inludingvariousequationaltheories,severalpresentationsofsimpletypetheory(withombinatorsorlambda-alulus,withorwithouttheaxiomofin-nity,...),thetheoryofequality,arithmeti,...However,asystematiwayoftransformingasetofaxiomsintoasetofrewriterulesisstilltobefound.AstepinthisdiretionisKnuth-Bendixmethod[12℄anditsextensions,thatpermittotransformsomeequationaltheoriesintorewritesystemswiththeutelimina-tionproperty(i.e.withtheonueneproperty).AnotherstepinthisdiretionistheresultofS.NegriandJ.VonPlato[14℄thatgivesawaytotransformsomesetsofaxioms,inpartiularallquantierfreetheories,intoasetofnonlogialdedutionrulesinsequentalulus,preservingutelimination.Inthispaper,weproposeawaytotransformanyonsistentquantierfreetheoryintoasetofomputationruleswiththeuteliminationproperty.OurrstattemptwastouseDedutionmodulo[7,8℄orAsymmetridedu-tionModulo[6℄asageneralframeworkwhereomputationanddedutionanbemixed.InDedutionmodulo,theintrodutionruleofonjuntionABA^BistransformedintoaruleABifCA^BCwhereistheongruenegeneratedbytheomputationrules,andtheoth-erdedutionrulesaretransformedinasimilarway.InAsymmetridedutionmodulo,thisruleisrephrase