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?
Best Answer
What you are describing is the idea of "breaking" an abstraction. That there is an abstraction to be broken is pretty much intrinsic to the very notion of "model theory", where we interpret the concepts in one theory in terms of objects and operations in another one (typically set theory).
It may help to see a programming analogy of what you're doing:
All of these are examples of the very same thing you are complaining about in the mathematical setting: when you are presented with some sort of 'type', and operations for working on that type, but it is actually implemented in terms of some other underlying notions. In the above:
I've broken the abstraction of a
uint32_t
representing a number modulo $2^{32}$, by peeking into its byte representation and extracting a byte.I've broken the abstraction of a string being made out of characters, by using knowledge that the character
'T'
and the ASCII value84
are the same thingIn the third, I've broken the abstraction that
big_number
is an object of type integer, and peeked into the internals of how the GMP library stores such things.In order to avoid "junk", I think you are going to have to do one of two things:
(Or, depending on exactly what you mean by the notation, the symbols $2$ and $3$ aren't expressing constants in the theory of natural numbers, but are instead expressing constants in set theory.)