# Does negation of Axiom of Choice imply symmetry?

It seems that every construction of a model in which the Axiom of Choice fails involves some kind of symmetry. Is there an example of a construction of a model where AC fails but no argument involving symmetry appears? Is there any result that connects the negation of choice (any kind of choice) to some kind of symmetry?

-
I find "some kind of symmetry" a bit vague. –  Hagen von Eitzen Dec 8 '12 at 18:52
@Hagen: It's not vague at all. Permutation models; symmetric extensions; relative definability -- all those are essentially exploiting the existence of "somewhat indiscernable elements". –  Asaf Karagila Dec 8 '12 at 19:00
@Hagen: This is a philosophical thing, really, and I came to understand it in full while working on my masters thesis during the summer. The original idea uses atoms and permutations of them, and this translated into forcing and permutations of the generic sets. The reason it works is because atoms are completely indiscernible from one another; and generic sets are indiscernible enough over the ground model (i.e. from the point of view of the ground models the generic sets have the same properties and cannot be discerned). –  Asaf Karagila Dec 8 '12 at 19:07
[cont] and so permutations of these indiscernible sets ensure that nothing which can separate them from one another stays in the model, and so the axiom of choice fails (because well-orders can discern them, obviously... :-)) –  Asaf Karagila Dec 8 '12 at 19:08
@Zhen: Even when there is obvious symmetry in the construction of a model, it often disappears in the final result. For example, Cohen's original models for the failure of AC involved (in modern terms) a Boolean-valued universe invariant under Boolean automorphisms that arbitrarily permute a countable set of generic reals. But the 2-valued models obtained via a generic filter have no automorphisms except the identity. (If I remember correctly, Cohen later built 2-valued models that have nontrivial automorphisms, but this took some additional work.) –  Andreas Blass Dec 8 '12 at 21:59

## 2 Answers

We have a vague idea. First let me cover the historical background for symmetries.

First one should observe that we don't actually know how to generate models of set theory. Sure, under assumptions that those models exist we can generate more, but we can't really come up with them out of nowhere. This means that most ways to generate a model of ZF would require us to already have a model and then alter it using one way or another. If we want to have "nice" models (i.e. countable transitive models) then we have two major ways of obtaining them from already existing nice models -- inner models, and adding new sets (usually generic sets). Using symmetric extensions is to do both, first we add sets then we move to an inner model of the extension.

The idea of using symmetries goes back to Fraenkel, and was then incorporated into forcing by Cohen. This idea began with ZF+Atoms, and of course we cannot separate between the atoms without the axiom of choice (they all satisfy the same formulas), so by taking only things which are definable from a small set of atoms and are impervious to most of the permutations of the atoms (namely, a large set of permutations of the atoms will not change our object) we are removing anything which can separate between the atoms. In particular we ensure that they cannot be well-ordered.

Similar approach was taken by Cohen, and is the guiding idea behind symmetric extensions by forcing. We add generic sets that from the ground model have the same properties and cannot be discerned. While atoms satisfy virtually no formula; generic sets satisfy virtually every formula. But inseparability is still there so we can do a similar trick.

Lastly relative definability is also an option, but it was proved to be essentially equivalent to symmetric extensions (under reasonable conditions) by Griegoreff. I am saying essentially because we can generate relative definability models which are not symmetric extensions, but the idea is close enough that we can think of it as the same thing.

About two years ago several prominent set theorists met in Bristol and in a few days concocted a model which is not a symmetric extension and the axiom of choice fails there. Sadly, however, no one wrote the details. I hope to reconstruct their work sometime in the next couple of years. But until then I can't give more details because I don't really have them.

There is also a proof that if there are uncountably many measurable cardinals then Chang's model does not satisfy the axiom of choice. Chang's model is the model which is constructed when taking an $L$-like closure using an infinitary logic instead first-order logic.

While I don't know much (yet) about this process, I have been told that if we use an undefinable logic then its closure is unlikely to satisfy the axiom of choice. But I don't have too much to give about that yet, either. I should mention that this is one of the proposed topics for my Ph.D. dissertation, and I have yet to overrule it completely.

Of course sometime one can just assume that they live within a model without the axiom of choice. It is possible that this model is not a symmetric extension of any ground model, but this too is still quite an open end as far as I know. One could verify whether or not it is a symmetric extension of a set forcing (symmetries satisfy Blass' SVC) but not all class forcing symmetries do, so we can't really ensure that in the general case (if we wish to include class forcing based symmetries, that is).

All in all, I have a hard time to point out exact references and who would know to give better answers, but I have the feeling that there isn't too much that we can conclude with certainty.

-
What about the Martin-Steel-Woodin result that AD holds in $L ( \mathbb{R} )$ assuming infinitely many Woodins with a measurable above? (I am quite unfamiliar with all but the statement of this result.) –  Arthur Fischer Dec 8 '12 at 19:29
Of course, this is a pickle. I don't whether or not it is exactly a symmetric extension (furthermore Woodin cardinals are very very far from $L$ so it is surely not a generic extension of $L$ by any set forcing). But the idea of relative constructibility is essentially symmetries. –  Asaf Karagila Dec 8 '12 at 19:33
Now that I am thinking about it, it is possible that $L(\mathbb R)$ is a symmetric extension over some inner model of the form $L[A]$ in which there are infinitely many Woodins and a measurable above them (although I think we can replace the measurable with a sharp for some appropriate set, e.g. $V_{\delta+1}$ where $\delta$ is the limit of the Woodin cardinals). –  Asaf Karagila Dec 9 '12 at 11:42
The result that Arthur mentions was proved by showing that $L(\mathbb{R})$ elementarily embeds into the $L(\mathbb{R})$ of a generic ultrapower by the stationary tower, which in turn is equal to the $L(\mathbb{R})$ of a symmetric extension. The proof of AD using genericity iterations rather than the stationary tower (see Neeman's handbook article) also uses symmetric extensions. –  Trevor Wilson Dec 18 '12 at 22:51
@Trevor: Thanks for the information! I'll look it up. (although I have to admit that I am profoundly illiterate in those areas, and while I was planning to study them over the next year and choose a suitable question for my Ph.D. it seems that I will go another way after all... and pursue questions of my own wild imaginations which are dreadfully cool and whatnot...) –  Asaf Karagila Dec 18 '12 at 23:02

I have an example which is not symmetric, or at least not obviously so. It is a bit advanced, so I advice searching the literature for it.

In the effective topos, which is based on recursive realizability, there are surjective functions that do not have sections. In this topos, all morphisms $\mathbb N \to \mathbb N$ are recursive functions. Therefore, there is a set of algorithms for total functions $\mathbb T$ and a surjection $s:\mathbb T \to \mathbb N^{\mathbb N}$. This surjection cannot have a section for the following reason. We can recursively decide whether two algorithms are equal. An inverse of $s$ would allow us to decide the equality of functions, which is impossible.

-
Note that this is a model for higher order intuitionistic logic. If you need classical set theory, try Krivine's classical realizability models. –  Wouter Stekelenburg Dec 8 '12 at 20:22