 Church’s type theory can be employed as a meta-logic to concisely embed expressive other logics such as the higher-order modal logic assumed by Gödel. By exploiting the possible world semantics of this target logic, its syntactic elements are defined in such a way that the infrastructure of the meta-logic are reused as much as possible. In this technique, called shallow semantical embedding, the modal operator \(\Box\), for example, is simply identified with (taken as syntactic sugar for) the λ-formula 