Although it's a little wordy, there is a method of formalizing things that avoids these theorems. To be sure, theorems such as $ \{ \{ \} , \{ \{ \} \} \} \in \{ \{ \} , \{ \{ \} , \{ \{ \} \} \} \} $ remain, but that's not junk; however, $ 2 \in 3 $ (or even $ 2 _ \mathbb N \in 3 _ \mathbb N $) will not be there.

Define a **natural-number system** to be an ordered pair $ ( N , \sigma ) $ such that $ \sigma $ is an ordered pair $ ( z , s ) $ such that $ z $ is an element of $ N $, $ s $ is a function from $ N $ to $ N $, $ z $ is not in the range of $ s $, $ s $ is injective, and the only subset $ A $ of $ N $ such that $ z \in A $ and $ s [ A ] \subseteq A $ is $ N $ itself. Given a natural-number system $ \mathbb N = ( N , ( z , s ) ) $, let $ 0 _ \mathbb N $ be $ z $, let $ 1 _ \mathbb N $ be $ s ( z ) $, etc; similarly, you can define $ + _ \mathbb N $, $ \times _ \mathbb N $, etc. You can now prove theorems about natural numbers; such theorems take the form ‘For each natural number system $ \mathbb N $, […].’, much like theorems about groups take the form ‘For each group $ G $, […].’.

Of course, number theory is unlike group theory in an important respect, which is that all natural-number systems are isomorphic (indeed uniquely isomorphic). This is certainly worth proving (after defining what such an isomorphism is so that you can even state it), but you don't actually have to prove it (or even state it) to start stating and proving theorems about prime numbers or whatever. You might at least want to prove that a natural-number system exists (which is the only place in all of this that requires the Axiom of Infinity), although you don't even have to do that to prove theorems about prime numbers; in any case, the system whose existence you choose to prove plays no special role in the rest of the theory.

In something like ETCS, of course, one always does something like this to construct natural numbers, which is why ETCS seems to have fewer junk theorems. But then when you construct $ \mathbb R $ out of $ \mathbb N $, the junk theorems appear in both formal systems, unless you go through the same rigmarole to define a real-number system, etc. But you can do that.

ETA: If I can cite an authority, this approach is pretty much the one taken by Walter Rudin in Principles of Mathematical Analysis (baby Rudin) for $ \mathbb R $. In Chapter 1, Rudin defines a complete ordered field, defines an isomorphism between such, proves that any two such are uniquely isomorphic, and says that we will now use any one of them and not worry about which one it is. Thus the remainder of the book essentially becomes preceded by ‘If $ \mathbb R $ is a complete ordered field’. (In an appendix to the chapter, he proves that one exists, he but makes no further reference to that construction.)

type theory? Why do you want sets, or global membership? $\endgroup$notacceptable to have junk theorems. Mathematicians want variables to have types, either explicitly ("In this paper we assume that $G$ is a simple group...") or by convention ($f$ is a function, $k$ is an integer, etc). What would happen if a student wrote on a math exam "If $1 \in (x,y)$ then $x = 0$ or $y = 0$"? They would say the statement makesno senseand would refuse to judge its truth value. These are clear indications that we have a type theory. $\endgroup$materialset theory, that is set theory based on a global membership relation. But the OP and other commenters are also talking aboutstructuralset theory. What's important is that mathematicians can keep on talking about sets like we always do but still purge the junk statements from our formal language. A structural set theory, while arguably a type theory and certainly quite similar to a type theory, is still a set theory because it is a theory of sets. $\endgroup$31more comments