As to my own proof-effort abstraction-introduction-disjunction-eli
Whoa, scratch that. The crazy idea I had earlier today before leaving for dinner --- a peculiar technical conjecture that I came up with and tossed aside as apparently irrelevant, which seems by the way to have something to do with the kind of intrinsically multiple-argument functions that you might expect to arise in a focussing system for intuitionistic logic --- looks like it might be the final puzzle piece left after all. If it still holds up in the harsh light of morning tomorrow, I will be a very happy theory-wanker. Doing math is not really like doing a jigsaw puzzle, though, since ordinarily if you have exactly one piece left, it is the easiest piece to place. Maybe it would be fair to say that doing math is like doing a puzzle where all the pieces are scattered around the house, and you have to find them before even approaching the task of putting them together. Also, the pieces are preferentially hidden in the hardest places. You know, back of the refrigerator, or in the couch-cracks, or below some boxes in the basement closet you hardly ever open because, ew, spiders. Furthermore, the pieces may in fact be hidden outside your house entirely or, if you are especially unlucky, on the moon. Or, in the sad case that your pet theorem is false, they may have never been manufactured in the first place.
Other things I did today: One, music with heather. Kind of spotty today, but there were some very good moments, and "Now That You're a Ghost" came off much better than I remembered it being the last time we played it, which was quite a while ago.
Two, hung out with neal before the movie a bit. I bought during this time a Dover book full of Art Nouveau doo-whiddleys and borders and things. God bless the Dover publishing company. I love their crappy little public domain clip-artesque art books, not to mention all the math they reprint.