Definability of identity in higher-order languages

Thanks to the long weekend I finally found some time to write up a first draft of a paper that I've meant to write for quite a while. (I know, spending the long weekend doing research is a tad pathetic and geeky, but I really wouldn't have time to do this some other time). It's about a thing that seems to have been settled - the definability of identity. Below is the abstract. The full version of the paper is here.

It is a commonplace remark that the identity relation, even though not expressible in a first-order language without identity with classical set-theoretic semantics, can be defined in a language without identity, as soon as we admit second-order, set-theoretically interpreted quantifiers binding predicate variables that range over all subsets of the domain. However, there are fairly simple and intuitive higher-order languages with set-theoretic semantics (where the variables range over all subsets of the domain) in which the identity relation is not definable. The point is that the definability of identity in higher-order languages not only depends on what variables range over, but also is sensitive to how predication is construed.


TXLogic said…
Can you provide (or provide a link to) an example of one of these (genuinely) higher-order languages in which identity is not definable? Thanks!
TXLogic said…
Just a followup so I will be notified if/when you reply. (I forgot to check the "follow-up" box in my previous post.)
Rafal Urbaniak said…

Just follow the link to the full paper, it's not too long, just a few pages. The idea is quite simple (btw, it's been accepted and is forthcoming in the Australasian Journal of Logic).