Axiom of regularity for sets and other types!

Question

This is really not a mathematical question, but a philosophical question about the theory in which mathematicians work. Andreas Blass describes this theory T as follows (here):

Mathematicians generally reason in a theory T which (up to possible minor variations between individual mathematicians) can be described as follows. It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. For example, there are axioms saying that the real numbers form a complete ordered field, that any formula determines the set of those reals that satisfy it (and similarly with other sorts in place of the reals), that two tuples are equal iff they have the same length and equal components in all positions, etc.

There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind. (Different mathematicians may disagree as to whether, say, the real numbers are a subset of the complex ones or whether they are a separate sort with a canonical embedding into the complex numbers. Such issues will not affect the general idea that I'm trying to explain.) So mathematicians usually do not say that the reals are Dedekind cuts (or any other kind of sets), unless they're teaching a course in foundations and therefore feel compelled (by outside forces?) to say such things.

Question: Does this theory T contain the axiom of regularity? If yes, then it would follow that there is no set $A$ with $A\in A$, for example. But it wouldn't follow that there is no function $f$ with $f\colon \{f\}\to\{f\}$, since there are no axioms that attempt to reduce one sort to another. So should one add a version of the "axiom of regularity" for every type? What would one get if one only has the axiom of regularity for sets, but not for functions, tupels, and so on? Which branches of mathematics would this issue concern? When does it matter for which types one has the regularity axiom available?

Do set theorists also work in this theory T, or are they using a pure set theory, i. e. a theory in which all objects are sets?

Answer 1

You don't need the axiom of regularity, since you usually can't even say $A \in A$ in this theory.

For example, suppose $A$ is a variable of type $\mathcal{P}(\mathbb{R})$, and $r$ is a variable of type $\mathbb{R}$.

There is, for example, a relation named $\in$ on the type $\mathbb{R} \times \mathcal{P}(\mathbb{R})$, and we could posit the proposition $r \in A$.

However, this theory generally does not include a relation named $\in$ on the the type $\mathcal{P}(\mathbb{R}) \times \mathcal{P}(\mathbb{R})$ — so the theory offers no way to formulate the proposition $A \in A$.