I had a bit of a blogging hiatus last week because I was fairly busy with some talks. In particular, I gave a talk to the math graduate students about the Fraenkel-Mostowski method of proving the independence of the Axiom of Choice from a slight weakening of Zermelo-Fraenkel set theory. Coincidentally, Sol Feferman was in town giving the Tarski Lectures, and the one that day was on a topic with some similarities, namely Tarski’s notion of a logical constant.

The question of which symbols count as logical is an important one in many characterizations of the notion of logical consequence, so after discussing his notion, Tarski started work on a characterization of the logical symbols. The idea he hit upon is phrased in terms of a sort of Russellian type-theory, but it could probably be equally well formulated in something more like ZF set theory. Basically, the idea is that we start with some domain of basic objects, and then form sets of these objects, and sets of those sets, and so on. Now, we consider any permutation of the basic objects, and see what effect these permutations have on sets of various levels. Tarski’s idea was that the ones that are fixed under all permutations are the sets that can be adequately denoted by a logical symbol. For instance, the identity relation (consisting of all ordered pairs of a basic object and itself) is fixed under every permutation, as is its negation, the trivial relation that holds between no objects, and the relation that holds between any two objects. At a level one step higher, the sets of sets that are fixed include the set of all non-empty sets (which corresponds to the existential quantifier), the set consisting of just the empty set (which corresponds to the negated universal quantifier), the set consisting of all sets of cardinality k (which corresponds to a cardinality quantifier), and so on. So it seems like a pretty good match for the intuitive notion. Feferman went on to point out that this idea was further developed by a variety of people over later decades, and notably Vann McGee who advocated a slightly different characterization.

The Fraenkel-Mostowski method actually works fairly similarly. We start with a collection of basic objects (“urelements”) and construct a hierarchy of sets above them. The existence of urelements is a slight weakening of standard ZF set theory, which only allows a single object with no elements, namely the empty set. Thus, this theory is called ZFU. If we start with a model of ZFU with infinitely many urelements, then we can construct a model of ZFU that falsifies choice fairly easily. Basically, we consider all the permutations, and take just the sets that are fixed under “most” permutations, rather than the sets fixed under all of them, like in Tarski’s idea for the purely logical notions. To measure what “most” means, we say that a set is fixed by most permutations if we can choose finitely many urelements, such that any permutation fixing all of them also fixes the set in question. Of course, the finitely many urelements to be fixed will in general be different for each set in this class, which I will call “FB”, for the sets with “finite basis”.

It is straightforward to see that in FB, every set containing just urelements is either finite, or it contains all but finitely many urelements. But since the set of urelements is infinite, this is a violation of the Axiom of Choice, which is what we want. However, FB isn’t quite a model of ZFU – for instance, it includes the full powerset of the set of urelements, even though there may be sets of urelements that are not included among the sets with a finite basis. We want our model to be transitive – that is, any element of a set in the model is itself in the model. This condition is very useful for verifying the axioms of Extensionality and Foundation. So we define HFB (for “hereditarily FB”) to be the sets in FB whose elements are all in HFB – this is a recursive characterization of HFB that basically guarantee that its elements are in FB, as are their elements, and their elements, and so on. It doesn’t take too much work to prove that HFB is a model of ZFU (the hard axioms to check are powerset and replacement – some lemmas to use are the fact that any formula satisfied by a sequence of sets is also satisfied by their images under any permutation, and that a permutation applied to a set of finite basis gives another set with finite basis).

Thus, a very similar method gives Tarski’s account of the logical constants, and also a proof of the independence of Choice! Of course, both needed to be updated to deal with trouble cases, but it’s interesting to see that a similar start gives rise to two seemingly unrelated results.

Russell O'Connor(00:59:19) :Andrew Pitts has been championing nominal logic as a practical way of handling variable binding (in data structures such as functions, quantifiers, integrals, whatever). Basically the variable names are the atoms (or urelements) of the FM-sets. α-equivalence is enforced by requiring everything to be invariant under permutations of the atoms. There is even an implementation of this in a language called FreshML.