For a bit of light bedtime reading, I'm going through Raymond Smullyan's book First-Order Logic. It's a proper math book, not one of his popular fantasias like The Lady or the Tiger, and it was first published in 1968.

One of the things that strikes me is how mired in mechanics it is. He defines propositional formulae, as you might expect, as formed from variables, negations, and parenthesized binary connectives, and then he is at pains to point out that every proposition uniquely decomposes as either a variable, a negation, or a parenthesized binary connective. He cites proofs from Church and Kleene.

I spent ages going back and forth trying to decide what the difference between the definition and the lemma was, or to see what the supposed proof obligation was here.

Finally it dawned on me that he sees his formulae as essentially strings of symbols, rather than terms per se, and so the "uniqueness of decomposition" was essentially saying that there is a unique way to parse these symbol-strings as terms. To my modern eyes, it never occurred to me that the definition itself would be interpreted as anything but a definition about terms, or trees.

He goes on to note that, whereas his definition provided for connectives formed as, for example, (X /\ Y), they could have been defined as (X) /\ (Y). Three pages are spent on all this fuss over parentheses, and the equivalence between their different placements! When I didn't even see the parentheses as objects in the first placeâ€”they were just notation. How times have changed, for the better.

Yeah, logicians didn't know about abstract syntax. At least not back in the day.

Dave

Weird, though. Algebraists would have known about it, right?

I guess this was a few years before category theory started unifying the two areas . . .

Oh, Hi Dave! I heard you were in town recently. How goes Rust?

I'm not sure anyone knew (knows) about category theory. ;)

Rust is going great! I gave a talk about it at NU this past week, and it seemed to be well received. My talk was tailored for the NU audience, and contained many musings that are subject to change, so I won't be posting the slides online. But I'm hoping that we'll make more of a concerted effort to blog about it.

I also had dinner with your colleague Richard, although I didn't get a chance to say hi to David (your other colleague I'm friends with). Hope you're enjoying the new job!

Dave