Working on the section of my thesis proposal about crazy things I'd like to do with ordered logic, I took the chance to go back and skim Lambek's 1958 paper "The Mathematics of Sentence Structure" (Amer. Math. Monthly 65(3):154-170) which is just frightfully cute. I mean, what else do you call precociously proving the decidability of entailment for an intuitionistic substructural logic via cut elimination like forty years before everyone else realizes it's cool?