Where is axiom of regularity actually used?
Where is axiom of regularity actually used? Why is it important? Are there some proofs, which are substantially simpler thanks to this axiom?
This question was to some extent provoked by Dan Christensen's comment: Would regularity ever be used in a formal development of, say, number theory or real analysis? I can't imagine it.
I have to admit that I do not know other use of this axiom than the proof that every set has rank in cumulative hierarchy, and a few easy consequences of this axiom, which are mentioned in Wikipedia article.
I remember seeing an introductory book in axiomatic set theory, which did not even mention this axiom. (And that book went through plenty of stuff, such as introducing ordinals, transfinite induction, construction of natural numbers.)
Wikipedia article on Non-well-founded set theory links to Metamath page for Axiom of regularity and says: Scroll to the bottom to see how few Metamath theorems invoke this axiom.
Based on the above, it seems that quite a lot of stuff can be done without this axiom.
Of course, it's quite possible that this axiom becomes important in some areas of set theory which are not familiar to me, such as forcing or working without Axiom of Choice. (It might be difficult to define cardinality without AC and regularity, as mentioned here.) But even if the this axiom is important only for some advanced stuff - which I will probably never get to - I'd be glad to know that.
Solution 1:
Basic mathematics was done long before set theory. Its users couldn't care less whether or not ZF is the underlying theory of the universe or some other theory. As long as it works fine.
There are a few things to point out:
The natural numbers (standard model of PA), on which classical number theory is developed, are well-ordered regardless to their construction. This is one of their defining properties, after all. Therefore all the inductions we use on them hold regardless to whether or not regularity holds in general.
Classical analysis can be developed, again, without regularity to hold. Most basic theorems (i.e. freshman calculus) are theorems about continuous functions or sequences of real numbers.
Even if the axiom of regularity fails, it still holds in an inner model (granted the other axioms of ZF hold). Therefore even without regularity we can still insist on working with sets for which regularity holds.
The main idea behind having set theory as a foundational theory is that we can carry out the "non set-theoretic" constructions as sets. There is, at least in the basic level of mathematics, little to none interaction between the mathematics and the foundational theories. This is the same reason we don't see proofs assuming CH during our first two-three years of mathematics, these assumptions while interesting are irrelevant for basic mathematics.
Within set theory, the rank function and the Mostowski collapse are already enough reason for assuming it, and these are used a lot.
Solution 2:
Here's an (IMO) interesting example. Surely you're familiar with the set-theoretic interpretation of ordered pairs given by $(x,y) = \{ \{ x \}, \{ x, y \} \}$. You may wonder, why not use $(x,y) = \{ x, \{ x, y\}\}$?
We can... if we assume some amount of regularity. If there exists a set $S$ satisfying $S = \{ \{S, T\}, U \}$ with $T \neq U$, then we would have
$$ (S, T) = \{ S, \{ S, T \} \} = \{ \{ \{ S, T \}, U \}, \{ S, T \} \} = ( \{ S, T \}, U ) $$
which contradicts the property of ordered pairs $(S, T) = (X, Y) \implies S = X \wedge T = Y$, however regularity forbids the existence of such a set $S$.