2024/10/22 by Sean Walsh, Walsh, Sean
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.46298/lmcs-22(3:4)2026
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 BCKW-like basis rather than an 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 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λθ.