A system $\boldsymbolλ_θ$ 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 $\boldsymbolλ_θ$ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system $\boldsymbolλ_θ$ 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 $\boldsymbolλ_θ$: (i) an Andrews-like characterization of its models in terms of combinatory logic is given, and this combinatory logic involves a $\mathsf{BCKW}$-like basis rather than an $\mathsf{SKI}$-like basis and (ii) semantic conservation and expressibility results relating $\boldsymbolλ_θ$ to the maximal system $\boldsymbolλ_ω$ are proven. Similar results are proven for the relation between $\boldsymbolλ_ω$ and$\boldsymbolλ$, 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 $\mathsf{BCKW}$-like basis and the weak deductive system for $\boldsymbolλ_ω$ wherein $β$-reduction is not allowed under a lambda abstract, and we use this to show partial deductive conservation between the maximal system $\boldsymbolλ_ω$ and the intermediary systems $\boldsymbolλ_θ$.

翻译：本文发展了一个结合模态逻辑与简单类型λ演算的系统$\boldsymbolλ_θ$，并推广了Montague与Gallin所研究的系统。Montague和Gallin使用Church的简单类型论展开研究，而本文的系统$\boldsymbolλ_θ$则建立在当今最常用的有类型基础理论——即简单类型λ演算之上。此外，系统$\boldsymbolλ_θ$由参数$θ$控制，该参数提供了比Montague与Gallin系统更多的状态类型与状态变量选择。本文的主要目标是建立$\boldsymbolλ_θ$的基本元理论：（i）给出其模型在组合逻辑意义上的类Andrews刻画，其中组合逻辑采用基于$\mathsf{BCKW}$的基而非基于$\mathsf{SKI}$的基；（ii）证明$\boldsymbolλ_θ$与最大系统$\boldsymbolλ_ω$之间的语义保守性与可表达性结果。对于$\boldsymbolλ_ω$与对应的普通简单类型λ演算$\boldsymbolλ$之间的关系，也得到了类似结果。这回应了Zimmermann在简单类型设定语义学中提出的一个问题。在配套论文中，该结果被推广至Church的简单类型论。我们进一步发展了以$\mathsf{BCKW}$类基为核心的纯组合逻辑与$\boldsymbolλ_ω$的弱演绎系统之间的部分对应关系（该弱系统中λ抽象下不允许β归约），并利用这一对应关系证明了最大系统$\boldsymbolλ_ω$与中间系统$\boldsymbolλ_θ$之间的部分演绎保守性。