Fixing intensional logic

One of my favorite hobbies is reading about intensional logic. This refers to any form of logic that allows us to refer somehow to the "sense" of a logical entity, in addition to the extension. I have never contributed any of my own research to this topic, but I believe that we can never have a useful computational theory of natural semantics without some kind of decent intensional logic.

It seems like every proposed form of intensional logic through the years has got something wrong with it. Quite a bit of recent literature is still devoted to the seemingly endless task of "fixing" some variety of intensional logic.

As far as I can see, there are two dichotomies that can help classify various approaches to intensional logic. You can do things with type theory, or without it. You can do things with possible worlds, or without them. I have already posted about my dislike for possible worlds. In fact, I doubt there is a possible world in which I like them! But kidding aside, for a working intensional logic I favor Church's formalization of Frege, the Logic of Sense and Denotation---type theory, but no worlds. This logic was published in several incarnations over many decades. In fact, Church's own publications on the subject span from 1946 to 1993! This might qualify as the longest period spent by one scholar publishing papers on something that remained unsatisfactory, even to the scholar himself. I certainly hope to spend 47 years publishing, pretty well anything, if you want to know the truth.

But there is hope for Church's method, apparently. Quite a few scholars followed up on Church's flawed logic in the past decade (including some leading names like Terence Parsons), and the most recent entry in the game to fix Church is a paper by Kevin Klement in the June issue of the Bulletin of Symbolic Logic. I'll fill in the details in another post in the near future, but I direct your attention to Klement's fine paper in the meantime.