fxn: I haven't gotten the chance to look at Brian Ford's paper, but it sure is intriguing.
If indeed ZF comes crashing down, that would really validate my decision to make proofs in Ghilbert truly portable with respect to axioms, rather than trying to pick a single axiom system that is both powerful enough for the work at hand, but not so powerful as to raise questions about soundness, or raise problems porting the proofs over to other systems.
That said, the timing could have been a little better for me; as a demonstration of Ghilbert's portability, I picked a construction of HOL logic in ZF[C] set theory, and it's only a few proofs away from being done (of the core HOL axioms, I have only the law of the excluded middle (BOOL_CASES) and a theorem to introduce the iota operator). Oh well.
It has been a busy month since the last time I blogged. Among other things, we had an Artifex staff meeting, and also tor stayed for a couple of weeks. We had a great time talking serious 2D graphics, color, and so on, plus hanging out with the family.
I'm proud of a couple photos I took on Alan's 8th birthday; the portrait of him, and another of the brothers posing with a penguin prop. Both were taken with my archaic Rapid Omega 100 on slow B/W film (6x7cm), then scanned on my brand new Epson 4870 scanner (highly recommended, btw).
Alan's photo page has unbelievably high Google-juice - looking at the referer logs, the most popular images are the ones that currently show up as #1 and #2 for a Google image search on happy. Even more exciting, a photo from last year of him playing his guitar is now on the cover of a book recently published by Wesleyan University Press.
Max, who just turned four last week, is developing quite a subtle sense of humor. A few weeks ago, when I was reading him Eating the alphabet, he asked if I would get him a Xigua melon. I answered that I didn't remember ever seeing one in a store, but that if I did see one, I'd get it for him, then we'd be able to tell if it's as good as a watermelon, or better (watermelon is one of Max's absolute favorites right now). Max replied that he knew that Xiguas are way better than watermelon. I asked him how he knew that, and he said: I can see inside people's minds. Even fruit. And that Xigua melon is thinking, "I'm way better than a watermelon".
"More later" is one of Josh Marshall's favorite catchphrases, and people rib him for it. I've been doing quite a bit of deep thinking lately about the place of free software in the world, among other things, and I do want to write about it, but it will have to wait until I have a bit more time.