Eliminate Cut Elimination

Sorry for the radio silence; I’ve been under the weather lately.

Is there any major theorem in mathematics drier than Gentzen’s cut elimination theorem. I feel guilty for picking on proof theory, since it is an undeservedly unfashionable area of mathematics (it’s probably better known by computer scientists than mathematicians at this point). I feel guilty for picking on the cut elimination theorem in particular, since it’s an important ingredient in the proof that Goodstein’s theorem is independent of Peano arithmetic, which is one of my favorite theorems. But, I had to read the statement of the theorem forty-nine times before I got what it was trying to say. I have yet to make it all the way through the proof before blacking out.

I was trying to think of a theorem in a more-fashionable area of mathematics that is particularly dry. The best I could come up with the Riemann-Roch theorem (for curves). I know what it says. I know what it’s good for. I just can’t bring myself to like it.

Category and Model Theory

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.

Shalizi on Econophysics

Cosma Shalizi has written a detailed posting on what’s wrong with econophysics. Econophysics is the application of certain ideas that have been influential in physics in recent years — power laws, phase transitions, nonlinear dynamics — to finance and economics. Econophysics articles are generally published in physics journals, and have not had much of an impact on economics as practiced in economics departments. If you love statistical mechanics, and you think it explains everything, then econophysics is the area for you.

Cosma also includes a section on what’s wrong with economics, because he intends on dying friendless and alone.

Axiom of Constructibility

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.

On the Persistence of Myths

This article from the Washington Post on the persistence of myths reports some of the most disturbing research about human psychology that I’ve ever heard of. The repetition of a statement makes it more likely that the hearer will believe it. That much is not surprising, but the result obtains even in the context of being told that the statement is false. The mind remembers the statement, but slowly forgets the context.

Insert your joke about the Axiom of Choice here.

Links on Constructive Set Theory and Realizability

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:

On realizability and the effective topos:

Cambridge mathematicians not yet wasting time completely

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.

Journal of K-Theory press release

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.

R6RS Scheme

A new revision of the standard for the Scheme programming language, the Revised6 Report on the Algorithmic Language Scheme, has been approved. The draft standard and other information can be found at r6rs.org.

The changes seem to be aimed at enhancing portability between implementations of Scheme. Opinions, both pro and con, can be gleaned from the online ratification process.