First order logic with domain conditions. Availabl

FirstorderlogiwithdomainonditionsFreekWiedijkandJanZwanenburgUniversityofNijmegenAbstrat.Theorretnessofproofsisinreasinglybeingveriedwithomputerprogramsalled‘proofhekers’.Examplesofsuhproofhek-ersareMizar,ACL2,PVS,Nuprl,HOL,IsabelleandCoq.Thispaperaddresseswhatisoneofthemostimportantproblemsforthatkindofsystem,whihishowtodealwithpartialfuntionsandtherelatedis-sueofhowtotreatundenedterms.Inmanysystemstheproblemisavoidedbyartiiallymakingallfuntionstotal.Howeverthatdoesnotorrespondtothepratieofeverydaymathematis.Intypetheorypartialfuntionsaremodeledbygivingfuntionsextraargumentswhihareproofobjets.Beauseofthatitisnotpossibletoapplyafuntionoutsideitsdomain.Howeverhavingproofsasrstlassobjetsmakestheloginon-standard.Thishasthedisadvantagesthatitisunfamiliartomostmathematiiansandthatmanyprooftoolswon’tbeusableforit.ForinstaneatheoremproverlikeOtterannotbeeasilyusedforthiskindoflogi.Alsoexpressionsintypetheoretialsystemsgetlumsybeausetheyontainproofobjets.ThePVSsystemsolvestheproblemofpartialfuntionsdierently.PVSgeneratestype-orretnessonditionsorTCCsforstatementsinitslan-guage.Theseareproofobligationsthathavetobesatised‘ontheside’toshowthatthestatementsarewell-formed.InthispaperwerelatethetypetheoretialapproahtooneresemblingthePVSapproah.Weadddomainonditionstoordinaryrstorderlogi(whihinthispaperwillbelassialandone-sorted)andweshowthattheombinationorrespondspreiselytoarstordersystemthattreatspartialfuntionsinthestyleoftypetheory.1Introdution1.1ProblemUntilafewdeadesagomathematiswassomethingthatwasdoneinhumanheads,ontheblakboardoronpaper.Onlysinetheseventieshavesystemsbeendevelopedthatverifymathematiswiththeomputer.TherstofthesewastheAutomathsystem[13℄fromtheNetherlands.OtherearlysystemsofthiskindweretheMizarsystem[12,20℄fromPolandandtheLCFsystem[6℄fromtheUK.Reentlythiskindofsystemhasbeomewidelyused(mostlybeauseofappliationsinomputersiene).CurrentlythemostpopularisthePVSsystem[14℄fromaUSompanyalledSRIInternational.OtherontemporarysystemsofthiskindareACL2[9℄andNuprl[3℄fromtheUS,HOL[5,8℄andIsabelle[15,2FreekWiedijkandJanZwanenburg16℄fromtheUKandGermany,andtheCoqsystem[1℄fromFrane.Thislastsystemisanimplementationofanapproahtoformalizingmathematisalledtypetheory.Thedevelopmentofformalmathematishashangedtheroleoflogialsys-tems.Theynolongerjustexisttobestudied,theynowreallyhavetobeused.Thereforetheyhavetosatisfydierentrequirementsthanbefore.Anexampleishowdenitionsaretreated.Traditionallydenitionswereseenassomethingextra-logialthatoneouldimagineashavingbeenexpanded.Howeverthiskindofexpansionmakesformulasimpossiblybig,whihisnotpratial.Sotodaydef-initionshavetobetakenseriouslyandarestudiedfortheirownsake.Thetopiofthispaperishowpartialfuntionsmightbetreatedinformalmathematis.Theprototypialexampleofapartialfuntionisdivision.Thequotient:1=0isproblematibeause0isoutsidethedomainofthedivisionfuntion.Onewayoftreatingpartialfuntionsisbyeliminatingthembytranslationtorelations.Sooneinterpretsastatementaboutdivisiontobereallyaboutaternaryprediatediveqthatsatisestheequivalene:diveq(x;y;z)()x=y=zHoweverwhentranslatingstatementsthiswaytheybeomeanorderofmagni-tudelargerthantheoriginal,whihisnotpratial.Fortheorythe‘solution’ofmodelingpartialfuntionswithrelationsisaeptable.HoweverinpratieitisineÆientandthereforenotattrative.In[7℄JohnHarrisonenumeratedthefourmainapproahestopartialfun-tionsthatoneatuallyenountersinproofhekers:1.Resolutelygiveeahpartialfuntionaonvenientvalueonpointsoutsideitsdomain.2.Giveeahpartialfuntionsomearbitraryvalueoutsideitsdomain.3.Enodethedomainofthepartialfuntioninitstypeandmakeitsappliationtoargumentsoutsidethatdomainatypeerror.4.Haveatruelogiofpartialterms.Intherstaseonewoulddene1=0=0,intheseondase1=0wouldbesomerealnumberbutonewouldnotbeabletoprovewhihoneitis,inthethirdase1=0wouldbeatypeerror,andinthelastase1=0wouldbeanallowedexpressionbutitwouldnotdenoteanything.InthispaperweexploreavariantHarrison’sapproahnumber3.Althoughwedopresentasystemofourownitisnota‘logiofpartialterms’.Itdoesnotallowonetowrite1=0oranyotherundenedtermandthereisnowaytostatewhetheratermisdened(beauseitalwaysis).Althoughtheapproahthatwepresenthereisbasedontypetheory,ourlogiatuallyisone-sorted.Sothevariablesofourlogiallhavethesame‘type’.Itiseasytogeneralizeourapproahtoamany-sortedlogi.Werestritedourselvestotheone-sortedaseforsimpliity.Firstorderlogiwithdomainonditions3Nowtheproblemthatwewanttoaddressinthispaperishowtorelateapproahnumber3torstorderlogi(theordinaryrstorderlogiwithtotalfuntions).Therearetworeasonswhyitisvaluablenottohavetogiveuprstorderlogi:{Firstorderlogiisthebestknownlogi.Usersofaproofhekerwillunder-standthesystembetterifthelogiisrstorderlogi.{Thereismuhtehnologyforrstorderlogi.Forinstanetherearemanytheoremproversforit.ThebestknownoftheseisOtter[11℄buttherearemanymore.Theyevenompeteinrstordertheoremproverompetitions.Itisvaluabletobeabletousethistehnologyinaproofheker.1.2ApproahWewillintroduethreelogialsystems,alledsystemT,systemDandsystemP.Thenamesofthosesystemsareabbreviationsof‘total’,‘domain’and‘partial’.T