In Chang and Keisler’s Model Theory, they give one of the most indirect proofs I’ve ever seen. They prove a theorem assuming the continuum hypothesis, and then they prove a metatheorem that any theorem of that particular form proven using the continuum hypothesis must also have a different proof that does not use the continuum hypothesis. They don’t actually exhibit this proof — they just prove that it exists. (The theorem shows that a theory preserves reduced products if and only if it can be defined entirely in terms of Horn sentences.)

At Rigorous Trivialities, a relatively new math weblog, there is a post that is an early contender for the title of Most Important Blog Post of All Time. It’s a sketch of a rigorous proof that parallel parking is always possible (assuming the space is longer than your car). So if you can’t fit your car in that space, it’s your fault. Mathematics demonstrates its practical usefulness once again.

The post’s argument relies on an appeal to Lie algebras. If you take infinitesimal versions of the two basic motions of a car — turning the steering wheel and going forward — these generate a Lie algebra. Contained in the Lie algebra is the vector field that corresponds to going sideways. This implies that you can parallel park any car if you can switch between going forward and turning rapidly enough.

I was reading Eric Schechter’s Handbook of Analysis and its Foundations when I had a small epiphany about (of all things) the relationship between model theory and category theory. In contrast to universal algebra, the concept of homomorphism is not very important in model theory. A model is a very rigid object. From the point of view of algebra, a free group (for example) is a very flexible object with many homomorphic images. From the point of view of model theory, the free group comes bundled with every theorem that it satisfies, and that includes the statements that every element is different from the identity. The only map that preserves these statements is an embedding into a larger group. The problem is that for every model, every possible statement is either true or false (this means the set of theorems about the free group, or any model, is a complete theory).

What we want to get the analogue of a homomorphic image is to somehow forget those inequality statements. In model theory terms, we want to work with an incomplete theory rather than a complete theory. This is easy to do, and in fact, many naturally-arising theories are incomplete, but this does not guarantee a rich supply of homomorphisms. If a theory is equationally presented (all of its axioms can be put in the form of equalities) such as that of groups or rings, then homomorphisms are easy to come by. But in general, the only types of homomorphisms that exist are embeddings. The theory of fields is typical.

There is a more indirect way to create incomplete theories: boolean-valued models. To force statements to be neither definitely true nor definitely false, we assign intermediate truth values in a Boolean algebra with more than two elements. Despite their exotic logic, these are easy to construct. For example, the set of functions from a set I into a field F is not itself a field, but it forms a boolean-valued model. The truth value of a logical statement becomes the set of elements of I for which the statement holds. A statement is true if it holds for all of I and false if it holds for none of I. Boolean-valued models have lots of homomorphisms.

Several standard constructions can be interpreted in terms of boolean-valued models. The ultraproduct, which creates models in the ordinary sense, not boolean-valued models, works by creating a boolean-valued model and then taking a maximal quotient. (Nonstandard analysis can constructed using an ultraproduct.) Set-theoretic forcing can also be interpreted in terms of boolean-valued models. In turn, boolean-valued models can considered as a special case of sheaf semantics.

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

Like most people in mathematics, you are probably a devotee of astrology. If you are also a Scorpio, you’re in luck, since this is your horoscope according to the Onion:

Love means different things to different people, but you’re the only one for whom it means that to every w-consistent class K of formula there correspond recursive class-sign r (on free var. v), such that neither (v Gen r) nor ~(v Gen r) belong to Flg (K).

Via Computational Complexity.