Borel determinacy requires countable-ordinal-iterations of powerset, for arbitrary countable ordinals, which is weaker than uncountably many.
]]>Requires uncountably many applications of powerset operation in its proof (result of Friedman)
Anonymous
]]>sets are characterized by the membership relation and propositional equality in material set theory.
Anonymous
]]>membership function -> membership relation
Anonymous
]]>changed clause
This is in contrast to traditional “material set theory” such as ZFC or ZFA, where sets are characterized by the membership function
to
This is in contrast to traditional “material set theory” such as ZFC or ZFA, where sets are characterized by the membership function alone
Anonymous
]]>replaced
This is in contrast to traditional Zermelo-Fraenkel-style “material set theory” where sets can be elements of other sets, where the primitive global set-membership relation “” forces one to think of all elements of sets as sets themselves, hence of sets-of-sets-of-sets-…, a feature that is almost never actually used or even considered in mathematics, away from the study of material set theory itself.
with
This is in contrast to traditional “material set theory” such as ZFC or ZFA, where sets are characterized by the membership function , and where sets can be elements of other sets, hence where there are sequences of sets which are elements of the next set in the sequence, the latter feature which is almost never actually used or even considered in mathematics, away from the study of material set theory itself.
Anonymous
]]>This is in contrast to traditional Zermelo-Fraenkel-style “material set theory” where the primitive global set-membership relation “” forces one to think of all elements of sets as sets themselves, hence of sets-of-sets-of-sets-…, a feature that is almost never actually used or even considered in mathematics, away from the study of material set theory itself.
This paragraph is just flat out wrong. Any material set theory with non-set urelements such as ZFA is a material set theory which does not force one to think of all elements of sets as sets themselves, as urelements are elements which are not sets. One could interpret Zermelo-Fraenkel-style “material set theory” as referring only to pure set theories, but I don’t think the distinction between pure set theory and non-pure set theories is the right distinction between material and structural set theory.
]]>Updated page to talk about distinguishing set theories by if they include families in the theory
Anonymous
]]>Corrected small spelling error
EFinatS
]]>Looks fine, I think.
]]>Now I noticed that the Examples-section never mentioned the word “topos”. I have given each example a section header, and then added some lines containing the term “topos” to the section on ETCS and also a few words to the section on h-sets .
Would be great if you could fine a minute to fine-tune.
I would like to have the entry say that the idea of sets in HoTT is very much in the spirit (even if different in technical detail) of ETCS, especiall the spirit of “fixing one base topos and then doing all maths in there”. Maybe this could be said in the entry in some way that feels acceptable.
]]>Thanks!
]]>Thanks, this looks pretty good. I tweaked the first paragraph since not all structural set theories (e.g. not SEAR) proceed by axiomatizing functions and the category .
]]>I noticed that structural set theory was not cross-linked with Sets for Mathematics, so I added some.
Then I noticed that the lead-in paragraphs seemed to be lacking some gentle broad remarks before entering technical detail, so I expanded the first paragraph and added a second (before what is now the third).
Experts here may want to touch this further. Let’s try to keep in mind a reader with standard mathematics background but otherwise no initiation. Think of your colleague on the other floor. Try to make the entry give him a good idea of why strutural set theory matters.
]]>external link is fine
]]>algebraic set theory misses a reference to stack semantics (michaelshulman). Should I just add the “external” link, or is there a better way?
]]>Sounds good.
]]>I had a short discussion on structural set theory today. Tom’s beautiful short paper rethinking set theory seems to be missing. Also, we don’t seem to have local set theory by Bell and Aczel. I am inclined to put all three of them in structural set theory. Any objections to this? I seem to recall that we had a pending discussion on reorganizing the set theory pages.
]]>Sure. Thanks!
]]>Ah, I see. I have changed it to the following, is that better?
]]>
Set theory set up in intuitionistic type theory via setoids is structural.
Set theory set up via h-sets in homotopy type theory is structural (Rijke-Spitter 13).
What do you intend the word “generally” to mean? One can just as well set up a material set theory inside ITT, such as Aczel’s construction of CZF.
]]>To the Examples-section at structural set theory I have added the following paragraph:
Generally, set theory set up in intuitionistic type theory is structural. For instance setoids in extensional type theory or h-sets in homotopy type theory (Rijke-Spitter 13).
Hope that’s okay. Please fine-tune if not. But I thought some mentioning like this must not be omitted from that page.
]]>Oops! I forgot to add that reference. Thanks! I also added the other one I intended to add, by McLarty.
]]>I put the reference in.
]]>