ZFC in nLab

Axioms nLab ZFC SkiptheNavigationLinks| HomePage| AllPages| LatestRevisions| Discussthispage| Contents Context Foundations foundations Thebasisofitall mathematicallogic first-orderlogic typetheory,homotopytypetheory settheory materialsettheory ZFC ZFA structuralsettheory ETCS SEAR universe Foundationalaxioms foundationalaxiom basicconstructions: axiomofcartesianproducts axiomofdisjointunions axiomoftheemptyset axiomoffullness axiomoffunctionsets axiomofpowersets axiomofquotientsets materialaxioms: axiomofextensionality axiomoffoundation axiomofanti-foundation Mostowski'saxiom axiomofpairing axiomoftransitiveclosure axiomofunion structuralaxioms: axiomofmaterialization axiomsofchoice: axiomofchoice axiomofcountablechoice axiomofdependentchoice axiomofexcludedmiddle axiomofexistence axiomofmultiplechoice Markov'saxiom presentationaxiom smallcardinalityselectionaxiom axiomofsmallviolationsofchoice axiomofweaklyinitialsetsofcovers Whitehead'sprinciple largecardinalaxioms: axiomofinfinity axiomofuniverses regularextensionaxiom inaccessiblecardinal measurablecardinal elementaryembedding supercompactcardinal Vopěnka'sprinciple strongaxioms axiomofseparation axiomofreplacement further reflectionprinciple Removingaxioms constructivemathematics predicativemathematics Editthissidebar Contents Idea History Axioms Variations Constructiveversions Classtheories Largecardinals Miscellaneousvariations Relationtostructuralsettheories Relatedentries References Idea ThemostcommonlyacceptedstandardfoundationofmathematicstodayisamaterialsettheorycommonlyknownasZermelo–FraenkelsettheorywiththeaxiomofchoiceorZFCZFCforshort.Therearemanyvariationsonthattheory(includingconstructiveandclass-basedversions,whicharealsodiscussedhere). AccompanyingZFC,especiallytakingintoaccounttheaxiomoffoundation,isapicture(or‘ontology’)ofmaterialsetsformingacumulativehierarchyorganizedbyanordinal-valuedrankfunction.Thispicture(sometimesreferredtoasthe‘iterativeconception’)considerssetsasgeneratedbystartingatbottomwiththeemptysetandbuildingtohigherranksbyapplyingapowersetoperationtogettoanextsuccessorordinalrank,andtakingunionstogettolimitordinalranks.Thisiterativeconceptionfindsalternativeexpressioninalgebraicsettheory. History ThefirstversionwasdevelopedbyErnstZermeloin1908;in1922,AbrahamFraenkelandThoralfSkolemindependentlyproposedaprecisefirst-orderversionwiththeaxiomofreplacement;vonNeumannaddedtheaxiomoffoundationin1925.Alloftheseversionsincludedtheaxiomofchoice,butthiswasconsideredcontroversialforsometime;onehasmerelyZFZFifitistakenout. ZFCZFCissimilartotheclasstheoriesNBG(duetoJohnvonNeumann,PaulBernays,andKurtGödel)andMK(duetoAnthonyMorseandJohnKelley).Theformerisaconservative,finitelyaxiomatisableextensionofZFCZFC,whilethelatterisstrongerandcannotbefinitelyaxiomatised(althoughaconservativeextensioninvolvingmeta-classescouldbe). Contemporarysettheoristsoftenacceptadditionallargecardinalaxioms,whichcangreatlyincreasethestrengthofZFCZFC,farbeyondevenMKMK.Otheradditionalaxiomswhicharesometimesaddedaretheaxiomofdeterminacy(orvariousweakerversionsofit)ortheaxiomofconstructibility.TherearealsoweakervariantsofZFCZFC,especiallyforconstructiveandpredicativemathematics.Thentherearealternativesonadifferentbasis,notablyNFU(averyimpredicativematerialsettheorywithasetofallsets)andETCS(astructuralsettheory). (Thesourceforthishistory,especiallythedates,ismostlytheEnglishWikipedia.) Axioms ZFCZFCisasimplytypedfirst-ordermaterialsettheory,withasingletypeVVcalledthecumulativehierarchyandabinarymembershippredicate∈\inonVV.EverytermofVVinstandardZFCZFCisapureset,whichwewillcallsimplyaset.Asetaaissaidtobelongto,bein,beamemberof,orbeanelementofasetbbifa∈ba\inb,andsetbbissaidtohavethememberaa. TherearealsovariationsofZFCwithnon-settermssuchasurelementsandclasses.Urelementsmaybedistinguishedfromsetsandclassessincetheyhavenoelements(althoughtheemptysetalsohasnoelements);setsareusuallythoseclassesthatarethemselveselements(members)ofsets.Urelementsarealsocalledatoms,andZFZFwithatomsincludedissometimescalledZFAorZFUZFU. Extensionality:Iftwosetshavethesamemembers,thentheyareequalandthemselvesmembersofthesamesets.Seeaxiomofextensionalityforvariations,suchaswhetherthisistakenasadefinitionoranaxiomatisationofequalityofsets,andhowtheconditionmightbestrengthenedif(10)isleftout. NullSet:Thereisanemptyset:aset∅\emptywithnoelements.By(1),itfollowsthatthissetisunique;byeventheweakestversionof(5),itisenoughtostatetheexistenceofsomeset.(Analogousremarksapplytoaxioms(3),(4),(6),(7),and(8),exceptwhen(5)isomittedand(4)and(6)areneededtoderiveit.) Pairing:Ifaaandbbaresets,thenthereisaset{a,b}\{a,b\},theunorderedpairingofaaandbb,whoseelementsarepreciselythosesetsequaltoaaorbb.Betweenthem,(2)and(3)formanullary/binarypair;theunaryversionfollowsfrom(3),since{a}={a,a}\{a\}=\{a,a\}by(1).Thehigherfinitaryversionsrelyalsoon(4)(with{a,b,c}={a}∪{b,c}\{a,b,c\}=\{a\}\cup\{b,c\},etc),sotheyshouldprobablybestatedexplicitlyasanaxiomscheme?if(4)isomitted(butnobodyseemstodothat). Union:If𝒞\mathcal{C}isaset,thenthereisaset⋃𝒞\bigcup\mathcal{C},theunionof𝒞\mathcal{C},whoseelementsarepreciselytheelementsoftheelementsof𝒞\mathcal{C}.ItisnormaltowriteA∪BA\cupBfor⋃{A,B}\bigcup\{A,B\},etc,A∪B∪CA\cupB\cupCfor⋃{A,B,C}\bigcup\{A,B,C\},etc.Notethat⋃{A}=A\bigcup\{A\}=Aand⋃∅=∅\bigcup\empty=\empty(using(1)toprovetheseresults),sonospecialnotationisneededforthese. Separation/Specification/Comprehension:Givenanypredicateϕ[x]\phi[x]inthelanguageofsettheorywiththechosenfreevariablexxoftypeVV,ifUUisaset,thenthereisaset{x∈U|ϕ[x]}\{x\inU\;|\;\phi[x]\},thesubsetofUUgivenbyϕ\phi,whoseelementsarepreciselythoseelementsxxofUUsuchthatϕ[x]\phi[x]holds.Therearemanyvariations,fromBoundedSeparationtoFullComprehension,whichweshouldprobablydescribeataxiomofseparation;theversionlistedhereisFullSeparation.Thisisanaxiomscheme?,butitcanbemadeasingleaxiominNBGNBG(butnotcompletelyinMKMK).Notethat(5)followsfrom(4)and(6)usingclassicallogic,soitisoftenleftout,butitmustbeincludedinintuitionisticvariations,variationswhere(6)isomittedorweakened(orwhere(4)isomittedorweakened,inprinciple,althoughthatneverhappensinpractice),andvariationswhere(5)itselfisstrengthened. Replacement/Collection:Givenapredicateψ[x,Y]\psi[x,Y]withthechosenfreevariablesxxandYYoftypeVV,ifUUisasetandifforeveryxxinUUthereisauniqueYYsuchthatψ[x,Y]\psi[x,Y]holds,thenthereisset{ιY.ψ[x,Y]|x∈U}\{\iota\,Y.\;\psi[x,Y]\;|\;x\inU\},theimageofUUunderψ\psi,whoseelementsarepreciselythosesetsYYsuchthatthereisanelementxxofUUsuchthatψ[x,Y]\psi[x,Y]holds;ifΨ[x]\Psi[x]isadefinedterm,thenwewrite{Ψ[x]|x∈U}\{\Psi[x]\;|\;x\inU\}for{ιY.Y=Ψ[x]|x∈U}\{\iota\,Y.\;Y=\Psi[x]\;|\;x\inU\}.Againtherearemanyvariations,fromWeakReplacementtoStrongCollection,whichweshouldprobablydescribeataxiomofreplacement;theonedescribedhereisReplacement.Thisisalsoanaxiomscheme?,butitcanbemadeintoasingleaxiominbothNBGNBGandMKMK.Onecouldcombinethiswith(5)toproduce{ιY.ψ[x,Y]|x∈U|ϕ[x]}\{\iota\,Y.\;\psi[x,Y]\;|\;x\inU\;|\;\phi[x]\},butnobodyseemstodothis. PowerSets:IfUUisaset,thenthereisaset𝒫U\mathcal{P}U,thepowersetofUU,whoseelementsarepreciselythesubsetsofUU,thatisthesetsAAwhoseelementsareallelementsofUU.Whenusingintuitionisticlogic,itispossibletoacceptonlyaweakversionofthis,suchasSubsetCollectionor(evenweaker)Exponentiation.Butinclassicallogic,PowerSetsfollowsfromExponentiationandtheweakestformof(5). Infinity:Thereisasetω\omegaoffiniteordinalsaspuresets.Normallyonestatesthat∅∈ω\empty\in\omegaanda∪{a}∈ωa\cup\{a\}\in\omegawhenevera∈ωa\in\omega,althoughvariationsarepossible.Usinganybuttheweakestversionof(6),itisenoughtostatethatthereisasetsatisfyingPeano'saxiomsofnaturalnumbers,orevenanyDedekind-infiniteset.Itseemstobeuncommontoincorporate(2)into(8),butinprinciple(8)implies(2). Choice:If𝒞\mathcal{C}isaset,eachofwhoseelementshasanelement,thenthereisasetwithexactlyoneelementfromeachelementof𝒞\mathcal{C}.Notethatthissetisnotunique,norcanweconstructacanonicalversionwhichis,sowedonotgiveitanynameornotation.ThisversionisthesimplesttostateinthelanguageofZFCZFC;seeaxiomofchoiceforfurtherdiscussionandweakversions.Itispossibletoincorporate(9)into(5)or(6),butthisseemstoberare. Foundation/Regularity/Induction:Givenaformulaϕ\phiwithachosenfreevariableXXoftypeVV,ifϕ\phiholdswheneverϕ[a/X]\phi[a/X]holdsforeverya∈Xa\inX,thenϕ\phiholdsabsolutely.Forvariations(includingtheaxiomofanti-foundation),seeaxiomoffoundation.Thisaxiomscheme?canbemadeintoasingleaxiomeveninZFCZFCitself(althoughnotinversionswithintuitionisticlogic;inthatcaseitcanbemadeasingleaxiomonlyinaclasstheory). Variations Zermelo'soriginalversionconsistsofaxioms(1–5)and(7–9),inasomewhatimpreciseform(whichaffectstheinterpretationof5)ofhigher-orderclassicallogic. ThemodernZFZFconsistsof(1–8)and(10),usingfirst-orderclassicallogic,thestrongestformof(6)(thatis,StrongCollection,althoughthestandardReplacementissufficientwithclassicallogic),andthestrongestformof(5)possibleusingonlysetsandnotclasses(FullSeparation).SinceFullSeparationfollowsfromReplacementwithclassicallogic,itisoftenomittedfromthelistofaxioms. ZFCZFCadds(9)andisthusthestrongestversionwithoutclassesoradditionalaxioms.TheversionoriginallyformulatedbyFraenkelandSkolemdidnotinclude(10),althoughthethreefoundersalleventuallyacceptedit. ItiscommontotakeZermelosettheory(Z\mathrm{Z})tobeZFZFwithout(6),althoughZermeloneveracceptedthefirst-orderformulation;notethattheweakestform(WeakReplacement)of(6)followsfrom(7)and(5),soitholdseveninZ\mathrm{Z}. AnothervariantisboundedZermelosettheory(BZBZ),whichislikeZ\mathrm{Z}butwithonlyBoundedSeparation;thisisofinteresttocategorytheoristsbecauseBZCBZCisequivalenttoETCS. Constructiveversions Seealsoconstructivesettheory. Themostwell-knownfoundationsforconstructivemathematicsthroughmaterialsettheoryarePeterAczel'sconstructiveZermelo–Fraenkelsettheory(CZFCZF)andJohnMyhill'sintuitionisticZermelo–Fraenkelsettheory(IZFIZF). CZFCZFusesaxioms(1–8)and(10),usuallyweakforms,inintuitionisticlogic;specifically,itusesBoundedSeparationfor(5),StrongCollectionfor(6),andanintermediate(SubsetCollection)formof(7).IZFIZFissimliar,butitusesFullSeparationfor(5)andthefullstrengthof(7);Myhill'soriginalversionusesonlyReplacementfor(6),butCollection(equivalenttoStrongCollectionusingFullSeparation)isstandardnow. Notethatadding(9)toIZFIZFimpliesexcludedmiddleandsomakesZFCZFC.However,someauthorsliketoincludeaweakformof(9),suchasdependentchoiceorCOSHEP. MikeShulman'ssurveyofmaterialandstructuralsettheories(Shulman2018)takesCPZ↺−CPZ^{\circlearrowleft-}asthemostbasicform;itconsistsof(1–4)andtheweakestversions(BoundedSeparationandWeakReplacement)of(5&6)inintuitionisticlogic.Adding(10)givesCPZ−CPZ^{-},adding(8)givesCPZ↺CPZ^{\circlearrowleft},andaddingbothgivesCPZCPZ,constructivepre-Zermelosettheory.Shulmangivessystematicnotationforotherversions,whichincludesthose(constructiveandclassical)listedabove. Myhillhasanotherversion,constructivesettheory(CSTCST);thisconsistsof(1–4),BoundedSeparationfor(5),Replacementfor(6),theweakest(Exponentiation)formof(7),(8),andaweakversion(DependentChoice)of(9).Italsousesavariationofthelanguage,withurelementsfornaturalnumbers;notethattheexistenceofω\omegastillfollowsusing(6).ThisclassifiesCSTCSTasCΠZF↺+DC\mathrm{C}{\Pi}ZF^{\circlearrowleft}+DCinShulman'ssystemifoneignorestheuseofurelementsandstrengthensReplacementtoStrongCollection. Classtheories Morse–Kelleyclasstheory(MKMK)featuresbothsetsandproperclasses.Thisallowsittostrengthen(5)toFullComprehension,sinceϕ\phicanincludequantificationoverclasses;thesameholdsin(6)and(10),althoughthisdoesnotaddanyadditionalstrength. VonNeumann–Bernays–Gödelclasstheory(NBGNBG)usesthesamelanguageasMKMK,butitstillusesonlyFullSeparationfor(5).ThismakesitconservativeoverZFCZFCandalsoallowsforafiniteaxiomatisation;wereplacetheformulasin(5)and(6)withclasses,andaddsomespecialcasesof(5)forsubclasses,oneforeachlogicalconnective.(ItisprovablethatplainZFZF,ifconsistent,cannotbefinitelyaxiomatizedinitsownfirst-orderlanguage;NBGNBGescapesthisconclusionbyextendingthelanguagewiththenotionofclasses.) OnecanalsoreworkalloftheweakversionsofsettheoryaboveintoaclasstheorylikeNBGNBG,whichisconservativeovertheoriginalsettheory.OnecanalsouseaclasstheorylikeMKMK,althoughthisdestroysanyattempttouseaweakversionof(5). Largecardinals OneoftenaddsaxiomsforlargecardinalstoZFCZFC.Even(8)canbeseenasalargecardinalaxiom,statingthatℵ0\aleph_0exists.Theseadditionalaxiomsaremostcommonlystudiedinthecontextofamaterialsettheory,buttheyworkjustaswellinastructuralsettheory. Notethataddinganinaccessiblecardinal(commonlyconsideredthesmallestsortoflargecardinal)toZFCZFCisalreadystrongerthanMKMK:givenaninaccessiblecardinalκ\kappa,onecaninterpretthesetsandclassesinMKMKasthesetsinVκV_\kappaandVκ+1V_{\kappa+1},respectively.Ofcourse,onecanaddalargecardinaltoMKMKtogetsomethingevenstronger. Itisoftenconvenienttoassumethatonealwayshasmorelargecardinalswhennecessary.Youcannotsaythisinanabsolutesense,butyoucanadopttheaxiomthateverysetbelongstosomeGrothendieckuniverse.AddingthisaxiomtoZFCZFCmakesTarski–Grothendiecksettheory(TGTG).Thisisnotthelastword,however;youcanmakeitstrongerbyaddingclassesinthestyleofMKMK,orevenaddingacardinalwhichisinaccessiblefromTGTG.Infact,wehavebarelybegunthelargecardinalsknowntomodernsettheory! Miscellaneousvariations Theaxiomofconstructibility,usuallynotated“V=LV=L”,isaverystrongaxiomthatcanbeaddedtoZFZF;itassertsthatallsetsbelongtotheconstructibleuniverseLL,whichcanbe“constructed”inadefinablewaythroughatransfiniteprocedure.Thisnotionof“constructible”shouldnotbeconfusedwithconstructivemathematics;forinstance,V=LV=Limpliestheaxiomofchoiceandthusalsoexcludedmiddleevenwithintuitionisticlogic.V=LV=Lalsoimpliesthegeneralizedcontinuumhypothesis(GCHGCH),whichishowGödeloriginallyprovedthatGCHGCHwasconsistentwithZFCZFC.However,itisincompatiblewiththesufficientlylargecardinals:theexistenceofameasurablecardinalimpliesthatV≠LV\neqL.MostcontemporarysettheoristsdonotregardV=LV=Laspotentially“true.” Theaxiomofdeterminacy(ADAD)isanotheraxiomthatcanbeaddedtoZFZF;itassertsthatacertainclassofinfinitegame?sisdetermined(oneplayerortheotherhasawinningstrategy).ADADisinconsistentwiththefullaxiomofchoice,althoughitisconsistentwithdependentchoice.AweakerformofADADcalled“projectivedeterminacy”isconsistentwithACACandisequiconsistentwithcertainlargecardinalassertions. TheGCHGCHitself,oritsnegation,couldalsoberegardedasanadditionalaxiomthatcanbeaddedtoZFZF.Manysettheoristswouldprefertofindamore“natural”axiom,suchasalargecardinalaxiom,whichimplieseitherGCHGCHoritsnegation.Theequiconsistencyofprojectivedeterminacywithalargecardinalassertioncanberegardedasastepinthisdirection. Relationtostructuralsettheories ThestructuralsettheoryETCSisequivalenttoBZCBZCinthatthecategoryofsetsinthattheorysatisfiesETCSETCSwhilethewell-foundedpuresetsinETCSETCSsatisfyBZCBZC.Thisuses(1–4),BoundedSeparationfor(5),and(7–10),withWeakReplacementfollowingfrom(5)and(7). MikeShulman'sSEARCisequivalenttoZFCZFCinthesameway.SEARSEAR,whichlackstheaxiomofchoice,isequivalenttoZF↺ZF^{\circlearrowleft},whichisZFZFwithout(10),inaweakersenseofequivalence. Shulman2018isanextensivesurveyofvariationsofZFCZFCandvariationsofETCSETCS(mostlyweakones),showinghowthesecorrespond. Relatedentries materialsettheory algebraicsettheory cumulativehierarchy References Zermelo’saxiomatisationgrewoutofhisreflectionsonhisproofsofthewell-orderingtheorem(1904/08)andwaspublishedin ErnstZermelo,UntersuchungenüberdieGrundlagenderMengenlehreI,Math.Ann.65(1908)pp.261-81.(gdz) EnglishversionsoftheearlykeytextsonsettheorybyZermelo,Fraenkel,Skolem,vonNeumannetal.canbefoundin J.vanHeijenoort,FromFregetoGödel-ASourcebookinMathematicalLogic1879-1931,HarvardUP1967. TherearemanytextswhichdiscussZFCandthecumulativehierarchyfromatraditional(material)set-theoreticperspective.Agoodexampleis KennethKunen,SetTheory:AnIntroductiontoIndependenceProofs,StudiesinLogicandtheFoundationsofMathematicsVol.102(2006),Elsevier. AclassificationofaxiomsofvariantsofZFCZFC,withaneyetowardscorrespondingstructuralsettheories,is MichaelShulman(2018).Comparingmaterialandstructuralsettheories.arXiv:1808.05204. LastrevisedonFebruary6,2021at20:21:31. Seethehistoryofthispageforalistofallcontributionstoit. EditDiscussPreviousrevisionChangesfrompreviousrevisionHistory(40revisions) Cite Print Source