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 $\mathsf{BCKW}$-like basis rather than an $\mathsf{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 $\mathsf{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λ_θ$.

Abstract Frege’sGrundgesetzewas one of the 19th century forerunners to contemporary set theory which was plagued by the Russell paradox. In recent years, it has been shown that subsystems of theGrundgesetzeformed by restricting the comprehension schema are consistent. One aim of this paper is to ascertain how much set theory can be developed within these consistent fragments of theGrundgesetze, and our main theorem (Theorem 2.9) shows that there is a model of a fragment of theGrundgesetzewhich defines a model of all the axioms of Zermelo–Fraenkel set theory with the exception of the power set axiom. The proof of this result appeals to Gödel’s constructible universe of sets and to Kripke and Platek’s idea of the projectum, as well as to a weak version of uniformization (which does not involve knowledge of Jensen’s fine structure theory). The axioms of theGrundgesetzeare examples ofabstraction principles, and the other primary aim of this paper is to articulate a sufficient condition for the consistency of abstraction principles with limited amounts of comprehension (Theorem 3.5). As an application, we resolve an analogue of the joint consistency problem in the predicative setting.