My laptop broke again today, so posting will continue to be light. (This time, it’s the monitor.) Also, my car broke. Next, after I post this, a meteor will probably flatten my house.
Author Archives: Walt
Back
I was out of town for a couple of days. Regular posting should resume. (I was going to post beforehand to let you all know that I was going out of town, but then I thought “Who are you? My mom?”)
2007 Nobel Prize in Economics
I was looking at an interview with Roger Myerson, one of the three winners of the 2007 Nobel Prize in Economics (technically the Sveriges Riksbank Prize). Myerson says
How would my career have been different without John Nash? What a wonderful question! My difficulty in answering it is an indication of how influential he has been in everything that I have done. I wanted to be a mathematical social scientist since I was 12 years old, when I read Isaac Asimov’s science-fiction novel Foundation. But my concept of what kinds of mathematical models should be studied was completely transformed when I read Nash’s and Harsanyi’s papers in college.
BHK Interpretation
The BHK interpretation of intuitionistic logic articulates the sense in which intuitionistic logic captures constructive reasoning. Statements that involve logical connectives are interpreted as constructions that transform proofs of simpler statements into proofs of more complicated statements. The interpretation requires a primitive notion of what it means to give a construction function that turn objects and proofs into another proof.
Generally, the BHK interpretation is invoked as a piece of metamathematical reasoning, with the actual definition of a constructive function left to the particular theory under development. This puzzled me, since there is a natural notion of construction: one given by an arbitrary Turing machine. At first, I chalked it up to a philosophical unwillingness to accept the Church-Turing thesis, but I think I’ve identified the real problem: it doesn’t work.
For the BHK interpretation to work, Turing machines that represent constructions must be total functions. Worse, to satisfy the philosophical aim of constructivism, they must be provably total in a constructive system. But a simple diagonal argument shows that there exists total functions that are not provably total in any constructive system since we would expect the valid proofs in such a system to be recursively enumerable. You can simply identify constructions with those provably total in a specific system, but philosophically the diagonal argument is constructively valid: given any recursively enumerable axiomatization of valid constructions, I can give you an explicit construction that is different from every element of that enumeration, and for any given element an explicit proof that it’s different.
The way this issue is handled in the realizability interpretation (and therefore the effective topos) is by identifying the constructions as those functions that are provably total in Heyting arithmetic, the intuitionistic analogue of Peano arithmetic.
Now That’s Indirect
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.)
2007 Ig Nobel Prizes
The 2007 Ig Nobel prizes have been announced. I would say the most important discovery highlighted by the awards is that Viagra cures jetlag in hamsters. There’s nothing quite like a jetlagged hamster to ruin a fun-filled vacation.
Australian Models turn to Crime
As we all know, crime on the internet knows no national boundaries, as Scott Aaronson has learned. Australian fashion models have taken to stealing the contents of his quantum mechanics lectures in order to sell printers. Mark my words, next they’ll be using quantum mechanics to rob banks and assassinate major world leaders.
Parallel Parking at Rigorous Trivialities
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.
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.