  Montague’s work is primarily in Montague 1960 and 1970, and has natural language as its primary motivation. The treatment is semantic, but in Gallin 1975 an axiom system is presented. The logic Gallin axiomatized is a full type-theoretic system, with intensional objects of each type. Completeness is proved relative to an analog of Henkin models, familiar for higher type classical logics.