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

TL;DR

The paper develops the simply-typed modal lambda calculus $\boldsymbol\lambda_{\theta}$, introducing a state-type parameter $\theta$ to generalize Montague–Gallin within a simply-typed base and addressing Zimmermann’s question about the expressive power of Henkin semantics. It establishes a robust metatheory: $βη$-completeness for $\boldsymbol\lambda_{\theta}$, an Andrews-style combinatorial characterization of Henkin models using a $\mathsf{BCDKW}$-basis and a distanced $β$-reduction, semantic conservation of the maximal system $\boldsymbol\lambda_{\omega}$ over $\boldsymbol\lambda_{\theta}$, and expressibility results between nested modal and non-modal calculi. A central technical development is the distanced $β$-reduction, together with an intensional combinatory logic framework that supports a $\mathsf{BCDKW}$-basis rather than the traditional $\mathsf{SKI}$-basis, enabling complete model-theoretic analyses via open-term models and combinatorial characterizations. The work shows, among other results, the semantic and deductive conservation and expressibility between $\boldsymbol\lambda_{\omega}$, $\boldsymbol\lambda_{\theta}$, and $\boldsymbol\lambda$, and proves that certain expressive enrichments (e.g., constants of state type) are not eliminable, revealing both the strengths and limitations of finite-variable modal logics. Collectively, the results advance the metatheory of modal typed lambda calculi, provide tools for combining modal reasoning with functional programming formalisms, and pave the way for extending the framework to Church’s simple theory of types in a companion paper.

Abstract

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 the basic metatheory of $\boldsymbolλ_θ$: (i) a completeness theorem is proven for $βη$-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 $β$-reduction and a $\mathsf{BCKW}$-like basis rather than $\mathsf{SKI}$-like basis. Further, conservation of the maximal system $\boldsymbolλ_ω$ over $\boldsymbolλ_θ$ is proven, and expressibility of $\boldsymbolλ_ω$ in $\boldsymbolλ_θ$ is proven; thus these modal logics are highly expressive. 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 simply-typed setting. In a companion paper this is extended to Church's simple theory of types.

Theorems & Definitions (175)

• Theorem 1.1
• Theorem 1.2
• Theorem 1.3
• Theorem 1.4
• Theorem 1.5
• Theorem 1.6
• Theorem 1.7
• Theorem 1.8
• Definition 2.1
• Example 2.2