 where \(R_{{o}\imath\imath}\) denotes the accessibility relation associated with \(\Box\) and type \({\imath}\) is identified with possible worlds. Moreover, since \(\forall x_{\alpha} [\bA_{{o}\alpha} x_{\alpha}]\) is shorthand in Church’s type theory for \(\Pi_{{o}({o}\alpha)} [\lambda x_{\alpha} [\bA_{{o}\alpha} x_{\alpha}]]\), the modal formula 