The 7.31 beta candidate tarballs are up. Please give them a shot.

I was hoping to get subpixel text antialiasing in this release, but didn't quite manage. Hopefully next time.

Proofs

I got some very nice email from Robert Solovay, answering many of my questions about second-order arithmetic.

I'm starting to get a handle on definitions. All proof systems have a mechanism for them, but mathematically they tend to be not very interesting, so mathematicians don't talk about them much. Even so, they're clearly important.

In general, definitions create a mapping from a source language to a target language, mostly by expanding out rewrites of the form <symbol> = <expansion>. The target language has just the axioms of the underlying system, like ZFC set theory or Z_2 arithmetic. So the concept of truth or provability is basically the same between the two languages: a statement in the source language is provable iff its expansion is provable in the target language.

So now the important thing is to make sure that there are usable inference rules in the source language. Ideally, all the inference rules that work in the target language are also sound in the source. But this doesn't necessarily have to be the case. For example, if you define the expansion of, say, y = 1/x to be x * y = 1, then you have 1/0 not equal to anything. This is cool in a way, but you have to use somewhat different axioms for equality.

Partiality is of course a big issue here. Joe Hurd recommended this paper on how to get partial effects in a total logic such as HOL. A different approach is Jan Kuper's quite readable thesis, which gave me the courage to consider tweaking the equality axioms in the source language so that you can write terms that don't exist. Also see Freek Wiedijk's First order logic with domain conditions.

There is one way in which definitions may be interesting: as a means of making proofs portable to different axiomatizations. The idea is that a module of definitions has an interface that exports proved theorems, but might keep certain details private. A good example is pairing. Your theorems basically say that you get out what you put in, and are the same in Z_2, HOL, and ZFC, but the actual construction (hidden) is quite different. When you plug in a different definition module with the same interface, you still expect your proofs to go through.

I'm not sure about the mathematical consequences of this approach. I get a feeling that it won't work in all cases, but if it works in all non-contrived ones, that's good enough. It's also entirely possible I'm reinventing category theory, in which case I better break down and get a book on it. I got a nice email from Sarah Mount recommending a few, as well as this paper updating Reynolds' result that polymorphism is not set-theoretic.

The feedback and intellectual excitement I'm getting from my exploration into proof systems is turning out to be quite addictive!