Nelson’s Work on Logic and Foundations and Other R

Nelson’sWorkonLogicandFoundationsandOtherReflectionsonFoundationsofMathematicsSamuelR.Buss∗DepartmentofMathematicsUniversityofCalifornia,SanDiegoLaJolla,[e-mail]8,2006AbstractThispaperstartsbydiscussingNelson’sphilosophyofmathematics,whichisablendofmathematicalformalismandaradicalconstructivism.Assuch,itmakesstrongassertionsaboutthefoundationsofmathematicandtherealityofmathematicalobjects.Wethenofferourownsugges-tionsforthedefinitionofmathematicsandthenatureofmathematicalreality.Wesuggestasecondcharacterizationofmathematicalreasoningintermsofcommonsensereasoningandargueitsrelevanceformathematicseducation.Nelson’sphilosophyisthefoundationofhisdefinitionofpredicativearithmetic.Therearecloseconnectionsbetweenpredicativearithmeticandthecommontheoriesofboundedarithmetic.Weprovethatpoly-nomialspace(PSPACE)predicatesandexponentialtime(EXPTIME)predicatesarepredicative.WediscussNelson’sformalistphilosophiesandhisunpublishedworkinautomatictheoremchecking.ThispaperwasbegunwiththeplanofdiscussingNelson’sworkinlogicandfoundationsandhisphilosophyonmathematics.Inparticular,itisbasedonourtalkattheNelsonmeetinginVancouverinJune2004.ThemaintopicsofthistalkwereNelson’spredicativearithmeticandhisunpublishedworkonautomatictheoremproving.However,itprovedimpossibletostaywithinthisplan.Inwritingthepaper,wewerepromptedtothinkcarefullyaboutthenatureofmathematicsandmorefullyformulateourownphilosophyofmathematics.Wepresentthisbelow,alongwithsomediscussionaboutmathematicseducation.MuchofthepaperfocusesonNelson’sphilosophyofmathematics,onhowhisphilosophymotivateshisdevelopmentofpredicativearithmetic,andonhisunpublishedworkoncomputerassistedtheoremproving.Wealsodiscussthe∗SupportedinpartbyNSFgrantsDMS-0400848.1natureofmathematicalrealityandNelson’sviewsandourownviewsonthenatureofmathematics.Predicativearithmeticand,moregenerally,Nelson’sphilosophyofmathematics,arecloselyrelatedtoNelson’sdevelopmentofin-ternalsettheoryandnonstandardanalysis,butthisconnectionisnotpursuedinthepresentpaper;forthis,thereadermayconsultG.Lawler’spaperinthisvolume.Themainbodyofthepaperiswrittentobeaccessibletoamathemati-cianwithlittleknowledgeoflogic.Thepaperbeginswithaquickoverviewofthreeofthemainphilosophiesofmathematics:formalism,platonism,construc-tivism.WethenpresentthebasicideasbehindNelson’spredicativearithmetic,aframeworkthathehasputforwardasbeingthecorrectgeneralsettingformathematicalreasoning.Thenextsection,Section4,discussesourownviewsofmathematics.Wegiveonedefinitionofmathematics,andthenasecondcharacterizationofmathematicsanddiscusssomeimplicationsformathemat-icseducation.Afterthat,wereturntoNelson’sworkonautomatictheoremproving,andthenthemainbodyofthepaperconcludeswithsomequotesfromNelson’swritings.Twoappendicesincludeextramaterial.Thefirstappendixgivesanew,weakerbasetheoryQ−forpredicativearithmetic.Thesecondappendixprovesthatexponentialtimecomputabilityispredicative.1Platonism,constructivismandformalismInourtalk[1],wedescribedNelson’sphilosophyofmathematicsasbeing“radi-calconstructivism.”Afterward,Nelsonsuggestedthathethinksofhimselfasa“formalist”ratherthana“radicalconstructivist.”Infact,bothoftheselabelsapplyverywelltoNelson’sphilosophy;heisnotmerelyaformalist,healsogivesbothpredicativearithmeticandnon-standardanalysisveryconstructivefoundations.Thereaderiswarned,however,thatwewillbeexpressingourpersonalopinionsofNelson’sphilosophy,andNelsonmightnotalwaysagreewithwhatwesay.Inparticular,incomparisonwiththepresentpaper,Nelsonwouldprobablystressformalismmoreandconstructivismless.The“platonist”philosophyofmathematicstakestheviewthattheusualobjectsofmathematicstudy,suchastheintegers,therealnumbers,functionsontherealnumbers,etc.—evenabstractsets—havesomekindofinde-pendentexistence.Thenatureofthisexistenceistypicallyleftvague,andtheplatonistphilosophyusuallypositsthatthesemathematicalobjectsexistonlyinsomeabstractornon-physicalsense.Nonetheless,thehallmarkoftheplatonistphilosophyisthathumanmathematicianshavedirectintuitionaboutordirectperceptionofmathematicalobjects.Theplatonistphilosophyholdsthatourmathematicaltheoremsandconstructionsare“about”somethingreal.Mostmathematiciansareplatonists,buttherearecompetingschoolsofthought.Theseincludethe“intuitionists,”the“constructivists,”andthe“for-malists.”1ConstructivismwasadvocatedbyD.Hilbertasameanstoestablish1Wewillnotdiscussintuitionismatallinthispaper.2theconsistencyofformalizationsoftheoriesabouttherealnumbersandsetthe-ory.Theconstructivistphilosophytakesthepointofviewthatfiniteobjects,notablytheintegers,existinsomeplatonicsenseandthatfinitarycombinato-rialoperationsontheintegershaveawell-definedsemantics.Aconstructivistwouldgenerallyrejecttheexistenceofinfinitesets,oratleasttheexistenceofa“completedinfinity”,butwouldacceptthemeaningfulnessoftheconceptofanarbitraryinteger.Theusualconventionisthatprimitiverecursiveoperationsaretheconstructiveoperations.Formalismistheviewpointthatmathematicsismerelya‘game’thatactsonsymbolsaccordingtoafixedsetofrules.Foraformalist,theactivityofamathematiciancon