most recent 30 from http://mathoverflow.net 2013-05-18T23:33:26Z http://mathoverflow.net/feeds/question/51834 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/51834/multitype-approaches-to-choice David Feldman 2011-01-12T10:16:34Z 2011-01-12T10:16:34Z

<p>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). </p> <p>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.)</p> <p>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.</p>