Got woken up this morning around 7 by the phone ringing. Someone from Panera trying to get Tom (Russo) to come in early. Having regained consciousness, I found myself thinking frantically about various mathy things. Beat my head against the MELL-decidability wall some more. I thought I saw a glimmer of hope of connecting the undecidability of reachability sets of petri nets to this binary VAS gadget I came up with, but I tried that long ago, and it's not working now, either. Thought a little about the "all the connectives" project - no concrete insights yet, but I'm feeling interested in the approach, still, despite the total lack of clue as to how I would get a negative result. Finally started sketching out Tom7's idea of a "classically true" modality on the whiteboard. I think it might actually work. If everything does work, it will be extremely clean: the rules and cut principles divide themselves neatly into classical and intuitionistic, and the modality is the sole bridge between them. Frank's claim that it's really implication that matters is corroborated by the fact assumptions of conjunctions and disjunctions can be always written with a parametrized truth-mode.