A system $\boldsymbol\lambda_{\theta}$ 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\lambda_{\theta}$ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system $\boldsymbol\lambda_{\theta}$ is controlled by a parameter $\theta$ 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 the basic metatheory of $\boldsymbol\lambda_{\theta}$: (i) a completeness theorem is proven for $\beta\eta$-reduction, and (ii) an Andrews-like characterization of Henkin models in terms of combinatory logic is given; and this involves, with some necessity, a distanced version of $\beta$-reduction and a $\mathsf{BCKW}$-like basis rather than $\mathsf{SKI}$-like basis. Further, conservation of the maximal system $\boldsymbol\lambda_{\omega}$ over $\boldsymbol\lambda_{\theta}$ is proven, and expressibility of $\boldsymbol\lambda_{\omega}$ in $\boldsymbol\lambda_{\theta}$ is proven; thus these modal logics are highly expressive. Similar results are proven for the relation between $\boldsymbol\lambda_{\omega}$ and $\boldsymbol\lambda$, the corresponding ordinary simply-typed lambda calculus. This answers a question of Zimmermann in the simply-typed setting. In a companion paper this is extended to Church's simple theory of types.

翻译：本文发展了一个结合模态逻辑与简单类型 lambda 演算的系统 $\boldsymbol\lambda_{\theta}$，它推广了 Montague 与 Gallin 所研究的系统。Montague 与 Gallin 基于 Church 的简单类型论工作，而系统 $\boldsymbol\lambda_{\theta}$ 则在当今最常用的类型基础理论——即简单类型 lambda 演算——中发展。此外，系统 $\boldsymbol\lambda_{\theta}$ 由一个参数 $\theta$ 控制，该参数为状态类型和状态变量提供了比 Montague 与 Gallin 系统中更多的选项。本文的一个主要目标是建立 $\boldsymbol\lambda_{\theta}$ 的基本元理论：(i) 证明了关于 $\beta\eta$-归约的完备性定理；(ii) 给出了一个类似 Andrews 的、用组合子逻辑刻画 Henkin 模型的方法；这必然涉及一种有距版本的 $\beta$-归约以及一个类似 $\mathsf{BCKW}$ 的基，而非类似 $\mathsf{SKI}$ 的基。此外，证明了极大系统 $\boldsymbol\lambda_{\omega}$ 对 $\boldsymbol\lambda_{\theta}$ 的保守性，以及 $\boldsymbol\lambda_{\omega}$ 在 $\boldsymbol\lambda_{\theta}$ 中的可表达性；因此这些模态逻辑具有很强的表达能力。对于 $\boldsymbol\lambda_{\omega}$ 与相应的普通简单类型 lambda 演算 $\boldsymbol\lambda$ 之间的关系，也证明了类似的结果。这回答了 Zimmermann 在简单类型框架下的一个问题。在一篇配套论文中，此结果被推广至 Church 的简单类型论。