Illative Combinatory Logic

I've been reading the paper "Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus" after looking over posts on an awesome blog: http://lukepalmer.wordpress.com/, and I have to say its pretty cool. It took a while for me to understand even the simplest notions of these systems, but the paper is a good one and the discussions on the blog show examples of inference and interpretations in this logic. For reference, I wanted to record some of the things I've learned even though I haven't finished the paper.

Application can be thought of as "type of" so Xa means a has type X. This means that types are predicates (presumably allowing some form of set theory), yet are still terms, apparently collapsing the type hierarchy without a problem. Application can also be thought of in the usual way, as reduction works as in the lambda calculus (the terms of these logics are lambda terms).

The Xi combinator can be thought of as the subset combinator- which I'm going to write as Z here. ZXY can then be seen as saying that X is a subset of Y, or if we think of predicates, then for all "a" such that Xa, Ya. This gives rise to implication in a way that I finally understood today. Given the combinator K, which as a lambda term is (\x.\y.x) with "\" standing for lambda, the term Z(KX)(KY) means X => Y. This is not a function from type X to type Y, which is instead written ZX(Y . f) to say f : X -> Y with "." as composition (\f.\g.\x.f(g(x))) (I may need to stop with the ascii art symbols and start putting in real ones)) with says that for all x such that Xx (x in X), Y(fX), so fx in Y. Back to the term Z(KX)(Ky), notice that this means that for all x KXx reduces to X and KYx reduces to Y. This is then the statement that if X then Y, which is exactly what we wanted! My jaw literally dropped when I realized that this is what the interpretation is (I hope I'm right) and I had to just sit there for a second and chill before reading on.

To get a universal quantifier, we simply do a lambda abstraction over a term and make use of Z. To say that for all x in X, Px we write ZX(\x.P a).

To get the Universe combinator U (the set of all things) we simply write K(True). This term reduces to True for all arguments, and therefore all terms are of this type. This means that we need some value for True, however (not that this is unexpected). First off, the system in question has a combinator H saying that something is a proposition, and so ZHH is True. As I understand it, this is saying that the statement that something is a proposition is a proposition, which is surely the case.

There is still more for me to say about this system. I still don't understand the product and coproduct construction given by Luke Palmer, and I haven't finished the paper, so I haven't seen how it interprets logic yet. This is cool stuff, and I find it all surprising for some reason. It seems to stretch my intuitions, which is always fun.