On the physical interpretation of sets

Physicality and pedagogy

A few years ago i introduced my twelve year old daughter to the theory of sets. The approach that i took was to make the interpretation as physical as possible. That is to say, we developed a notion of sets as physical containers. This leads naturally to the question of what is contained in those containers. If the answer is that containers are also contained, and one simultaneously maintains the axiom of extensionality -- that sets are equal if they have the same members -- then there is a problem. This is because it is easy to construct sets where the same container appears in two distinct locations. The Von Neumann representations of the natural numbers gives an example at the representation of 2.

Recall that the Von Neuman numeral is defined by the relation

V[n] = { V[n-1],...,V[0] }

so that we can calculate

V[0] = {}
V[1] = { V[0] } = { {} }
V[2] = { V[1], V[0] } = { { {} } , {} }
...

Notice that in V[2], V[0] shows up in two clearly distinct locations -- inside V[2] and inside V[1] which is also inside V[2]. It is easy to check that V[0], i.e. {} a.k.a. the empty set, has the same elements as the empty set. So, it really is the same container showing up in two distinct locations. This breaks our physical intuitions. Even quantum mechanics doesn't have the same physical object showing up simultaneously in two different places.

Our solution was simple. We decided that sets don't contain sets they contain 'pointers'. We thought of pointers as little slips of paper on which was written an identifier for the set. The set could be redeemed by going with the slip of paper to an authority. This solution allowed us to define all the usual operations like subset, intersection, union and the like. We could do arithmetic with the Von Neumann numerals.

Later, i thought about how this idea might be made explicit in set theory. This line of thought led to a series of developments.

Representing set theories

What i wanted first of all was a methodology for reasoning about set theories. It occurred to me that i could use domain equations -- with EBNF serving as a compact notation for writing such equations -- to write down a recipe for generating the universe of sets. In this formulation we have a very simple equation to capture all the basic universe of a (finite-image version of) the Zermelo-Fraenkel theory of sets

Set ::= { Set* }

This says that a Set is a container bracketed by '{' and '}' containing zero or more Sets. Clearly, this grammar generates {} and { {} } and { {}, { {} } } and all the Von Neumann numerals and many others besides. It automatically respects the foundation axiom; that is, the element-of relation always bottoms out. It won't give infinitely wide sets, either. This can be addressed in a number of ways, but as the short-coming is not really relevant for this discussion i won't mention them, here.

Set theories with quotation

Now, using our methodology how can we modify this basic universe to introduce 'pointers' or 'references'? Here is a simple grammar that does the job.

Set ::= { Quote* }
Quote ::= `Set+'

Like the previous grammar it indicates that a Set is a container bracketed by '{' and '}'. But, unlike the previous grammar it indicates that the containers contain Quotes, not Sets. It goes on the inform us that Quotes are kinds of containers, too. They can contain zero or one Set. Examples of such sets include {}, { `{}' }, { `{ `{}' }' }, { `{}', `{ `{}' }' }, ....

This allows us to build the sort of set theory that my daughter and i were using in our investigations. But, is there anything else of value here?

Sets, quotes and games

One of the first things i observed about this theory is that it has a curious correspondence with games semantics. In particular, we can make the following correspondence.

Opponent question <--> {
Player answer <--> }
Player question <--> `
Opponent answer <--> '

Under this correspondence we have that Sets are winning strategies for opponent while Quotes are winning strategies for player.

Sets, quotes and atoms

Recently, a lot of attention in the programming language semantics community has been focused on set theories with atoms, i.e. set theories in which there are fundamental entities, apart from the empty set, out of which to build sets. One such theory, FM-theory (that's Fraenkel-Mostowski theory), has been used by Gabbay and Pitts and others to great effect (See this paper, for example.). i observe that having 'atom-builders', in the form of quotes, enables accounts of freshness without sacrificing the 'closedness' of ZF set theory. That is, one can still build the universe out of nothing without having to introduce unexplained atoms. In yet other words, the theory is not predicated on a theory of atoms.

Sets, quotes and barbers

In a famous variation of his paradoxical construction, Bertrand Russell described a town in Italy in which the one and only barber (a man himself) shaves exactly those men who do not shave themselves. The question is: who shaves the barber? Since, under these conditions, it is apparent that the barber shaves himself if and only if he does not shave himself, the answer would seem to be that there is no such town.

Of course, this is a whimsical version of the paradox of all the sets that do not contain themselves. Like the barber, there is something strange about this set in that it contains itself if and only if it doesn't contain itself, making us loathe to admit it. There are a number of ways out of the Russellian situation, one of which is to carefully contrain the language of the comprehension defining the set. Notice, that in set theory with quotes you can't form this set because sets do not contain sets! Sets contain pointers.

In fact, it turns out that the key step of a lot of diagonalization-style arguments (from a version of Turing's halting problem to a version of the Cantor construction) become localized to the manner in which quotes are dereferenced. There is no way out of these constructions if the reference/de-reference mechanism provides a certain level of expressiveness. But, localizing the issue to one mechanism seems to have practical benefits.

Now, if you compare these ideas to the footnote at the bottom of the previous entry you will see that we are building toward something.