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

TL;DR

This paper introduces a modal lambda calculus system that extends simply-typed lambda calculus with modal logic, establishing its foundational properties, expressiveness, and connections to combinatory logic and Henkin models.

Contribution

It develops the system $oldsymbol\lambda_{\theta}$ with a parameterized approach, proves its metatheoretical properties, and demonstrates its high expressiveness and relation to existing lambda calculi.

Findings

Proves completeness for $eta\eta$-reduction.

Provides an Andrews-like characterization of Henkin models.

Shows conservation and expressibility of the maximal system $oldsymbol\lambda_{\omega}$.

Abstract

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.