A system λ_θ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory of types, the system λ_θ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system λ_θ is controlled by a parameter θ which allows more options for state types and state variables than is present in Montague and Gallin. A main goal of the paper is to establish some basic metatheory of λ_θ: (i) an Andrews-like characterization of its models in terms of combinatory logic is given, and this combinatory logic involves a BCKW-like basis rather than an SKI-like basis and (ii) semantic conservation and expressibility results relating λ_θ to the maximal system λ_ω are proven. Similar results are proven for the relation between λ_ω and λ, the corresponding ordinary simply-typed lambda calculus. This answers a question of Zimmermann in the semantics of the simply typed setting. In a companion paper this is extended to Church's simple theory of types. We further develop a partial correspondence between a pure combinatory logic centered on the BCKW-like basis and the weak deductive system for λ_ω wherein β-reduction is not allowed under a lambda abstract, and we use this to show partial deductive conservation between the maximal system λ_ω and the intermediary systems λ_θ.
Sean Walsh (Tue,) studied this question.