I don't think anyone minds this. The purpose of a formal foundation is to prove useful theorems. Junk theorems are just a side effect. But I'm always tickled by logicians who think type theories are philosophically superior to set theories because in some of the latter you might be able to prove something like 1 ∈ 2, whereas type theories, even without their own junk theorems, have a pragmatic difficulty with division (hence they tend to define 1/0 = 0). Junk theorems just come with the territory, and foundations need to be considered based on their utility, not philosophical purity, which is never achieved anyway (at least not without a cost to utility).
> But I'm always tickled by logicians who think type theories are philosophically superior to set theories because in some of the latter you might be able to prove something like 1 ∈ 2
Note that this is actually how the basic ZF construction works, where 0 = {} and successor(n) = n ∪ {n}, so you immediately get 2 = {0, 1} and thus 1 ∈ 2 , without any need for a proof.
Except it suffices to know that some construction that supports the integer/natural axioms exists without having any specific theorems, such as 1 ∈ 2, about its specifics. In fact, in TLA+, which contains a formalised set theory, the construction is not part of the definition of the integers, and 1 ∈ 2 (or any other theorem about the construction of the integers) is not provable (of course, 1 ∉ 2 is not provable, either). The details of the construction can remain unknowable.
Anyway, my point is that type theories contain at least as many junk theorems as set theories, if not more, and junk theorems are fine either way. Neither approach is more philosophically pure. Any claims to that effect are really an expression of personal aesthetic preferences.
