There is a discussion at the Everything Seminar about everyone’s favorite topic, the axiom of choice. The axiom of choice has various pathological consequences, such as the Banach-Tarski paradox and the existence of a non-Lebesgue-measurable set. The problem, everyone notes, is that by its very nature constructions that depend on the axiom of choice cannot be given explicitly. It’s tempting to dismiss the axiom of choice on those grounds as illegitimate (as Lebesgue himself did).

This philosophy can be taken further. What if we restrict ourselves to sets we can construct explicitly? One answer leads to constructivism, which entails rejecting many other basic principles of mathematics, such as the law of excluded middle, and has a dramatic impact on how every branch of mathematics is developed. A less dramatic course of action was proposed by Gödel: the axiom of constructibility. Gödel analyzed the types of sets that you can construct from a given collection of sets in terms of nine explicitly-given functions (these are familiar operations such as taking the direct product of two sets, or taking the image of a function between two sets). Gödel then defined a universe of sets in stages. At each stage, the sets defined by repeatedly applying the operations to the sets from the previous stage. He then iterated the construction of stages (allowing the stages to indexed by ordinals) to build the constructible universe. Any explicitly given set will appear somewhere in the constructible universe. The axiom of constructibility is that every set is in the constructible universe.

What happens to the axiom of choice under the axiom? It becomes a theorem. Even more amazingly, you can define a single well-ordering over the entire universe of sets. Choice functions can be found using the well-ordering. You can even define the well-ordering reasonably explicitly: at each stage, you define each new set in terms of a finite number of the nine operations on the old sets, so to order the sets at each stage you just need to define an order on the operations. You extend this to the whole universe by defining sets that first appear at later stages to be bigger than sets from earlier stages. To find an example of a non-measurable set, or the paradoxical decomposition in the Banach-Tarski paradox, you can just take the first one under the well-ordering.

I was doing some web searches to see if I could answer Todd Trimble’s questions here. As usual, instead of answers I found more papers to read and no time to read them.

On constructive set theory:

• Notes on Constructive Set Theory by Peter Aczel and Michael Rathjen. Aczel is the inventor of CZF, a constructive analogue of ZF.
• Programming in Martin-Löf’s Type Theory by Bengt Nordström, Kent Petersson, and Jan M. Smith. Martin-Löf’s Type Theory is apparently one of the few theories that is uncontroversially constructive.
• Predicative topos theory and models for constructive set theory by Benno van den Berg. This is a Ph.D. thesis that tries to weaken the notion of topos appropriately.

On realizability and the effective topos:

• Realizability: A Historical Essay by Jaap van Oosten.
• Categorical Models of Constructive Logic by Thomas Streicher.

I came across this weird story by Ben Goldacre at a site called Bad Science. The Daily Telegraph (a British newspaper) printed a story that claimed that a team of Cambridge mathematicians had shown that actress Jessica Alba had the sexiest walk. The simplest explanation would be that a Telegraph reporter was hanging out at a bar frequented by Cambridge mathematicians who announced, five pints into the evening, that the sexiness of Alba’s walk was objective fact.

The actual story is much more bizarre. A PR firm, as a small piece of a larger marketing strategy, wanted to produce scientific-sounding research that proved that curvier women were sexier than skinny women. They hunted around for someone who would produce the desired result, apparently without much success. They did find a single Cambridge mathematician to analyze survey data for them. When that didn’t result in the correct answer, they simply made up the result they wanted and reported that in a press release. A press release that the Telegraph reported as fact.

If you had that kind of power to feed drivel to newspapers and get it printed, why would you waste it on something as banal as Jessica Alba, sex symbol? Why not Wallace Shawn, sex symbol? Why not: Cambridge mathematicians discover that thanks to years of children not brushing their teeth three times a day, the world is going to end next Tuesday? It’s time that public relations stop being about the money, and start being about the artistry.

The editorial board of the new Journal of K-Theory has put out a press release announcing the formation of the new journal. The journal will be published by Cambridge University Press. It will initially be owned by a private company, but ownership will be transferred to a non-profit foundation by 2009.

The press release also addresses the now-notorious backlog. Authors who had originally submitted to K-Theory can choose to have their manuscript remain at the new journal, or submit to another journal entirely.

The text of the press release was posted by AC at Noncommutative Geometry.

Here’s something that I just learned: a topos, despite the fact it can model intuitionistic logic is not quite the right setting for a constructive set theory. The reason is that in a topos every function has an image. In a constructive set theory, the only sets whose existence you want to assert is those whose membership functions are explicitly computable. The image of a function between two infinite sets may not be explicitly computable.

(I think the correct analogue for constructive set theory is something called a quasitopos, but I don’t know much about them.)