gt; &gt; The typed lambda calculus is basically just omega-order logic
&gt;
&gt; MW: Omega-order logic? You lost me.

Well, there's second-order logic, in which there are quantifiers range
over properties (or set) of individuals (among other things),
third-order logic in which there are quantifiers that range over
properties of properties of individuals (among other things), and so on.
Omega-order logic has quantifiers that range over all the things that
all the nth-order logics range over, for all n.

&gt;