Kreisel and Lawvere on Category Theory and the Fou

KreiselandLawvereonCategoryTheoryandtheFoundationsofMathematicsJean-PierreMarquisUniversitédeMontréalMontréalCanadaImpactofcategories•Whentheimpactofcategoriesonfoundationsisdiscussedwith«mainstream»logicians,weoftengettworesponses:1.Pragmaticscepticism:stillwaitingfornewsignificantresults;2.Philosophicallymotivatedobjections.Claims1.Kreiselhasarticulatedaviewaboutthefoundationsofmathematicsandcategorytheorythatprevailsamonglogicianseventoday;2.Althoughthisviewhadsomecredibilityandforcewhenitwasformulated,itoughttobereevaluated;3.Kreisel’sviewisbasedoncertainassumptionswhicharedubitableandoughttobecontrastedwithalternatives,inparticularwithLawvere’sviews.Kreisel’sclaims:thesources1.AppendixtoFeferman’spaperonthefoundationsofcategorytheoryin1969;2.«Observationsonpopulardiscussionsoffoundations»inAxiomaticSetTheory1971;3.AreviewofMacLane’s«Categoricalalgebraandset-theoreticfoundations»inAxiomaticSetTheory1971;4.AppendixtoElementsofMathematicalLogicwithKrivine1967.Thesocio-historicalcontext1.«Mainstream»developmentsandresearchprogramsinthefoundationsofmathematicsinthe1960’s;2.Categorytheoryinthe1960’s.1963:Berkeley•Meetingonmodeltheory:–Itisthewho’swhooflogicandthefoundationsofmathematics.1963•Wecanbecategorytheorists:–LectureoncategoricalalgebraattheAMS;–Grothendieck’sSGA4;–Freyd’spresentationofhisAFT;–Lawvere’sthesis;–Ehresmann’s«catégoriesstructurées»;–Firstcoherencetheorem;–Adjointfunctorsandlimits1963:Lawvere’sthesis•Algebraiccategoriesandalgebraicfunctors;•Thecategoryofcategoriesasafoundationformathematics;•Setswithincategories;•Centralroletoadjointfunctors.1964•ETCS:weshoulddevelopsettheorywithincategorytheory;•Itcanbedone:hereishow.1964•AsItoldyou,youcan’tdothatBill!Membershipisprimitiveinsettheory;•ButIwillletyoupublishitanyway…1966•Now,Iwilltelleveryone,thecategoryofcategoriesshouldbethefoundationsofmathematics;•Hereisanaxiomatizationofit…Lawvere’sviews1.«Inthemathematicaldevelopmentofrecentdecadesoneseesclearlytheriseoftheconvictionthattherelevantpropertiesofmathematicalobjectsarethosewhichcanbestatedintermsoftheirabstractstructureratherthanintermsoftheelementswhichtheobjectswerethoughttobemadeof.Thequestionthusnaturallyariseswhetheronecangiveafoundationformathematicswhichexpresseswholeheartedlythisconvictionconcerningwhatmathematicsisabout,andinparticularinwhichclassesandmembershipinclassesdonotplayanyrole.Hereby“foundation”wemeanasinglesystemoffirst-orderaxiomsinwhichallusualmathematicalobjectscanbedefinedandalltheirusualpropertiesproved.»(Lawvere,1966,1)Thesocio-historicalcontext•Summingup:1.Thereareexcitingdevelopmentsandmuchtodoin«mainstream»foundationalresearch;itisanactive«researchprogram»;2.Thereareset-theoreticalwaystohandlecategorytheory.Thesocio-historicalcontext•Summingup:1.Categorytheoryisarisingasanautonomousmathematicaldiscipline;2.Itisnotglobal;3.Itsfoundationalroleisstillproblematicandpresentedinaclassicaltarskianmanner(first-ordertheory).1968-1969•Thefoundationsofcategorytheoryraisesdifficultiesforsettheory;•Herearesomewaysofhandlingthem(oneuniverse,commonfoundations).KreiseljumpsinThiscan’tberight!Thewholeissueisbasedonaconfusionandafailuretounderstandthetruepurposeofthefoundationalenterprise.Kreisel’sclaims1.Kreiseldistinguishesfoundationsandorganizationofmathematics.a)Thedistinctionisuseful«foranalyzingthenatureoftheproblemspresentedby(existing)categorytheory,and,moregenerally,foranalyzingtheroleoffoundationsforworkingmathematicians.»(Kreisel,1971,189)b)Foundationshavetodowithvalidity,justification;c)Organizationhastodowithefficiency.Kreisel’sclaims1.«Forfoundationsitisimportanttoknowwhatwearetalkingabout;wemakethesubjectasspecificaspossible.Inthiswaywehaveachancetomakestrongassertions.Forpractice,tomakeaproofintelligible,wewanttoeliminateallpropertieswhicharenotrelevanttotheresultproved,inotherwords,wemakethesubjectmatterlessspecific.»Kreisel’sclaims1.«Foundationsprovideananalysisofpractice.Todeservethisname,foundationsmustbeexpectedtointroducenotionswhichdonotoccurinpractice.Thusinfoundationsofsettheory,typesofsetsaretreatedexplicitlywhileinpracticetheyaregenerallyabsent;andinfoundationsofconstructivemathematics,theanalysisofthelogicaloperationsinvolves(intuitive)proofswhileinpracticethereisnoexplicitmentionofthelatter.»(Kreisel,1971,192)Kreisel’sclaims2.«Foundationsandorganizationaresimilarinthatbothprovidesomesortofmoresystematicexposition.Butastepinthisdirectionmaybecrucialfororganization,yetfoundationallytrivial,forinstanceanewchoiceoflanguagewhen(i)oldtheoremsaresimplertostatebut(ii)theprimitivenotionsofthenewlanguagearedefinedintermsoftheold,thatisiftheyarelogicallydependentonthelatter.Quiteoften,(i)willbeachievedbyusingnewnotionswithmore‘structure’,thatislessanalyzednotions,whichisastepintheoppositedirectiontoafoundationalanalysis.Inshort,foundationalandorganizationalaimsareliabletobeactuallycontradictory.»(Kreisel,1971,192)Kreisel’sclaims3.«Organizationandfoundationsareincomparable.Organizationinvolvesaproperchoiceoflanguage;wehavealreadyseenthatthisisnotnecessarilypro