Ars Mathematica

This is a test post to see what’s involved in uploading images.

This is of course the Sierpinski carpet. What’s interesting to me is that many objects that, in a previous age dominated by a picture of the physical world as a continuum, seemed deeply pathological, have straightforward computer-language descriptions. For example, you can check whether or not a point in the plane is on the Sierpinksi plane by looking at the ternary expansion of its coordinates, which is a couple of lines of computer code. From the point of view of the computer, the Sierpinksi carpet is not much more complicated than a parabola. I suspect that the popularity of fractals marks a change in the popular imagination of the dominant metaphor for mathematics, from mathematics as mechanics to mathematics as computer program.

While thin on details, I found the article A new efficient algorithm for computing Gröbner basis intriguing. While a naive implementation of Gröbner bases is easy to come by, as a practical algorithm it is highly sensitive to the order in which you add new polynomials to the basis. This has given rise to a whole literature on strategies to add new polynomials. In the paper, Faugere seems to suggest that the whole question can be bypassed, and that polynomials can be added to the basis in bulk by using sparse linear algebra techniques.

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.

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.