Twin Paradox and the logical foundation of relativ

arXiv:gr-qc/0504118v325Aug2005TWINPARADOXANDTHELOGICALFOUNDATIONOFRELATIVITYTHEORYJUDITX.MADAR´ASZ,ISTV´ANN´EMETI,ANDGERGELYSZ´EKELYAbstract.Westudythefoundationofspace-timetheoryintheframeworkoffirst-orderlogic(FOL).Sincethefoundationofmathematicshasbeensuccessfullycarriedthrough(viasettheory)inFOL,itisnotentirelyimpossibletodothesameforspace-timetheory(orrelativity).FirstwerecallasimpleandstreamlinedFOL-axiomatizationSpecrelofspecialrelativityfromtheliterature.Specreliscompletewithrespecttoquestionsaboutinertialmotion.Thenweaskourselveswhetherwecanprovetheusualrelativisticpropertiesofacceleratedmotion(e.g.,clocksinacceleration)inSpecrel.Asitturnsout,thisispracticallyequivalenttoaskingwhetherSpecrelisstrongenoughto“handle”(ortreat)acceleratedobservers.Weshowthatthereisamathematicalprinciplecalledinduction(IND)comingfromrealanalysiswhichneedstobeaddedtoSpecrelinordertohandlesituationsinvolvingrelativisticacceleration.WepresentanextendedversionAccRelofSpecrelwhichisstrongenoughtohandleacceleratedmotion,inparticular,acceleratedobservers.Amongothers,weshowthattheTwinParadoxbecomesprovableinAccRel,butitisnotprovablewithoutIND.Keywords:twinparadox,relativitytheory,acceleratedobservers,first-orderlogic,axiom-atization,foundationofrelativitytheory1.INTRODUCTIONTheideaofelaboratingthefoundationofspace-time(orfoundationofrelativity)inaspiritanalogouswiththerathersuccessfulfoundationofmathematics(FOM)wasinitiatedbyseveralauthorsincluding,e.g.,DavidHilbert[12]orleadingcontemporarylogicianHarveyFriedman[9,10].Foundationofmathematicshasbeencarriedthroughstrictlywithintheframeworkoffirst-orderlogic(FOL),forcertainreasons.Thesamereasonsmotivatetheeffortofkeepingthefoundationofspace-timealsoinsideFOL.OneofthereasonsisthatstayinginsideFOLhelpsustoavoidtacitassumptions,anotherreasonisthatFOLhasacompleteinferencesystemwhilehigher-orderlogiccannothaveonebyG¨odel’sincompletenesstheorem,seee.g.,V¨a¨an¨anen[24,p.505]or[2,Appendix].FormoremotivationforstayinginsideFOL(asopposedtohigher-orderlogic),cf.e.g.,Ax[3],Pambuccian[17],[2,Appendix1:“WhyexactlyFOL”],[1],butthereasonsinV¨a¨an¨anen[24],Ferreir´os[8],orWole´nski[26]alsoapply.Followingtheabovemotivation,webeginatthebeginning,namelyfirstwerecallastreamlinedFOLaxiomatizationSpecrelofspecialrelativitytheory,fromtheliterature.Specreliscompletewithrespectto(w.r.t.)questionsaboutinertialmotion.Thenweaskourselveswhetherwecanprovetheusualrelativisticpropertiesofacceleratedmotion(e.g.,clocksinacceleration)inSpecrel.Asitturnsout,thisispracticallyequivalenttoaskingwhetherSpecrelisstrongenoughto“handle”(ortreat)acceleratedobservers.Weshowthatthereisamathematicalprinciplecalledinduction(IND)comingfromrealanalysiswhichneedstobeaddedtoSpecrelinordertohandlesituationsinvolvingrelativisticacceleration.WepresentanextendedversionAccRelofSpecrelwhichisstrongenoughtohandleacceleratedclocks,inparticular,acceleratedobservers.Alfr´edR´enyiInstituteofMathematicsoftheHungarianAcademyofSciences,POB127H-1364Bu-dapest,Hungary.E-mailaddresses:[e-mail],[e-mail],[e-mail].1TWINPARADOXANDTHELOGICALFOUNDATIONOFRELATIVITYTHEORY2Weshowthattheso-calledTwinParadoxbecomesprovableinAccRel.ItalsobecomespossibletointroduceEinstein’sequivalenceprinciplefortreatinggravityasaccelerationandprovingthegravitationaltimedilation,i.e.thatgravity“causestimetorunslow”.WhatwearedoinghereisnotunrelatedtoField’s“Sciencewithoutnumbers”pro-grammeandto“reversemathematics”inthesenseofHarveyFriedmanandStevenSimp-son.Namely,wesystematicallyaskourselveswhichmathematicalprinciplesorassumptions(like,e.g.,IND)arereallyneededforprovingcertainobservationalpredictionsofrelativity.(Itwasthisstrivingforparsimonyinaxiomsorassumptionswhichwealludedtowhenwementioned,wayabove,thatSpecrelwas“streamlined”.)Theinterplaybetweenlogicandrelativitytheorygoesbacktoaround1920andhasbeenplayinganon-negligibleroleinworksofresearcherslikeReichenbach,Carnap,Suppes,Ax,Szekeres,Malament,Walker,andofmanyothercontemporaries.1InSection2werecalltheFOLaxiomatizationSpecrelcompletew.r.t.questionsconcern-inginertialmotion.TherewealsointroduceanextensionAccRelofSpecrel(stillinsideFOL)capableforhandlingacceleratedclocksandalsoacceleratedobservers.InSection3weformalizetheTwinParadoxinthelanguageofFOL.WeformulateTheorems3.1,3.2statingthattheTwinParadoxisprovablefromAccRelandthesameforrelatedquestionsforacceleratedclocks.Theorems3.5,3.7statethatSpecrelisnotsufficientforthis,moreconcretelythattheinductionaxiomINDinAccRelisneeded.InSections4,5weprovethesetheorems.MotivationfortheresearchdirectionreportedhereisnicelysummarizedinAx[3],Sup-pes[20];cf.alsotheintroductionof[2].HarveyFriedman’s[9,10]presentarathercon-vincinggeneralperspective(andmotivation)forthekindofworkreportedhere.2.AXIOMATIZINGSPECIALRELATIVITYINFOLInthispaperwedealwiththekinematicsofrelativityonly,i.e.wedealwithmotionofbodies(ortest-particles).Themotivationforourchoiceofvocabulary(forspecialrelativity)issummarizedasfollows.Wewillrepresentmotionaschangingspatiallocationintime.Todoso,wewillhavereference