REVERSE MATHEMATICS ■■■■■ REVERSE MATHEMATICS proofs from the inside out ■■■■■ John Stillwell princeton universit y press princeton and oxford Copyright©byJohnStillwell RequestsforpermissiontoreproducematerialfromthisworkshouldbesenttoPermissions, PrincetonUniversityPress PublishedbyPrincetonUniversityPress,WilliamStreet,Princeton,NewJersey IntheUnitedKingdom:PrincetonUniversityPress,OxfordStreet,Woodstock,Oxfordshire OXTR press.princeton.edu JacketimagescourtestyofShutterstock AllRightsReserved LibraryofCongressCataloging-in-PublicationData Names:Stillwell,John,author. Title:Reversemathematics:proofsfromtheinsideout/JohnStillwell. Description:Princeton:PrincetonUniversityPress,[]|Includes bibliographicalreferencesandindex. Identifiers:LCCN|ISBN(hardback) Subjects:LCSH:Reversemathematics.|BISAC:MATHEMATICS/History& Philosophy.|MATHEMATICS/General.|MATHEMATICS/Logic.|SCIENCE/History. Classification:LCCQA..S|DDC.–dcLCrecordavailableat https://lccn.loc.gov/ BritishLibraryCataloging-in-PublicationDataisavailable ThisbookhasbeencomposedinMinionPro Printedonacid-freepaper.“ PrintedintheUnitedStatesofAmerica           To Elaine ■■■■■ Contents ■■■■■ Preface xi  HistoricalIntroduction  . EuclidandtheParallelAxiom  . SphericalandNon-EuclideanGeometry  . VectorGeometry  . Hilbert’sAxioms  . Well-orderingandtheAxiomofChoice  . LogicandComputability   ClassicalArithmetization  . FromNaturaltoRationalNumbers  . FromRationalstoReals  . CompletenessPropertiesofR  . FunctionsandSets  . ContinuousFunctions  . ThePeanoAxioms  . TheLanguageofPA  . ArithmeticallyDefinableSets  . LimitsofArithmetization   ClassicalAnalysis  . Limits  . AlgebraicPropertiesofLimits  . ContinuityandIntermediateValues  . TheBolzano-WeierstrassTheorem  . TheHeine-BorelTheorem  . TheExtremeValueTheorem  . UniformContinuity  . TheCantorSet  . TreesinAnalysis   Computability  . ComputabilityandChurch’sThesis  viii ■ CONTENTS . TheHaltingProblem  . ComputablyEnumerableSets  . ComputableSequencesinAnalysis  . ComputableTreewithNoComputablePath  . ComputabilityandIncompleteness  . ComputabilityandAnalysis   ArithmetizationofComputation  . FormalSystems  . Smullyan’sElementaryFormalSystems  . NotationsforPositiveIntegers  . Turing’sAnalysisofComputation  . OperationsonEFS-GeneratedSets  . GeneratingΣSets   . EFSforΣRelations   . ArithmetizingElementaryFormalSystems  . ArithmetizingComputableEnumeration  . ArithmetizingComputableAnalysis   ArithmeticalComprehension  . TheAxiomSystemACA  . ΣandArithmeticalComprehension   . CompletenessPropertiesinACA  . ArithmetizationofTrees  . TheKőnigInfinityLemma  . RamseyTheory  . SomeResultsfromLogic  . PeanoArithmeticinACA   RecursiveComprehension  . TheAxiomSystemRCA  . RealNumbersandContinuousFunctions  . TheIntermediateValueTheorem  . TheCantorSetRevisited  . FromHeine-BoreltoWeakKőnigLemma  . FromWeakKőnigLemmatoHeine-Borel  . UniformContinuity  . FromWeakKőnigtoExtremeValue  . TheoremsofWKL  . WKL,ACA,andBeyond   ABiggerPicture  . ConstructiveMathematics  . PredicateLogic  . VarietiesofIncompleteness  CONTENTS ■ ix . Computability  . SetTheory  . Conceptsof“Depth”  Bibliography  Index 