# "Set theory" founded on lists rather than sets

On a computer, sets are often represented rather "indirectly / implicitly", e.g. in terms of some properties that they or their members satisfy. But some sets can be represented more "directly / explicitly", in the sense that the representation either directly contains, or gives an algorithm for enumerating, a representation of every individual element of the set. I realize that might still be quite a vague distinction, but hopefully it'll be clear enough for what follows.

Any "directly represented" set must of course be countable, and hence well-orderable regardless of one's stance on the axiom of choice. But more than that, the representation of the set must actually come with a particular well-ordering, since the elements must be represented or enumerated in some order regardless of whether that order is actually used for anything else. It's possible to some extent to work with such direct representations of sets without caring about the ordering, but one must first define an appropriate notion of equivalence up to reordering.

What would happen if we made such (implicitly) well-ordered countable sets the basis for a form of set theory, insisting on some sort of ω-rule to avoid ω-inconsistency, and then treated uncountable sets e.g. as proper classes, or as sets whose only properties we can discuss are those pertaining to their well-ordered countable subsets [edit: or quotients]? Has such a theory been characterized?

• What would we still be able to prove? What statements would definitely be independent of such a theory?
• What about statements in-between, where the definiteness depended on the precise formulation of the theory?
• What kinds of nonstandard models could such a theory have?

Edit: I realize that one possible ambiguity is which countable well-orders are allowed in this theory. My intended meaning was that only well-ordered sets of type ≤ω would be given a priori, but at least some ordinals larger than this could be modelled in the sense that if X has given order-type ω then we can construct X×X, also with given order-type ω (via e.g. Cantor's pairing function) and then construct a well-ordering relation on X×X of type ω2, say.

• Regarding downvotes: I accept that this question may be below research level or even poorly-defined, but would appreciate some feedback in the form of pointers to literature / textbooks, or a clarification of where the ambiguity lies so that I can try to resolve what question I really meant to ask. Thanks. Feb 12 '16 at 22:06
• John McCarthy would be proud. :-P Feb 12 '16 at 23:08
• actually your question is, in my modest opinion, very interesting. In a way sets are not the most basic entities: they are equivalence classes of lists up to re-ordering. Would be nice to have a precise characterization of set theory along these lines.... Feb 12 '16 at 23:12
• @AsafKaragila I did notice the connection with Lisp, which is part of the reason I feel like someone else must have done this decades ago. Feb 12 '16 at 23:32
• There is a weak notion of categorical foundations known as a 'list-arithmetic pretopos', which is one way of formalising Joyal's never published proposition for a notion called by him 'arithmetic universe'. Feb 13 '16 at 8:59