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.
