bytesplit: I mean you no ill will. However, by now it has become painfully clear that you and Advogato are not a good match for each other. I ask of you, please find another place for your writings.

Thinkpad 600 battery

Heather's got the 600 now. Yet another battery was tanking - the useful life was down to about 10 minutes. So I tried a technique suggested by Javier Valero, and so far it seems to work.

I've put up a page summarizing the ThinkPad 600 battery problem and possible solutions.

Proofs

I have lots more feedback than I can digest right now. But I will point out Robert Solovay's interesting reference to two flavors of second-order arithmetic. One is the "pure" Z_2 axiomatization with naturals, predicates over naturals (or functions from naturals to bool, if you prefer), and quantifiers over both. The other, with equivalent strength, has functions from naturals to naturals. The latter is probably a lot more directly useful for what I'm trying to do, because new functions can be defined as plain old lambda terms, and application is primitive, i.e. requires no hoops to be jumped through.

I'm more than a bit intrigued, though. Since these systems are indeed equivalent in logical strength, but differ widely in the convenience of their definitional systems, it's clear that choice of definitional framework is very important. How carefully has this space been mapped out, though? Is it possible that there are other definitional tricks that could make the systems even more usable, or is macro expansion plus function definition and application somehow complete in that all other definitional frameworks can be reduced to it tightly?

I'm not sure what such things might look like, but I see glimmerings. For one, I'd imagine that statements of the form "abstract tree S is a parse of string S by grammar G" might be easier to express and prove than in the usual logics. In any case, these statements are exactly the kind of thing I'd expect to be primitive in a human-friendly "source language", and then compiled automatically to a proof "object code", so maybe in the end it doesn't much matter.

Paul Snively has been blogging about proofs as well. I've skimmed his references, but so far am not sure how relevant they are.