Clearly I first need to formally define what I mean by "junk" theorem. In the usual construction of natural numbers in set theory, a side-effect of that construction is that we get such theorems as $2\in 3$, $4\subset 33$, $5 \cap 17 = 5$ and $1\in (1,3)$ but $3\notin (1,3)$ (as ordered pairs, in the usual presentation).
Formally: Given an axiomatic theory T, and a model of the theory M in set theory, a true sentence $S$ in the language of set theory is a junk theorem if it does not express a true sentence in T.
Would it be correct to say that structural set theory is an attempt to get rid of such junk theorems?
EDIT: as was pointed out $5 \cap 17 = 5$ could be correctly interpreted in lattice theory as not being a junk theorem. The issue I have is that (from a computer science perspective) this is not modular: one is confusing the concrete implementation (in terms of sets) with the abstract signature of the ADT (of lattices). Mathematics is otherwise highly modular (that's what Functors, for example, capture really well), why not set theory too?
