[adrian_b]

Slightly off-topic, but in any mathematical theory concerning a certain restricted domain and also in any theory attempting to cover the entire mathematics there are many possible choices for the primitive concepts and rules.

In most cases it is not possible to have an objective criterion for deciding which is the best choice, so the choice remains based on personal preferences.

For example, I could never accept the idea that set theory can be considered to belong to the foundations of mathematics.

I have always believed that it is more convenient to view the sets not as primitives, but as classes of equivalence of the ordered sequences, which in turn are constructed from ordered pairs, which are a primitive concept.

So instead of using set theory as a base, I believe it to be more convenient to start from some primitives that include some of the concepts and operations on which LISP was also based, plus some definitions, which normally are introduced using sets, modified to use ordered sequences instead.

All the set theory (and the number theory) can be constructed from these alternative primitive concepts.

[devit]

That doesn't work as written for uncountable sets.

[kmill]

That's true, but there's an amusingly odd theorem (downwards Lowenheim-Skolem) that implies that if set theory has a model, it has a countable model. So, in a sense, all sets are countable. I think this just leads you to the next problem, which is that (I think) it would be undecidable normalizing and sorting these sets.