Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

A system $\boldsymbol\lambda_{\upsilon}$ 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_{\upsilon}$ is developed in the typed base theory most commonly used today, namely the simply-typed lambda calculus. Further, the system $\boldsymbol\lambda_{\upsilon}$ is controlled by a parameter $\upsilon$ 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_{\upsilon}$: (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 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_{\upsilon}$ is proven, and expressibility of $\boldsymbol\lambda_{\omega}$ in $\boldsymbol\lambda_{\upsilon}$ 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 Zimmerman in the simply-typed setting. In a companion paper this is extended to Church's simple theory of types.