Está claro que primero tengo que definir formalmente lo que entiendo por teorema "basura". En el habitual construcción de números naturales en la teoría de conjuntos un efecto secundario de esa construcción es que obtenemos tal teoremas como $2\in 3$ , $4\subset 33$ , $5 \cap 17 = 5$ et $1\in (1,3)$ pero $3\notin (1,3)$ (como pares ordenados, en la presentación habitual).
Formalmente: Dada una teoría axiomática T, y un modelo de la teoría M en teoría de conjuntos, una sentencia verdadera $S$ en el lenguaje de la teoría de conjuntos es un teorema de la basura si no expresa una sentencia verdadera en T.
¿Sería correcto decir que teoría estructural de conjuntos es un intento de deshacerse de esos teoremas basura?
EDIT: como se ha señalado $5 \cap 17 = 5$ podría interpretarse correctamente en la teoría de entramados como que no es un teorema basura. El problema que tengo es que (desde la perspectiva de las ciencias de la computación) esto no es modular: uno está confundiendo la implementación concreta (en términos de conjuntos) con la firma abstracta de la TAD (de celosías). Por lo demás, las matemáticas son muy modulares (eso es lo que captan muy bien los Functores, por ejemplo), ¿por qué no la teoría de conjuntos también?