## September 29th, 2005

### (no subject)

So this problem I've been hacking on lately is kind of the epitome of what I like about mathematics; that a thing can be proved in the literature one way, proved by a colleague another way, proved by yourself a third way, and yet there is still another significantly different proof idea that promises to explain still more interesting things about what's going on with the connection between letcc-like control flow on the one hand, and the gap between intuitionistic and classical logic on the other. And this is only one little corner of what seems to be going on with "labelled" presentations of judgmental logics; I think they may nicely subsume modal logics in the style of both Alex Simpson and Pfenning/Davies, the logic of bunched implications, and resource logics in the vein of linear logic (including affine and strict implication as special cases).

Anyway the "little corner" is Yet Another Proof that Gödel's modal interpretation of intuitionistic logic into classical logic is correct. This one works in three steps:

LMCSC → LND+letcc → LND → ND

• LMCSC is the labelled multiple conclusion sequent calculus that embodies Gödel's translation.
• LND+letcc is a labelled natural deduction system that has a letcc construct that is required to obey a certain label discipline: you are only allowed to throw data at world p to a continuation at world q if "q is an accessible world from p" ("q is in the future of p")
• LND is the same labelled system only without letcc at all.
• ND is ordinary natural deduction

LND → ND is the easiest part; the presence of labels in the rules can only make things harder to prove. If you erase all the labels in the rules in LND, you get the rules in ND.

LMCSC → LND+letcc is the next easiest. It's a routine exercise in programming classical reasoning with letcc. One caveat is that you can't pull quite all the same tricks that can that essentially constitute Glivenko's theorem, and let you put only one letcc all the way on the outside. For some reason the label discipline prohibits those; I'm still not sure why. Anyway, it's not too bad.

LND+letcc → LND is the hard part: getting rid of all the letccs and throws. I think as of this afternoon, however that it might really work. Disjunction was my final worry. I've had everything worked out for every other basic connective (implication, conjunction, truth, and even falsehood) for a few days now, but disjunction is a total pain in the ass. If you have a lambda that has within its body a pile of nested case expressions, it looks like it may be necessary to commute up above the lambda those (and only those) case expressions that analyze an expression in which x does not occur free. Ugh ugh ugh.

### (no subject)

Having read "Anatomy of a Typeface" and now also reading Bartman's "Five hundred years of book design" got me a bit obsessed with oldstyle (i.e. italian humanist) typefaces. I started trying to make one a few days ago. I've just sketched a few letters so far; maybe I could claim the b came out okay, but even its counter is too wide, I think. The "a" is terrifically hard, but surprisingly interesting.

The letter "a" at about the transitional period (e.g. Baskerville) and later isn't too exciting. It seems rather fluid all around, and has a decently-sized counter. But oh, the old-style "a"! All sturdy and angular and with a bigger space between the bowl and ear. I went down two fairly different roads looking for a good one, and neither (that is, neither "a" number 5 or number 10) matches my reference models or my other letters too well. #10 is getting towards there, though. I finally, through pure-line sketching, stumbled on how to get the bowl more flat and angular, and at the same time not look like total shit. The character as a whole may be a bit too narrow now, however. #5 is pretty much crap as far as my goals are concerned, but I'm fond of it as a standalone letter.
)
I'm astonished how much subtlety there is in "ordinary" roman letterforms. Doing more decorative/sketchy/crazy fonts is fun, but this is a fascinating challenge, worlds harder already than anything I've tried before typographically.

Slavkappen was my biggest previous attempt at being "serious" and trying to make something really aesthetically tight, but I didn't take departure from any particular reference face as a failing. Also I don't see blackletter day-in day-out, so if it's not quite right, I wouldn't notice anyway.

Nelf was vaguely like the sort of revival I'm attempting now; constructed almost as if I had found 16th-century printed samples of tom7's Hockey is Lif all rough and rugged on handmade paper and wanted to reconstruct the "ideal" forms expressed therein. Except for some reason it didn't seem so maddeningly hard. I guess monotone sans-serifs give you much less wiggle room --- I just had to eyeball the width and the general shape of things, and at least the resulting font would hang together reasonably well. The bare concept of contrast in roman fonts --- never mind serifs and all the thickness and bracketing choices that come with them --- is a source of enormous subtlety and difficulty, especially the diagonal stress of the aldine-era forms.