Set theories without "junk" theorems? - MathOverflow

Set theories without "junk" theorems?

2012-03-10T14:34:19Z

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?

Answer by Andreas Blass for Set theories without "junk" theorems?

2012-03-10T16:38:50Z

Structural set theory, as described on the nlab page you linked to, is probably the best answer to your question. To avoid junk theorems, one must deviate somewhat from ordinary ZF-style set theory where everything is a set. That's because, once you decide, in the context of such a "material" set theory, that 5 and 17 are to be sets (because there's nothing else for them to be), they have to have a union, and there's no intuitively reasonable choice for that. (I said "union" rather than "intersection" because one might consider the empty set a reasonable intersection; but the union can't be empty unless both sets are.) A very elementary (undergraduate) presentation of some mathematics from this viewpoint is in the book "Sets for Mathematics" by Lawvere and Rosebrugh; a more advanced presentation is (if I remember correctly) Paul Taylor's "Practical Foundations of Mathematics".

Answer by Hurkyl for Set theories without "junk" theorems?

2012-03-10T19:07:33Z

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:

uint32_t x = 0x12345678;
unsigned char *ptr = (unsigned char *) x;
assert( ptr[0] == 0x12 || ptr[0] == 0x78 );  // Junk!

const char text[] = "This is a string of text.";
assert( text[0] == 84 );  // Junk!

// Using the GMP library.
mpz_t big_number;
mpz_init_ui(big_number, 1234);
assert(big_number[0]._mp_d[0] == 1234); // Junk!

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 value 84 are the same thing
In 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:

Abandon the notion of model entirely
Realize that you were actually lying in your theorems: it's not that $2 \in 3$ for natural numbers $2$ and $3$, but $i(2) \in i(3)$ for a particular interpretation $i$ of Peano arithmetic. Maybe making the interpretation explicit would let you be more comfortable?

(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)

Answer by кристиан for Set theories without "junk" theorems?

2012-03-10T19:38:58Z

i think the construction of formal theories has a price, the price is that you will get a lot of prepositions (not theorems) that would be natural and simple, but that is part of life, you will meet a lot of them all the time.

Answer by Michael Blackmon for Set theories without "junk" theorems?

2012-03-11T06:09:07Z

Among the many subtle realities of mathematics in the 21st century, the most amazing is the lack of imagination. The language of set theory is built from the ground up to be as simple as possible. To appreciate the complexity inherent and information encoded in such simple statements (even the ones you might not find aesthetically pleasing) requires detachment.

This detachment I'm talking about is the clear distinction between: syntax and semantics. Statements made in the formal language have absolutely no meaning outside of formal manipulation, and so are not meant to be seen as anything more than symbols without meaning.

It is only when you attach meaning (or an interpretation) to these symbols that something of value can be said.

That having been said:

The examples you give are not actually statements in the language of set theory; they are artifacts of a general lack of communication between logic/model theory and the rest of mathematics. The symbols you strung together (1, $2$, 5, $4 \subset 54$, $\cap$, and so on) are examples of defined notions, which are used as a convenience.

And when we attach meaning to these statements something amazing happens:

What was $2 \in 3$ becomes the obviously true

$\{ \{\}, \{\{\}\} \} \in \{\{\}, \{ \{\}, \{\{\}\} \}\}$

and $1 \in \langle 0, 3 \rangle$ becomes

$\{\{\}\} \in \{ \{ \{\} \}, \{ \{\{\}, \{ \{\}, \{\{\}\} \}\} \}\}$

In Summary:

You are confusing the formal language with the actual interpretation of the language.

As such you are faced with something every body has known since the 19th century:

Our perception imposes "phantom" structure on the universe in an attempt to have it make sense; not the other way around.

PS: Feel free to edit. You also might want to change the title, since the post I wanted to put here would have gotten me banned.

Answer by abo for Set theories without "junk" theorems?

2012-03-11T15:10:58Z

The question being, "Would it be correct to say that structural set theory is an attempt to get rid of such junk theorems?", the answer I think is "only partly or only if extremely limited."

Clicking on the link, I find a theory called ETCS as an example of structural set theory. ETCS has 0, N (the natural numbers), and S (the successor function) as primitives in its language, and it assumes effectively as axioms the normal assumptions about them (e.g. it assumes the existence and uniqueness of recursion).

Obviously, if you assume 0, N, and S as primitives and make the normal assumptions about them, rather than constructing them and proving the normal assumptions (Russell's honest toil rather than theft), then one can avoid junk theorems about the natural numbers. The same effect could be achieved, by modifying ZFC by introducing the same primitives and assuming, on top of the normal ZFC axioms, the Peano Axioms.

ETCS does not, however, get rid of all junk theorems unless it is only supposed to be about arithmetic and the natural numbers. If it, for instance, is also supposed to allow the construction of the real numbers and the development of analysis, then it will still get junk theorems about the real numbers.

Answer by Andreas Blass for Set theories without "junk" theorems?

2012-03-11T22:37:41Z

I apologize for posting as an answer what should really be a comment, connected to one of Jacques Carette's comments on my earlier answer. Unfortunately, this is way too long for a comment. Jacques asked why we would bother with set-theoretic foundations at all. It happens that I wrote down my opinion about that about 15 years ago (in a private e-mail) and repeated some of it on the fom (= foundations of mathematics) e-mail list. Here's a slightly edited version of that:

Mathematicians generally reason in a theory T which (up to possible minor variations between individual mathematicians) can be described as follows. It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. For example, there are axioms saying that the real numbers form a complete ordered field, that any formula determines the set of those reals that satisfy it (and similarly with other sorts in place of the reals), that two tuples are equal iff they have the same length and equal components in all positions, etc.

There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind. (Different mathematicians may disagree as to whether, say, the real numbers are a subset of the complex ones or whether they are a separate sort with a canonical embedding into the complex numbers. Such issues will not affect the general idea that I'm trying to explain.) So mathematicians usually do not say that the reals are Dedekind cuts (or any other kind of sets), unless they're teaching a course in foundations and therefore feel compelled (by outside forces?) to say such things.

This theory T, large and unwieldy though it is, can be interpreted in far simpler-looking theories. ZFC, with its single sort and single primitive predicate, is the main example of such a simpler theory. (I've left large categories out of T in order to make this literally true, but Feferman has shown how to interpret most of category theory, including large categories, in a conservative extension of ZFC.)

The simplicity and efficiency of ZFC and the fact that T can be interpreted in it (i.e., that all the concepts of T have set-theoretic definitions which make all the axioms of T set-theoretically provable) have, as far as I can see, two main uses. One is philosophical: one doesn't need to understand the nature of all these different abstract entities; if one understands sets (philosophically) then one can explain all the rest. The other is in proofs of consistency and independence. To show that some problem, say in topology, can't be decided in current mathematics means to show it's independent of T. So you'd want to construct lots of models of T to get lots of independence results. But models of T are terribly complicated objects. So instead we construct models of ZFC, which are not so bad, and we rely on the interpretation to convert them into models of T. And usually we don't mention T at all and just identify ZFC with "current mathematics" via the interpretation.

Answer by S. Carnahan for Set theories without "junk" theorems?

2012-03-13T09:33:53Z

Many of these answers are quite satisfying, but I'd just like to emphasize that much of the confusion may come from overloading of symbols like "$\in$", "$\subset$", "$\cap$", and "$2$", that is, such symbols have multiple context-dependent meanings. In particular, the junk theorems you provide are situations where some kind of overloading has been misinterpreted - indeed, the validity of the theorems may change if you switch to viewing the natural numbers as complex numbers.

The overloading of symbols is useful, because many algebraic and geometric structures like rings and manifolds admit a notion of "underlying set", but we should be careful not to confuse the $\subset$ attached to manifolds-as-we-use-them with the $\subset$ attached to a chosen pure set-theoretic encoding of manifolds. For example, the intersection of submanifolds is likely to look quite complicated once we choose a method to unfold such an operation into a pure set-theoretic formula.

Another way to view junk theorems is to say that they are statements that depend on a non-canonical choice of encoding of mathematical objects as pure sets. This is not to be interpreted as a claim that I know a way to sort out the foundations attached to notions like "non-canonical choice of encoding".