 Church’s notion of “order” is not quite one that is familiar from talk of “first order logic” and “second order logic”. First order logic will have bound variables of s-type 0, and a logic which quantifies over variables of s-type 1, thus the familiar notion of “order” is one more than the highest order of any of the bindable variables in the s-type system.