I wonder if anyone has developed a set theory which approaches the issue of the non-emptiness of products of non-empty sets via a hierarchy of types (comparable to how Von Neumann–Bernays–Gödel set theory addresses a different foundational crisis).

So what I have in mind might go like this: One could start with the axioms of ZF for, call them here 0-sets. Next, instead of AC, one would merely have the guarantee that the appropriate products of 0-sets contained a 1-set, a new type. Then I suppose that 0-sets and 1-sets together should again satisfy ZF. Then next, appropriate products of 1-sets indexed by a 0-set, or by a 1-set, or families of 0-sets indexed by 1-set would contain elements of even "higher" type(s). (I don't have a precise proposal for the best or right hierarchy of types - that's what I'm hoping to learn if the idea isn't new.)

My motivation lies in seeking a compromise between simply rejecting AC and accepting AC uncritically, in the form of a theory that forces one to track of how much choice one uses as one goes. Perhaps the hierarchy of types should even distinguish known weak forms of choice (countable, dependent, BPIT, etc.) Perhaps non-trivial facts would cause a naive proposal for a hierarchy of types to collapse. I'd welcome any thoughts on these issues if in fact this hasn't all been worked out somewhere.

  • $\begingroup$ I'm fairly confident what you are describing is not new, however I reserve the right to be dead wrong. I suggest that you take a look at a couple of books before you get too carried away: Axiom of Choice, by Horst Herrlich and The Axiom of Choice, by Jech. Herrlich's is a much more complete treatment. However, if this kinda stuff is not your 'cup o tea' I'd start with Jech's. $\endgroup$ – Not Mike Jan 26 '11 at 1:47
  • $\begingroup$ Thanks Michael. I've looked at both books now. I don't see any attempt to more away from the standard language of set theory. Neither book mentions type or type theory in the index. I'm often scooped, so that wouldn't shock me, but you say you're confident, so please say why. $\endgroup$ – David Feldman Jan 26 '11 at 4:42
  • $\begingroup$ Well, because what you have described (unless I'm mistaken about some fine point) is the cumulative hierarchy, or something similar to ZF with atoms (if you don't start with the empty set.) Moreover, you have asserted that choice maintains throughout it, except possibly for the base level 0-type objects, thus producing the full axiom of choice obtains almost everywhere. $\endgroup$ – Not Mike Jan 29 '11 at 7:07
  • $\begingroup$ With that rolling around in the back of my mind, I suggested Jech's book. As it has a nice self contained bit on ZFA, which I have always enjoyed. $\endgroup$ – Not Mike Jan 29 '11 at 7:09
  • $\begingroup$ Hi Michael. If you want AC to fail and you don't mind violating the axiom of extension (AE), urelements provide a technique. It's not enough, though, just to start with some urelements, you also want some group acting on them, and you want to carve out as a submodel just the hereditarily symmetric sets. All fine, these tools should lead to models of my hypothetical language, either provided I drop AE or imitate urelements via forcing. But having models doesn't substitute for crafting the language in the first place. Yes, I'm proposing a hierarchy, but one that extends or refines the ... $\endgroup$ – David Feldman Jan 29 '11 at 7:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.