Abstract

We introduce relational semantics for “flat Heyting-Lewis logic” \(\mathsf{HLC}^{\flat}\). This logic arises as the extension of intuitionistic logic with a Lewis-style strict implication modality that, contrary to its “sharp” counterpart \(\mathsf{HLC}^{\sharp}\), does not turn meets into joins in its first argument. We prove completeness and the finite model property for \(\mathsf{HLC}^{\flat}\) and for several extensions with additional axioms.

1 Introduction↩︎

Recent years have seen a revival of the interest in intuitionistic modal logics [@proietti2012; @litak14:trends; @stepaiale15; @artemovp16:rsl; @litakpr17; @BalbianiBDF20; @rog20b; @Kavvos20; @DasM23; @ShillitoGGI23; @GirlandoEA23; @AlmeidaB24; @BalbianiEA24; @DasEA24; @groshiclo25; @BozzelliCCM25; @Mojtahedi26; @BalbianiG26], including extensions with a Lewisian strict implication \(\sto\) [@LitVis18; @litvis24] and various types of conditional implications [@wei19; @DalGir26]. Recall that in the intuitionistic setting, \(\sto\) is not definable in terms of unary \(\Box\). Instead, it can be viewed as sitting between \(\Box(p \to q)\) and \(\Box p \to \Box q\). Indeed, the basic “flat” system³ \(\mathsf{HLC^{\flat}}\) proves [@LitVis18]:

\(\Box(p \to q) \to (p \sto q)\)
\((p \sto q) \to (\Box p \to \Box q)\).

The original motivation of the Utrecht school to study such a connective came from research on schematic logics of theories over intuitionistic arithmetic \(\mathsf{HA}\). More specifically, it arose from the study of \(\Sigma^0_1\)-preservativity [@viss:eval85; @viss:prop94; @viss:subs02; @iemh:pres03; @IemhoffJZ05:igpl], which over \(\mathsf{PA}\) can be seen as the contraposed variant of both \(\Pi^0_1\)-conservativity and arithmetical interpretability [@bera:inte90; @shav:rela88; @japa:logi98; @viss:over98; @arte:prov04]. Subsequently, many other application and interpretations were put forward, see e.g. [@LitVis18; @grolitpat26-arxiv]. In particular, in the presence of an additional axiom \(\mathsf{str}\) (see Section 5) the resulting calculus turns out to be the Curry-Howard counterpart (i.e. the inhabitation logic) of (Hughes) arrows in functional programming, in particular in Haskell [@Hug00; @Hug04; @atkey08:msfp; @jacobshh09:jfp; @lindleywy08:msfp; @lindleywy10:jfp; @lindley14:wgp]. Somewhat underdeveloped philosophical applications include a generalisation of intuitionistic epistemic logic \(\mathsf{IEL}\) [@artemovp16:rsl] to the intuitionistic logic of entailments \(\mathsf{IELE}\) [@grolitpat26-arxiv] or a fine-grained analysis of the collapse of Lewis’ original 1918 system of strict implication caused by involutive negation [@LitVis18].⁴

The flat calculus \(\mathsf{HLC^{\flat}}\) arises from extending intuitionistic logic with a binary operator \(\sto\) that is normal in it second argument, transitive, and satisfies implication necessitation, i.e. derivability of \(\varphi\to \psi\) implies derivability of \(\varphi\sto \psi\). From this, we can obtain the sharp calculus \(\mathsf{HLC^{\sharp}}\) by adding the axiom:

\((p \sto r) \wedge (q \sto r) \to ((p \vee q) \sto r)\)

This sharp version of the logic can conveniently be interpreted in Kripke-style relational semantics. This perspective has resulted in numerous correspondence, completeness and finite model property results for this “sharp” semantics [@iemh:prov01; @iemh:pres03; @Zhou03; @IemhoffJZ05:igpl; @LitVis18], with recent work showing how to use the natural Gödel-McKinsey-Tarski translation to transfer metatheory of bimodal classical logics [@grolitpat26-arxiv].

Nevertheless, from the point of view of applications and interpretations discussed above, there are few reasons to insists on the “sharp” calculus \(\mathsf{HLC^{\sharp}}\) as the minimal one, excluding interpretations not validating \(\mathsf{di}\). In more philosophical contexts such as \(\mathsf{IELE}\) [@grolitpat26-arxiv], the present state of the research does not determine the status of \(\mathsf{di}\), whereas in mathematical and computer science applications enforcing it as a base axiom would simply be too restrictive. Insisting on the validity of \(\mathsf{di}\) in the inhabitation logic of arrows in functional programming languages [@Hug00; @Hug04; @atkey08:msfp; @jacobshh09:jfp; @lindleywy08:msfp; @lindleywy10:jfp; @lindley14:wgp] would limit the Curry-Howard interpretation to so-called arrows with choice [@Hug04]. While this would still cover arrows with delay and higher-order arrows (corresponding, respectively, to applicative functors and monads), and some other instances such as list processors and Kleisli arrows, important examples of arrows without choice can be obtained using automata or functions on infinite streams [@grolitpat26-arxiv].

The situation is similar when it comes to schematic logics of arithmetical theories, i.e. the original motivation of the Utrecht school to study variants and extensions of \(\mathsf{HLC}\): Sharpness obtains in some contexts, but not in others. For example, it fails classically, i.e. when \(\mathsf{HA}\) is replaced by Peano Arithmetic (\(\mathsf{PA}\)). In fact, one can argue that the main reason why classical interpretability logic is a separate subfield with its own methods and semantics, irreducible even to multi-modal and multi-dimensional normal modal logics, is precisely the failure of the validity of the (contraposed form of) \(\mathsf{di}\) in the logic of \(\Pi^0_1\)-conservativity/interpretability of \(\mathsf{PA}\). Some readers might find this failure surprising given that \(\mathsf{di}\) holds in the schematic theory of \(\mathsf{HA}\), which is a subtheory of \(\mathsf{PA}\). However, non-monotonicity of schematic logics is a phenomenon observable even in the signature of provability with a single unary \(\Box\) ([@LitVis18]). A sufficient condition for sharpness of the schematic logic of a given arithmetical theory \(T\) is that \(T\) is able to prove that the set of \(T\)-theorems is closed under q-realisability [@LitVis18]. Note that if \(T' \supseteq T\), the \(T\)-provable statements about \(T\)-theorems remain \(T'\)-provable, but there might be new \(T'\)-theorems for which q-realisability is not \(T'\)-provable (and, a fortiori, not \(T\)-provable).

Arguably, the main temptation to accept the sharp system as the minimal one has been that of nice completeness results and natural countermodels. In the flat setting, so far one has had to turn to algebraic semantics or a suitable adaptation of Chellas-Weiss semantics for \(\mathsf{ICK}\) [@wei19; @cialiu19; @dufgro25], Routley-Meyer semantics for substructural logics [@roumey72a; @roumey72b; @roumey73; @restall00; @bimdunfer18], or (generalised) Veltman semantics [@dejo:prov90; @verb:unpu92; @dejo:comp99; @joosten2020], because a simple Kripke-style semantics for \(\mathsf{HLC^{\flat}}\) appeared elusive.

In this paper we fill this gap by providing a Kripkean interpretation for \(\mathsf{HLC^{\flat}}\). This semantics is inspired by recent work on semantics of \(\mathsf{CK}\) [@groshiclo25], and crucially relies on using a preorder \(\preceq\) instead of a partial order to interpret the intuitionistic implication. Since the semantic clause for \(\sto\) directly enforces upward persistence (Definition 5), the most general version of the new semantics (Definition 5) does not impose any interaction conditions between \(R\) and \(\preceq\). However, similarly to the case of intuitionistic \(\Box\) and unlike the sharp interpretation, our language is oblivious to closing \(R\) under post-composing with \(\preceq\) (Proposition [prop:upsame]), and the resulting upward-flat frames (Section 3.2) prove convenient for computing correspondents and obtaining completeness results.

Using a canonical model construction, we prove completeness and the finite model property for \(\mathsf{HLC^{\flat}}\) and several of its extensions (Sections 4 and 5.1). Guided by the canonical model construction for \(\mathsf{CK}\), we use segments rather than prime theories to have a more fine-grained handle on the modal accessibility relation. Still mirroring \(\mathsf{CK}\), we sometimes need to restrict our choice of segments, for example when proving completeness for natural variants of \(\mathsf{K4}\) and \(\mathsf{S4}\) in our setting (Section 5.2).

When \(\preceq\) is collapsed to equality, turning our frames into standard Kripke frames, our frames turn \(\mathsf{lb}\) into a bi-implication, rather than \(\mathsf{bl}\). This does not mean that our semantics trivialises classically: in the preorder setting, validating excluded middle simply requires \(\preceq\) to be symmetric, and such a classical variant of our semantics does not collapse \(\sto\) (Example 3). This creates the opportunity to use our semantics for completeness results for subsystems of standard interpretability logics such as \(\mathsf{ILM}\) and \(\mathsf{ILP}\).

In the \(\mathsf{CK}\) setting, the segment approach can be used to obtain duality results [@groshiclo26]. While our paper does not discuss duality in depth, we include comments for the interested reader, such as Remarks [rem:dualityhard] and [rem:nogmt], illustrating difficulties with more standard approaches. However, we discuss a promising application in Section 6 in the context of syntactically motivated notion of extension stability. We note the relationship of this notion to what one might call the open subframe construction, and use our semantics to show that \(\mathsf{HLC^{\sharp}}\) is not extension stable, unlike the flat base calculus.

2 Intuitionistic strict implication, sharply and flatly↩︎

This section provides preliminaries and recapitulates known material. Section 2.1 presents the base flat system \(\mathsf{HLC^{\flat}}\). Section 2.2 discusses the sharp variant \(\mathsf{HLC^{\sharp}}\)together with its known Kripke semantics. Section 2.3 recapitulates the algebraic semantics of both systems. Throughout the paper, we denote by \(\mathcal{L}_{\sto}\) the language generated by the grammar \[\varphi::= p \mid \top \mid \bot \mid \varphi\wedge \varphi\mid \varphi\vee \varphi\mid \varphi\to \varphi\mid \varphi\sto \varphi,\] where \(p\) ranges over some arbitrary but fixed set \(\mathop{\mathrm{Prop}}\) of proposition letters. We abbreviate \(\Box\varphi:= \top \sto \varphi\).

2.1 Syntax and axioms of the base flat system↩︎

A consecution is an expressions of the form \(\Gamma \Rightarrow\varphi\), where \(\Gamma \cup \{ \varphi\} \subseteq \mathcal{L}_{\sto}\).

Definition 1. Let \(\mathrm{Ax^{\flat}}\) be an axiomatisation of intuitionistic logic together with the axioms

\(((p \sto q) \land (p \sto r)) \to (p \sto (q \land r))\)
\(((p \sto q) \wedge (q \sto r)) \to (p \sto r)\)

If \(\mathrm{Ax}\subseteq \mathcal{L}_{\sto}\), the we denote by \(\mathcal{I}(\mathrm{Ax})\) the collection of substitution instances of formulas in \(\mathrm{Ax}\), and define the axiomatic system \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) by: \[\mathsf{(Ax)} \; \dfrac{\varphi\in\mathcal{I}(\mathrm{Ax^{\flat}})\cup \mathcal{I} (\mathrm{Ax})}{\Gamma \Rightarrow\varphi} \qquad \mathsf{(El)} \; \dfrac{\varphi\in \Gamma}{\Gamma \Rightarrow\varphi} \qquad \mathsf{(MP)} \; \dfrac{\Gamma \Rightarrow\varphi\qquad \Gamma \Rightarrow\varphi\to \psi}{\Gamma \Rightarrow\psi} \qquad \mathsf{(N_a)} \; \dfrac{\emptyset \Rightarrow\varphi\to \psi}{\Gamma \Rightarrow\varphi\sto \psi}\] We say that \(\Gamma \Rightarrow\varphi\) is provable in \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\), and write \(\Gamma \vdash_{\mathrm{Ax}} \varphi\), if there exists a tree of consecutions built using the rules above with \(\Gamma \Rightarrow\varphi\) as root and adequate applications of rules \(\mathsf{(El)}\) and \(\mathsf{(Ax)}\) as leaves. If \(\mathrm{Ax}= \emptyset\) then we abbreviate \(\vdash_{\mathrm{Ax}}\) to \(\vdash\), and if \(\mathrm{Ax}=\{ \varphi_1, \dots, \varphi_n\}\) then we write \(\mathsf{HLC^{\flat}}\oplus \varphi_1 \oplus \dots \oplus \varphi_n\) for \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\). Finally, we write \(\Gamma \vdash_{\mathrm{Ax}} \Delta\) if there exist \(\psi_1, \ldots, \psi_m \in \Delta\) such that \(\Gamma \vdash_{\mathrm{Ax}} \psi_1 \vee \cdots \vee \psi_m\).

For \(\mathrm{Ax}\subseteq \mathcal{L}_{\sto}\) and uniform substitution \(\sigma\), the following rules are admissible in \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\): \[\infer{\Gamma, \Gamma' \Rightarrow\varphi} {\Gamma \Rightarrow\varphi} \qquad \infer{\Gamma \Rightarrow\varphi} {\{\Gamma \Rightarrow\delta \; \mid \; \delta \in \Delta \} \quad \Delta \Rightarrow\varphi} \qquad \infer{\Gamma^\sigma \Rightarrow\varphi^\sigma} {\Gamma \Rightarrow\varphi} \qquad \infer={\Gamma \Rightarrow\varphi\rightarrow \psi} {\Gamma, \varphi\Rightarrow\psi}\]

Proof. By induction on the height of a derivation for the premiss(es). ◻

The first three rules show that \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) is a monotone, compositional and structural relation, respectively. The double line in the last rule indicates that it holds both ways. Furthermore, since proof trees are finite we have \(\Gamma \vdash_{\mathrm{Ax}} \varphi\) if and only if there is a finite \(\Gamma' \subseteq \Gamma\) such that \(\Gamma' \vdash_{\mathrm{Ax}} \varphi\). Therefore \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) is a finitary logic [@Kra99]. Wherever possible, we blur the distinction between a logic and the set of its theorems (identified with derivable consecutions with an empty premise).

2.2 The sharpening↩︎

Definition 2. Let \(\mathsf{di}\) be the axiom \((p \sto r) \wedge (q \sto r) \to ((p \vee q) \sto r)\), and define the sharp Heyting-Lewis calculus* by \(\mathsf{HLC^{\sharp}}:= \mathsf{HLC^{\flat}}\oplus (\mathsf{di})\).*

The sharp systems is known to allow a simple Kripke-style semantics, with soundness, completeness and the finite model property results for many of its extensions [@iemh:prov01; @iemh:pres03; @Zhou03; @IemhoffJZ05:igpl; @LitVis18; @grolitpat26-arxiv]:

Definition 3. A sharp frame* is a tuple \(\mathfrak{F} = (W, \leq, R)\) consisting of a set \(W\), a partial order \(\leq\) on \(W\), and a relation \(R\) on \(W\) such that for all \(w, v, u \in W\): \[\text{if}\quad w \leq v \quad\text{and}\quad v R u \quad\text{then}\quad w R u.\]*

A sharp model* is formed by adding a valuation that interprets proposition letters as upsets. The interpretation of \(\mathcal{L}_{\sto}\)-formulas at a world \(w\) in a sharp model \(\mathfrak{M}\) is defined recursively via: \[\begin{align} {4} &\mathfrak{M}, w \Vdash^sp &&\quad\text{iff}\quad w \in V(p) \\ &\mathfrak{M}, w \Vdash^s\bot &&\phantom{\quad\text{iff}\quad}\text{never} \\ &\mathfrak{M}, w \Vdash^s\varphi\wedge \psi &&\quad\text{iff}\quad\mathfrak{M}, w \Vdash^s\varphi\text{ and } \mathfrak{M}, w \Vdash^s\psi \\ &\mathfrak{M}, w \Vdash^s\varphi\vee \psi &&\quad\text{iff}\quad\mathfrak{M}, w \Vdash^s\varphi\text{ or } \mathfrak{M}, w \Vdash^s\psi \\ &\mathfrak{M}, w \Vdash^s\varphi\to \psi &&\quad\text{iff}\quad\text{for all } w' \succeq w, \text{ if } \mathfrak{M}, w \Vdash^s\varphi\text{ then } \mathfrak{M}, w \Vdash^s\psi \\ &\mathfrak{M}, w \Vdash^s\varphi\sto \psi &&\quad\text{iff}\quad\text{for all } v \, ( \text{if } w R v \text{ and } \mathfrak{M}, v \Vdash^s\varphi \text{ then } \mathfrak{M}, v \Vdash^s\psi ) \end{align}\]*

2.3 Algebraic semantics↩︎

While Kripke completeness has so far only been available for the sharp calculus and its reasonably well-behaved extensions, algebra provides an obvious route towards a generic completeness result.

Definition 4. A flat Lewisian Heyting Algebra Expansion, or \(\mathsf{L}\)-\(\mathrm{\small hae}\)⁵, is a tuple \(\mathcal{A}:=\langle A, \wedge, \vee, \sto, \to, \bot, \top \rangle\) such that \(\langle A, \wedge, \vee, \to, \top, \bot \rangle\) is a Heyting algebra and the following laws are satisfied:

\((a \sto b) \wedge (a \sto c) = a \sto(b \wedge c)\),
\((a \sto b) \wedge (b \sto c) \leq a \sto c\),
\(a \sto a = \top\).

If \(\mathcal{A}\) additionally satisfies

\((a \sto c) \wedge (b \sto c) = (a \vee b) \sto c\).

then it is a sharp Lewisian Heyting Algebra (\(\mathsf{L}\)-\(\mathrm{\small hao}\)).

A \(\mathsf{L}\)-\(\mathrm{\small hae}\)is a \(\mathsf{L}\)-\(\mathrm{\small hao}\)if and only if its strict reduct, i.e. the reduct without \(\to\), is a weak Heyting algebra [@CelaniJ05:mlq]. We note that \(\mathsf{CK}\), \(\mathsf{CD}\), \(\mathsf{CT}\), and \(\mathsf{CI}\) are referred to as \(\mathsf{C1}\) – \(\mathsf{C4}\) in [@CelaniJ05:mlq]. A valuation \(v\) in \(\mathcal{A}\), as usual, maps propositional atoms to elements of \(A\) and is inductively extended to \(\hat{v}\) defined on all formulas in the obvious way. We write \(\mathcal{A}, v \Vdash \varphi\) if \(\hat{v}(\varphi) = \top\) and \(\mathcal{A}\Vdash \varphi\) if \(\mathcal{A}, v \Vdash \varphi\) for every valuation \(v\). For \(\mathrm{Ax}\subseteq \mathcal{L}_{\sto}\), we write \(\mathsf{L}-\mathrm{\small hae}(\mathrm{Ax})\) for the class of \(\mathsf{L}-\mathrm{\small hae}\)-algebras \(\mathcal{A}\) such that \(\mathcal{A}\Vdash \varphi\) for all \(\varphi\in \mathrm{Ax}\). Furthermore, we write \(\mathsf{L}-\mathrm{\small hae}(\mathrm{Ax}) \Vdash \Gamma \Rightarrow\varphi\) if there exists a finite \(\Gamma' \subseteq \Gamma\) such that all algebras in \(\mathsf{L}-\mathrm{\small hae}(\mathrm{Ax})\) validate \((\bigwedge \Gamma') \to \varphi\). Then the usual Lindenbaum-Tarski construction gives:

Theorem 1. Let \(\mathrm{Ax}\subseteq \mathcal{L}_{\sto}\) be a set of axioms and \(\Gamma \Rightarrow\varphi\) a consecution. Then \(\Gamma \vdash_{\mathrm{Ax}} \varphi\) if and only if \(\mathsf{L}-\mathrm{\small hae}(\mathrm{Ax}) \Vdash \Gamma \Rightarrow\varphi\).

3 Relational semantics for flat Heyting-Lewis logic↩︎

We introduce relational semantics for \(\mathsf{HLC^{\flat}}\), first in the most general version (Section 3.1), then in the “upward-flat” variant (Section 3.2) simplifying calculations of correspondents and completeness proofs. In Section 3.3 we compare the flat semantics to the sharp semantics from Definition 3.

3.1 Flat frames↩︎

Definition 5. A flat frame* is a tuple \((W, \preceq, R)\) consisting of a nonempty set \(W\), a preorder \(\preceq\) on \(W\) and a relation \(R\) on \(W\). A flat model is a pair \(\mathfrak{M} = (\mathfrak{F}, V)\) consisting of a flat frame \(\mathfrak{F} = (W, \preceq, R)\) and a valuation \(V : \mathop{\mathrm{Prop}}\to \mathop{\mathrm{up}}(W, \preceq)\) that assigns to each proposition letter \(p\) an upset \(V(p)\) of \((W, \preceq)\). The interpretation of \(\mathcal{L}_{\sto}\)-formulas at a world \(w \in W\) extends the usual intuitionistic semantics with \[\begin{align} \mathfrak{M}, w \Vdash \varphi\sto \psi &\quad\text{iff}\quad\text{for all } w' \succeq w, \text{ if } \mathfrak{M}, v \Vdash \varphi \text{ for all } v \in W \text{ such that } w'Rv \\ &\phantom{\quad\text{iff}\quad\text{for all } w' \geq w, }\; \text{ then } \mathfrak{M}, v \Vdash \psi \text{ for all } v \in W \text{ such that } w'Rv \end{align}\] The truth set of \(\varphi\) is given by \(\llbracket\varphi\rrbracket^{\mathfrak{M}} = \{ w \in W \mid \mathfrak{M}, w \Vdash \varphi\}\).*

Let \(\Gamma \cup \{ \varphi\} \subseteq \mathcal{L}_{\sto}\) and let \(\mathfrak{M}\) be a flat model. We write \(\mathfrak{M}, w \models \Gamma\) if \(w\) satisfies all \(\psi \in \Gamma\), and we say that \(\mathfrak{M}\) validates* \(\Gamma \Rightarrow\varphi\) if \(\mathfrak{M}, w \models \Gamma\) implies \(\mathfrak{M}, w \models \varphi\) for all worlds \(w\) in \(\mathfrak{M}\). A flat frame \(\mathfrak{F}\) validates \(\Gamma \Rightarrow\varphi\) if every model of the form \((\mathfrak{F}, V)\) validates the consecution, and it validates a formula \(\varphi\) if it validates the consecution \(\emptyset \Rightarrow\varphi\). If \(\mathrm{Ax}\subseteq\mathcal{L}_{\sto}\) is a set of axioms, then we write \(\Gamma \Vdash_{\mathrm{Ax}} \varphi\), and say that \(\Gamma\) semantically entails \(\varphi\) on the class of flat frames for \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\), if every flat frame that validates all formulas in \(\mathrm{Ax}\) also validates the consecution \(\Gamma \Rightarrow\varphi\).*

Using truth-set notation, we have \(\mathfrak{M}, w \Vdash \varphi\sto \psi\) iff \(R[w'] \subseteq \llbracket\varphi\rrbracket^{\mathfrak{M}}\) implies \(R[w'] \subseteq \llbracket\psi \rrbracket^{\mathfrak{M}}\), for all \(w' \succeq w\). To illustrate the subtleties of this semantics (even in the classical setting), we give two examples showing that [ax:di] and the reverse of [ax:lb] are not valid.

A routine induction on the structure of \(\varphi\) allows us to prove:

Lemma 1 (Intuitionistic heredity). Let \(\mathfrak{M} = (W, \preceq, R, V)\) be a flat model. Then for all \(\varphi\in \mathcal{L}_{\sto}\) and all \(w, v \in W\), if \(\mathfrak{M}, w \Vdash \varphi\) and \(w \preceq v\) then \(\mathfrak{M}, v \Vdash \varphi\).

Every flat frame gives rise to a \(\mathsf{L}-\mathrm{\small hae}\) via its complex algebra.

Definition 6. The complex algebra* of a flat frame \(\mathfrak{F} = (W, \preceq, R)\) is \(\mathfrak{\mathfrak{F}}^{+\flat} := \langle\mathop{\mathrm{up}}(W, \preceq), \cap, \cup, \mathrel{\mkern 1mu\underline{\mkern-1mu \to\mkern-2mu}\mkern 2mu }, \mathrel{\mkern 1mu\underline{\mkern-1mu \sto\mkern-1mu}\mkern 1mu }^\flat, W, \emptyset \rangle\), where \[\begin{align} a \mathrel{\mkern 1mu\underline{\mkern-1mu \to\mkern-2mu}\mkern 2mu }b &:= \{ w \in W \mid \text{for all } v \succeq w, \, v \in a \text{ implies } v \in b \} \\ a \mathrel{\mkern 1mu\underline{\mkern-1mu \sto\mkern-1mu}\mkern 1mu }^\flat b &:= \{ w \in W \mid \text{for all } v \succeq w, \, R[v] \subseteq a \text{ implies } R[v] \subseteq b \}. \end{align}\]*

Lemma 2. If \(\mathfrak{F} = (W, \preceq, R)\) is a flat frame then \(\mathfrak{\mathfrak{F}}^{+\flat}\) is a \(\mathsf{L}-\mathrm{\small hae}\), and \(\mathfrak{F}\) and \(\mathfrak{\mathfrak{F}}^{+\flat}\) validate precisely the same consecutions.

Proof. We know that the upsets with the given operations form a Heyting algebra. A routine verification shows that \(\mathrel{\mkern 1mu\underline{\mkern-1mu \sto\mkern-1mu}\mkern 1mu }^\flat\) satisfies [it:alg-ck], [it:alg-ct] and [it:alg-ci]. The second part of the lemma follows from the fact that valuations for \(\mathfrak{F}\) correspond bijectively with assignments in \(\mathfrak{\mathfrak{F}}^{+\flat}\), and that the interpretation of connectives in \(\mathfrak{F}\) corresponds to that in \(\mathfrak{\mathfrak{F}}^{+\flat}\). ◻

Combining Lemma 2 and algebraic soundness proves:

For any \(\mathrm{Ax}\subseteq \mathcal{L}_{\sto}\) and any \(\Gamma \cup \{ \varphi\} \subseteq \mathcal{L}_{\sto}\), we have that \(\Gamma \vdash_{\mathrm{Ax}} \varphi\) implies \(\Gamma \Vdash_{\mathrm{Ax}} \varphi\).

One might expect that, at least in the finite setting, turning such a complex algebra back into a flat frame should be straightforward, with join-prime elements providing the carrier set of the frame. Example 3 illustrates that this is not the case: the Heyting reduct of the dual algebra is the Boolean algebra with three atoms (join-primes). Collapsing the \(\{v,w\}\) cluster would change the equational theory. The right approach to duality, similar to the one pursued in [@Wij90; @groshiclo25], uses a suitable algebraic translation of the notion of the notion a segment introduced in Section 4, potentially blowing up the number of states (cf. estimates in the proof of Lemma 8). While many segments can often be eliminated (cf. Remark [rem:notall] and Section 5.2), care is needed.

3.2 Upward-flat frames↩︎

When only using the modal relation to interpret \(\sto\), we can make a simplification to our frames and assume that \(R[w]\) is an upset for each \(w\).

Definition 7. An upward-flat frame* is a flat frame \((W, \preceq, R)\) such that for all \(w, v, u \in W\), if \(w R v \preceq u\) then \(w R u\). A upward-flat model is a flat model whose underlying frame is upward-flat.*

The coherence condition on the relation can be read as \((R \circ {\preceq}) = R\). While not strictly required, it simplifies the correspondence results for some of the additional axioms we consider in Section 5.

Let \(\mathfrak{F} = (W, \preceq, R)\) be a flat frame. Define \(R_{\preceq} := R \circ {\preceq}\), i.e. \(w R_{\preceq} u\) if there exists a \(v\) such that \(w R v \preceq u\), and let \(\mathfrak{F}_{\preceq} = (W, \preceq, R_{\preceq})\). Then \(\mathfrak{F}\) and \(\mathfrak{F}_{\preceq}\) have the same complex algebra.

Proof. Let \(a\) be an upset of \((W, \preceq)\) and \(w \in W\). Then \(R[w] \subseteq a\) if and only if \(R_{\preceq}[w] \subseteq a\). This entails that the change from \(\mathfrak{F}\) to \(\mathfrak{F}_{\preceq}\) leaves the definition of \(\mathrel{\mkern 1mu\underline{\mkern-1mu \sto\mkern-1mu}\mkern 1mu }^\flat\) unchanged, so that \(\mathfrak{F}^{+\flat} = \mathfrak{(F_{\preceq})}^{+\flat}\). ◻

It is often easier to find and depict frame correspondence results for upward-flat frames than for arbitrary ones. The definition and proposition above show that these can always be transformed into arbitrary frame conditions: simply replace every occurrence of \(R\) with \((R \circ {\preceq})\). To illustrate the difference, consider the axiom \(\mathsf{4_a}: \varphi\sto (\top \sto \varphi)\).

A flat frame validates \(\mathsf{4_a}\) if and only if for all \(x, y, z, w\) such that \(x R y \preceq z R w\), there exists \(v\) such that \(x R v \preceq w\).
An upward-flat frame validates \(\mathsf{4_a}\) if and only if \(R\) is transitive.

Proof. (1) Suppose \(\mathfrak{W}\) validates \(\mathsf{4_a}\), and \(xRy\preceq z R w\) for some worlds \(x, y, z, w\). Let \(V\) be a valuation of \(p\) with \(V(p) = {\uparrow}R[x]\). Then all worlds in \(R[x]\) satisfy \(p\), so by assumption they also all satisfy \(\top \sto p\). In particular, \(y \Vdash \top \sto p\), and since \(y \preceq z\) and (trivially) all worlds in \(R[z]\) satisfy \(\top\), we must have \(w \Vdash p\). By definition, this means that \(w\) lies above some \(R\)-successor \(v\) of \(x\), as desired.

Conversely, suppose \(\mathfrak{W}\) satisfies the frame condition. Let \(x\) be any world. To show that it satisfies \(\mathsf{4_a}\), let \(x \preceq x'\) and suppose all worlds in \(R[x']\) satisfy \(p\). Then we need that all worlds in \(R[x']\) satisfy \(\top \sto p\). Let \(y\) be such a world. Since \(\top\) is always true, we need to prove that \(y \preceq z R w\) implies that \(w \Vdash p\). This follows from the frame condition. So \(\mathsf{4_a}\) is valid.

(2) This is a straightforward simplification of the above condition. For readers’ convenience, we provide a direct proof. Suppose \(R\) is transitive and let \(w\) be a world such that \(R[w] \subseteq V(p)\). Then by assumption \(R[R[w]] \subseteq \llbracket p \rrbracket\), and since \(wRv \preceq u R s\) implies \(w R u R s\) we have \(R[u] \subseteq \llbracket p \rrbracket\) for every \(u \in R[w]\), so that \(R[w] \subseteq \llbracket\top \sto p \rrbracket\). Conversely, suppose \(w R v R u\). Let \(V\) be a valuation such that \(V(p) = R[w]\). Then \(R[w] \subseteq V(p)\), so we must have \(R[w] \subseteq \llbracket\top \sto \varphi\rrbracket\). This forces \(R[R[w]] \subseteq V(p) = R[w]\). In particular, we have \(u \in R[R[w]] \subseteq R[w]\) so \(w R u\). Therefore \(R\) is transitive. ◻

3.3 Relation to sharp semantics↩︎

The sharp semantics for \(\mathsf{HLC^{\sharp}}\) can be embedded into flat semantics in a truth preserving way. This gives rise to a completeness result for \(\mathsf{HLC^{\sharp}}\) with respect to flat semantics. We start with a simple sufficient condition for a flat frame to validate \(\mathsf{di}\). Let us call a flat frame \(\mathfrak{F} = (W, \preceq, R)\) pointwise downward directed if \(R[w]\) is a downward directed subset of \((W, \preceq)\) for every \(w \in W\).

Lemma 3. If a flat frame \(\mathfrak{F} = (W, \preceq, R)\) is pointwise downward directed, then it validates \(\mathsf{di}\)

Proof. Suppose \(\mathfrak{F}\) is a flat frame that is pointwise downward directed, \(\mathfrak{M} = (\mathfrak{F}, V)\) is a flat model based on \(\mathfrak{F}\) and \(w \in W\) satisfies \(p \sto r\) and \(q \sto r\). Suppose \(w' \succeq w\) and \(R[w'] \subseteq \llbracket p \vee q \rrbracket= V(p) \cup V(q)\). We claim that either \(R[w'] \subseteq V(p)\) or \(R[w'] \subseteq V(q)\). If this is not the case, then we can find \(v, u \in R[w']\) such that \(v \notin V(p)\) and \(u \notin V(q)\). By assumption there exists some \(s \in R[w']\) such that \(s \preceq v\) and \(s \preceq u\). But then \(s \notin V(p) \cup V(q)\), a contradiction. So we must have \(R[w'] \subseteq V(p)\) or \(R[w'] \subseteq V(q)\). In either case, using the assumption yields \(R[w'] \subseteq V(r)\). This proves \(w \Vdash (p \vee q) \sto r\), and hence \(\mathsf{di}\) is valid on \(\mathfrak{F}\). ◻

Next, we turn a sharp model into a flat one. Intuitively, for each \(w\) we create a cluster such that each element of the cluster can modally access precisely one of the worlds in \(R[w]\).

Definition 8. Let \(\mathfrak{F} = (W, \leq, R, V)\) be a sharp frame and \(\bullet\) a symbol such that \(\bullet \notin W\). Define \(\mathfrak{F}^{\flat} = (W^{\flat}, \preceq, \mathcal{R}, V^{\flat})\), where \[\begin{align} &W^{\flat} := \{ (w, v) \mid w \in W \text{ and } w R v \} \cup \{ (w, \bullet) \mid w \in W \text{ and } R[w] = \emptyset \} \quad & (w, v) \preceq (w', v') &\quad\text{iff}\quad w \leq w' \\ &V^{\flat}(p) := \{ (w, v) \in W^{\flat} \mid w \in V(p) \} & (w, v) \mathcal{R} (w', v') &\quad\text{iff}\quad v \leq w' \end{align}\]

Note that the definition of \(\mathcal{R}\) ensures that \(\mathfrak{M}^{\flat}\) is and upward-flat model. Moreover, for each \((w, v) \in W^{\flat}\) we have that \(\mathcal{R}[(w, v)]\) is the upward closure (under \(\preceq\)) of \((v, u)\), for any \(u \in W \cup \{ \bullet \}\) such that \((v, u) \in W^{\flat}\). This implies that \(\mathfrak{M}\) is pointwise downward directed.

Let \(\mathfrak{M} = (W, \leq, R, V)\) be a sharp model, and \(\mathfrak{M}^{\flat} = (W^{\flat}, \preceq, \mathcal{R}, V^{\flat})\) the corresponding flat model. Then for all \((w, v) \in W^{\flat}\) and all formulas \(\varphi\), we have \(\mathfrak{M}, w \Vdash^s\varphi\) if and only if \(\mathfrak{M}^{\flat}, (w, v) \Vdash \varphi\).

Proof. We use induction on the \(\varphi\), showcasing only the induction step for \(\varphi= \psi \sto \chi\). Suppose \(\mathfrak{M}, w \Vdash^s \psi \sto \chi\). Suppose \((w, v) \preceq(w', v')\) and \(R[(w', v')] \subseteq \llbracket\psi \rrbracket^{\mathfrak{M}^{\flat}}\). Then \(w \leq w'\) and \(w'Rv'\), so \(wRv'\) because \(\mathfrak{M}\) is a sharp model. Also \(R[(w', v')] = \{ (u, s) \in W^{\flat} \mid v' \leq u \}\), so by the induction hypothesis we have \(\mathfrak{M}, v' \Vdash^s \psi\). The assumption that \(\mathfrak{M}, w \Vdash^s \psi \sto \chi\) then gives \(\mathfrak{M}, v' \Vdash^s \chi\), and intuitionistic heredity entails \(\mathfrak{M}, u \Vdash^s \chi\) for all \(u \geq v'\). Using induction again, this implies \(R[(w', v')] \subseteq \llbracket\chi \rrbracket^{\mathfrak{M}^{\flat}}\), and hence \(\mathfrak{M}^{\flat}, (w, v) \Vdash \psi \sto \chi\). Conversely, suppose \(\mathfrak{M}^{\flat}, (w, v) \Vdash \psi \sto \chi\) and suppose \(w R u\) and \(\mathfrak{M}, u \Vdash^s \psi\). Then \((w, v) \preceq (w, u)\) and by induction \(\mathcal{R}[(w, u)] \subseteq \llbracket\psi \rrbracket^{\mathfrak{M}^{\flat}}\). This implies \(\mathcal{R}[(w, u)] \subseteq \llbracket\chi \rrbracket^{\mathfrak{M}^{\flat}}\), and hence \(\mathfrak{M}, u \Vdash^s \chi\). Therefore \(\mathfrak{M}, w \Vdash^s \psi \sto \chi\). ◻

Combining the known completeness result for \(\mathsf{HLC^{\sharp}}\) with respect to sharp frames, the lemma and proposition above, and the fact that \(\mathfrak{M}^{\flat}\) is a pointwise downward directed upward-flat model, gives:

The logic \(\mathsf{HLC^{\sharp}}\) is sound and complete with respect to the class of pointwise downward directed flat frames.

4 Canonical models and completeness↩︎

We provide a canonical model construction relative to some set \(\Sigma\) that is closed under subformulas. This will give us, at once, the finite model property and strong completeness of the logic. We use a modification of the canonical model construction for \(\mathsf{CK}\), using so-called segments. The idea behind a segment is that it encodes both a world of the frame (a prime theory) as well as its successors. We start by defining prime \(\Sigma\)-theories. Throughout this subsection, we let \(\mathrm{Ax}\) be a consistent set of formulas, and \(\Sigma\) denote a set of formulas that contains \(\top\) and is closed under subformulas.

Definition 9. A prime \((\mathrm{Ax},\Sigma)\)-theory* is a subset \(\Gamma \subseteq \Sigma\) that is deductively closed (i.e. if \(\varphi\in \Sigma\) and \(\Gamma \vdash_{\mathrm{Ax}} \varphi\) then \(\varphi\in \Gamma\)), consistent (i.e. \(\Gamma \not\vdash_{\mathrm{Ax}} \bot\)), and \(\Sigma\)-prime (i.e. if \(\varphi_1, \ldots, \varphi_n \in \Sigma\) and \(\Gamma \vdash_{\mathrm{Ax}} \varphi_1 \vee \cdots \vee \varphi_n\) then \(\varphi_i \in \Gamma\) for some \(i \in \{ 1, \ldots, n \}\)). Write \(\mathrm{Th}_{\mathrm{Ax},\Sigma}\) for the set of prime \((\mathrm{Ax},\Sigma)\)-theories. If \(\Sigma = \mathcal{L}_{\sto}\) then we omit reference to \(\Sigma\) and simply write prime \(\mathrm{Ax}\)-theory instead of prime \((\mathrm{Ax},\Sigma)\)-theory.*

The Lindenbaum lemma can be proved as usual. We can use it to obtain prime \((\mathrm{Ax}, \Sigma)\)-theories by taking the intersection of the resulting prime \(\mathrm{Ax}\)-theory with \(\Sigma\).

Lemma 4 (Lindenbaum lemma). Let \(\Gamma \cup \Delta \subseteq \mathcal{L}_{\sto}\) and suppose \(\Gamma \not\vdash_{\mathrm{Ax}} \Delta\). Then there exists a prime theory \(\Gamma'\) such that \(\Gamma \subseteq \Gamma'\) and \(\Gamma' \cap \Delta = \emptyset\).

Lemma 5. If \(\Gamma\) is a prime \(\mathrm{Ax}\)-theory, then \(\Gamma \cap \Sigma\) is a prime \((\mathrm{Ax},\Sigma)\)-theory.

Segments comprise of a prime \((\mathrm{Ax},\Sigma)\)-theory together with a suitable set of such theories that encodes the successors of the segment.

Definition 10. An \((\mathrm{Ax},\Sigma)\)-segment* is a pair \((\Gamma, U)\) where \(\{ \Gamma \} \cup U \subseteq \mathrm{Th}_{\mathrm{Ax},\Sigma}\) such that*

if \(\Delta \in U\) and \(\Delta \subseteq \Delta' \in \mathrm{Th}_{\mathrm{Ax},\Sigma}\) then \(\Delta' \in U\);
for all \(\varphi, \psi \in \Sigma\), if \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi\) and \(\varphi\in \Delta\) for all \(\Delta \in U\), then \(\psi \in \Delta\) for all \(\Delta \in U\).

Let \(\mathrm{SEG}_{\mathrm{Ax},\Sigma}\) be the set of \((\mathrm{Ax},\Sigma)\)-segments and define relations by setting \((\Gamma, U) \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}(\Gamma', U')\) iff \(\Gamma \subseteq \Gamma'\), and \((\Gamma, U) \mathcal{R} (\Gamma', U')\) iff \(\Gamma' \in U\). Define the (canonical) valuation by \(V_{\mathrm{Ax},\Sigma}(p) = \{ (\Gamma, U) \in \mathrm{SEG}_{\mathrm{Ax},\Sigma} \mid p \in \Gamma \}\). Then \[\mathfrak{F}_{\mathrm{Ax},\Sigma} = (\mathrm{SEG}_{\mathrm{Ax},\Sigma}, \subseteq, \mathcal{R}) \quad\text{and}\quad \mathfrak{M}_{\mathrm{Ax},\Sigma} = (\mathrm{SEG}_{\mathrm{Ax},\Sigma}, \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}, \mathcal{R}, V_{\mathrm{Ax},\Sigma})\] are an upward-flat frame and model, called the full canonical frame and model (with respect to \(\mathrm{Ax}\) and \(\Sigma\)). If \(\Sigma = \mathcal{L}_{\sto}\) then we abbreviate \(\mathrm{SEG}_{\mathrm{Ax}} := \mathrm{SEG}_{\mathrm{Ax}, \mathcal{L}_{\sto}}\) and \(\mathfrak{F}_{\mathrm{Ax}} := \mathfrak{F}_{\mathrm{Ax}, \mathcal{L}_{\sto}}\).

Lemmas 4 and 5 provide a way to construct prime \((\mathrm{Ax},\Sigma)\)-theories, given suitable sets of formulas. The following lemma allows us to extend this to a segment:

Lemma 6. Let \(\Gamma\) be a prime \((\mathrm{Ax},\Sigma)\)-theory and \(\varphi\in \Sigma\), and define \[U_{\Gamma, \varphi} := \{ \Delta \in \mathrm{Th}_{\mathrm{Ax},\Sigma} \mid \text{if } \psi \in \Sigma \text{ and } \Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi \text{ then } \psi \in \Delta \}.\]

\((\Gamma, U_{\Gamma, \varphi})\) is an \((\mathrm{Ax},\Sigma)\)-segment.
\(\varphi\in \Delta\) for all \(\Delta \in U_{\Gamma, \varphi}\).
If \(\theta \in \Sigma\) is such that \(\Gamma \not\vdash_{\mathrm{Ax}} \varphi\sto \theta\), then there exists \(\Delta \in U_{\Gamma, \varphi}\) such that \(\theta \notin \Delta\).

Proof. (1) It follows immediately from the definition that \((\Gamma, U_{\Gamma, \varphi})\) satisfies [it:seg-1], so we focus on proving [it:seg-2]. Suppose \(\chi, \xi \in \Sigma\) and \(\Gamma \vdash_{\mathrm{Ax}} \chi \sto \xi\) and \(\chi \in \Delta\) for all \(\Delta \in U_{\Gamma, \varphi}\). Then we must have \[\{ \psi \in \Sigma \mid \Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi \} \vdash \chi,\] because otherwise we could use the Lindenbaum lemma to find some prime \(\Sigma\)-theory in \(U_{\Gamma, \varphi}\) that does not contain \(\chi\). (We can first use the usual Lindenbaum lemma to find a prime theory containing the LHS but not \(\varphi\), and then take its intersection with \(\Sigma\).) By compactness, we can find \(\psi_1, \ldots, \psi_n \in \Sigma\) such that \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi_i\) for all \(i \in \{ 1, \ldots, n \}\) and \(\psi_1, \ldots, \psi_n \vdash_{\mathrm{Ax}} \chi\). This implies \[\varphi\sto \psi_1, \ldots, \varphi\sto \psi_n \vdash_{\mathrm{Ax}} \varphi\sto \chi,\] hence using transitivity \[\varphi\sto \psi_1, \ldots, \varphi\sto \psi_n, \chi \sto \xi \vdash_{\mathrm{Ax}} \varphi\sto \xi,.\] Since \(\Gamma\) derives everything on the LHS, we also get \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \xi\), hence by definition of \(U_{\Gamma, \varphi}\) we have \(\xi \in \Delta\) for all \(\Delta \in U_{\Gamma, \varphi}\).

(2) This follows from the fact (\(\mathsf{N_a}\)) entails \(\vdash \varphi\sto \varphi\) for any \(\varphi\in \mathcal{L}_{\sto}\). Therefore \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \varphi\) and hence \(\varphi\in \Delta\) for all \(\Delta \in U_{\Gamma, \varphi}\) by definition.

(3) We claim that \(\{ \psi \in \Sigma \mid \Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi \} \not\vdash_{\mathrm{Ax}} \theta\). Suppose towards a contradiction that this is not the case. Then by compactness we can find \(\psi_1, \ldots, \psi_n \in \Sigma\) such that \[\label{eq:3} \psi_1, \ldots, \psi_n \vdash_{\mathrm{Ax}} \theta\tag{1}\] and \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi_i\) for each \(i \in \{ 1, \ldots, n \}\). This implies \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto (\psi_1 \wedge \cdots \wedge \psi_n)\). Furthermore, 1 entails \(\vdash_{\mathrm{Ax}} (\psi_1 \wedge \cdots \wedge \psi_n) \to \theta\), so by (\(\mathsf{N_a}\)) we get \(\vdash_{\mathrm{Ax}} (\psi_1 \wedge \cdots \wedge \psi_n) \sto \theta\). In particular, this gives \(\Gamma \vdash_{\mathrm{Ax}} (\psi_1 \wedge \cdots \wedge \psi_n) \sto \theta\), so that \(\mathsf{tr}\) entails \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \theta\), a contradiction. So we have \(\{ \psi \in \Sigma \mid \Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi \} \not\vdash_{\mathrm{Ax}} \theta\). Then Lemma 4 gives a prime \(\mathrm{Ax}\)-theory \(\Delta\) containing \(\psi\) for every \(\psi \in \Sigma\) such that \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi\), but not \(\theta\). By definition \(\Delta \cap \Sigma \in U_{\Gamma, \varphi}\), so it is the desired witness. ◻

Lemma 7. For all \(\varphi\in \Sigma\) and \((\Gamma, U) \in \mathrm{SEG}_{\mathrm{Ax},\Sigma}\) we have \(\mathfrak{M}_{\mathrm{Ax},\Sigma}, (\Gamma, U) \Vdash \varphi\) iff \(\varphi\in \Gamma\).

Proof. We use induction on the structure of \(\varphi\). If \(\varphi\) is \(\top, \bot\) or a proposition letter, the statement is immediate. The cases for \(\wedge\) and \(\vee\) follow using induction and the fact that \(\Gamma\) is prime.

Case \(\varphi= \psi \to \chi\). Suppose \(\psi \to \chi \in \Gamma\). Let \((\Gamma, U) \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}(\Gamma', U')\) and suppose \((\Gamma', U') \Vdash \psi\). Then by definition of \(\mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}\), deductive closure of prime \((\mathrm{Ax},\Sigma)\)-theories, and the induction hypothesis we find \(\psi \in \Gamma'\) and \(\psi \to \chi \in \Gamma'\). This implies \(\chi \in \Gamma'\), hence by induction \((\Gamma', U') \Vdash \chi\). This proves \((\Gamma, U) \Vdash \psi \to \chi\).

Conversely, suppose \(\psi \to \chi \notin \Gamma\). Then \(\Gamma \not\vdash_{\mathrm{Ax}} \psi \to \chi\), so \(\Gamma, \psi \not\vdash_{\mathrm{Ax}} \chi\) and we can find a prime theory \(\Gamma'\) containing \(\Gamma, \psi\) but not \(\chi\). Then \(\Gamma' \cap \Sigma\) is a prime \(\Sigma\)-theory and we can extend it to an \((\mathrm{Ax},\Sigma)\)-segment (for example by using Lemma 6 with \(\varphi= \top\)) which (using induction) satisfies \(\psi\) but not \(\chi\). Therefore \((\Gamma, U) \not\Vdash \psi \to \chi\).

Case \(\varphi= \psi \sto \chi\). If \(\psi \sto \chi \in \Gamma\) then we get \((\Gamma, U) \Vdash \psi \sto \chi\) immediately from the definition of a segment. Now suppose \(\psi \sto \chi \notin \Gamma\). By Lemma 6 \((\Gamma, U_{\Gamma, \psi})\) is a \((\mathrm{Ax},\Sigma)\)-segment such that \(\psi \in \Delta\) for all \(\Delta \in U_{\Gamma, \psi}\) while \(\chi \notin \Delta\) for some \(\Delta \in U_{\Gamma, \psi}\). Since each \(\Delta\) can be extended to a segment, this proves \((\Gamma, U) \not\Vdash \psi \sto \chi\). ◻

Depending on our choice of \(\mathrm{Ax}\) and \(\Sigma\), the canonical model construction gives rise to a finite model property and a strong completeness result.

Lemma 8. Let \(\mathrm{Ax}\) be a set of axioms.

Suppose that for every finite consecution \(\Gamma \Rightarrow\varphi\) there exists a finite subformula-closed set \(\Sigma\) that contains \(\Gamma, \varphi\) and \(\top\) such that \(\mathfrak{F}_{\mathrm{Ax},\Sigma}\) validates \(\mathrm{Ax}\). Then \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) has the finite model property.
Suppose \(\mathfrak{F}_{\mathrm{Ax}}\) validates \(\mathrm{Ax}\). Then \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) is strongly complete with respect to the class of (upward-)flat frames validating \(\mathrm{Ax}\).

Proof. (1) Let \(\Gamma \cup \{ \varphi\}\) be a finite set of formulas and suppose \(\Gamma \not\vdash_{\mathrm{Ax}} \varphi\). Let \(\Sigma\) be as described. Then we can use Lemmas 4 and 5 to construct a prime \(\Sigma\)-theory \(\Gamma'\) extending \(\Gamma\) that does not contain \(\varphi\). Let \((\Gamma', U)\) be a segment in \(\mathrm{SEG}_{\mathrm{Ax},\Sigma}\). It follows from Lemma 7 that that \(\mathfrak{M}_{\Sigma}, (\Gamma', U) \Vdash \psi\) for all \(\psi \in \Gamma\) and \(\mathfrak{M}_{\Sigma}, (\Gamma', U) \not\Vdash \varphi\). So \(\mathfrak{M}_{\Sigma} \not\Vdash \Gamma \Rightarrow\varphi\), hence \(\mathfrak{F}_{\mathrm{Ax},\Sigma}\) is a flat frame that does not validate \(\Gamma \Rightarrow\varphi\).

By assumption \(\Sigma\) is finite. A prime \(\Sigma\)-theory is a subset of \(\Sigma\), so we have at most \(2^{|\Sigma|}\) many prime theories, and hence at most \(2^{|\Sigma|} \times 2^{2^{|\Sigma|}}\) \(\Sigma\)-segments, where \(|\Sigma|\) denotes the size of \(\Sigma\). Hence \(\mathfrak{F}_{\Sigma}\) is finite.

(2) The proof is identical to the first paragraph of item (1) with \(\Sigma = \mathcal{L}_{\sto}\). ◻

Taking \(\mathrm{Ax}= \emptyset\) and \(\Sigma\) the closure of \(\Gamma \cup \{ \varphi, \top \}\) under subformulas yields:

Theorem 2. The logic \(\mathsf{HLC^{\flat}}\) has the finite model property and is strongly complete with respect to the class of (upward-)flat frames.

While taking the collection of all \((\mathrm{Ax}, \Sigma)\)-segments in Definition 10 provides a canonical choice of segments, it is not strictly necessary. Analogous to [@groshiclo25], we can restrict the shape of segments we use while maintaining the truth lemma and completeness result. This can help create a canonical model that satisfies additional constraints. We will see an example of a restriction in Section 5.2, where we use this strategy to ensure that the modal accessibility relation is transitive when having \(\mathsf{4_a}\) as an axiom.

A different method for obtaining completeness results, employed for instance for \(\mathsf{HLC^{\sharp}}\) [@grolitpat26-arxiv] and intuitionistic modal logic with a \(\Box\) [@wolterz97:al; @wolterz98:lw], is via a Gödel-McKinsey-Tarski translation into classical bimodal logic with an S4-box \(\Box_i\) and a normal box \(\Box_m\). Our case seems amenable to this treatment: flat frames corresponds precisely to the semantics of \(\mathsf{S4 \oplus K}\), and the interpretation of \(\varphi\sto \psi\) is given by \(\Box_i(\Box_m\varphi\to \Box_m\psi)\). However, there is a mismatch between the descriptive frames of both logics: a duality for \(\mathsf{HLC^{\flat}}\) would resemble that for \(\mathsf{CK}\) [@groshiclo26] and use segments. As a consequence it does not seem to be the case that the two types of descriptive frames line up. This frustrates the transfer of e.g. completeness.

5 Completeness and the fmp for axiomatic extensions↩︎

We investigate the extension of \(\mathsf{HLC^{\flat}}\) with the axioms listed in Table 1 and the given correspondence conditions proven in Lemma 9 and Proposition [prop:fourcor]. We start by using Lemma 8 to obtain completeness and the finite model property for certain extensions of \(\mathsf{HLC^{\flat}}\) with the listed axioms. In Section 5.2 we modify this canonical model construction to obtain completeness for extensions that include \(\mathsf{4_a}\), and to obtain the finite model property for \(\mathsf{HLC^{\flat}}\oplus \mathsf{t_{\Box}}\oplus \mathsf{4_a}\).

Table 1: Five axioms and their correspondents for upward-flat frames \(\mo{F} = (W, \fleq, R)\).
Axiom	Formula	Upward-flat correspondent
\(\axEm\)	\(p \vee \neg p\)	\(\fleq\) is symmetric
\(\axTb\)	\((\top \sto p) \to p\)	\(({\fleq} \circ R)\) is reflexive
\(\foura\)	\(p \sto (\top \sto p)\)	\(R\) is transitive
\(\strength\)	\((p \to q) \to (p \sto q)\)	\(wRv\) implies \(w \fleq v\)
\(\pa\)	\((p \sto q) \to (\top \sto (p \sto q))\)	if \(wRvRs\) then there exists \(u \fgeq w\)
		such that \(uRs\) and \(R[u] \subseteq R[v]\)

Both \(\mathsf{4_a}\) and \(\mathsf{p_a}\) often occur in arithmetical contexts. It is worth noting that while \(\mathsf{4_a}\) is the “flat” correspondent of transitivity, \(\mathsf{p_a}\) is the “sharp” one [@litvis24]. While \(\mathsf{str}\) is a rather degenerate axiom classically (cf. Remark [rem:degstr]), intuitionistically it plays an important role, occurring in the logics of Haskell arrows [@Hug04], guarded (co)recursion, and entailments [@grolitpat26-arxiv], and even allows a non-trivial arithmetical interpretation as completeness principle.

Lemma 9. Let \(\mathfrak{F} = (W, \preceq, R)\) be an upward-flat frame. Then

\(\mathfrak{F}\) validates \(\mathsf{em}\) if and only if \(\preceq\) is symmetric;
\(\mathfrak{F}\) validates \(\mathsf{t_{\Box}}\) if and only if for all \(w\) there exists \(v\) such that \(w \preceq v R w\);
\(\mathfrak{F}\) validates \(\mathsf{str}\) if and only if \(w R v\) implies \(w \preceq v\);
\(\mathfrak{F}\) validates \(\mathsf{p_a}\) if and only if for all \(w, v, s\) satisfying \(w R v R s\) there exists \(u \succeq w\) such that \(s \in R[u]\) and \(R[u] \subseteq R[v]\).

Proof. [it:corr-em] Suppose \(\preceq\) is symmetric. Let \(V\) be any valuation and suppose \(w \in W\) does not satisfy \(p\). Then for all \(v \succeq w\) we have \(v \preceq w\) by symmetry, so \(v \not\Vdash p\). This proves \(w \Vdash \neg p\). Therefore \(\mathsf{em}\) is valid. For the converse, suppose the frame condition does not hold, so there exist \(v, w\) such that \(w \preceq v\) and \(v \not\preceq w\). Let \(V\) be a valuation such that \(V(p) = {\uparrow}v\). Then \(w \not\Vdash p\) because \(w \notin V(p)\) and \(w \not\Vdash \neg p\) because \(w \preceq v \Vdash p\), so \(\mathsf{em}\) fails.

[it:corr-tb] Suppose the frame condition holds and let \(V\) be any valuation. If \(w \Vdash \top \sto p\) then for all \(v \succeq w\) we have \(R[v] \subseteq p\). By assumption there exists such a \(v\) such that \(w \in R[v]\), hence \(w \Vdash p\). Therefore \(\mathsf{t_{\Box}}\) is valid. Conversely, suppose \(\mathsf{t_{\Box}}\) is valid. Let \(w\) be any world. Let \(V\) be a valuation such that \(V(p) = \bigcup \{ R[v] \mid v \succeq w \}\). Then \(w \Vdash \top \sto p\), hence \(w \Vdash p\), so we must have \(w \in R[v]\) for some \(v \succeq w\), as desired.

[it:corr-str] Suppose \(R \subseteq {\preceq}\), let \(V\) be any valuation, and \(w \Vdash p \to q\). If \(w \preceq v\) and \(R[v] \subseteq V(p)\) then by assumption \(w \preceq u\) for all \(u \in R[v]\), hence \(u \Vdash q\) for all such \(u\), so that \(R[v] \subseteq V(q)\). This proves \(w \Vdash p \sto q\), so \(\mathsf{str}\) is valid. For the converse, suppose the frame condition does not hold. Then we can find \(w, v \in W\) such that \(w R v\) while \(w \not\preceq v\). Let \(V\) be a valuation such that \(V(p) = R[w]\) and \(V(q) = {\uparrow}w\). (Recall that \(R[w]\) is upwards closed in upward-flat frames.) Then \(w\) trivially satisfies \(p \to q\), but \(w \not\Vdash p \sto q\) because all modal successors of \(w\) satisfy \(p\), but not all of them satisfy \(q\) (namely \(v\) does not satisfy \(q\)).

[it:corr-pa] Suppose the frame condition holds, and let \(V\) be any valuation. Suppose \(w \Vdash p \sto q\). To show that \(w \Vdash \top \sto (p \sto q)\), we need to prove that \(w \preceq w' R v\) implies \(v \Vdash p \sto q\). To this end, let \(v' \succeq v\) and assume \(R[v'] \subseteq V(p)\). Then because the frame is upward-flat we have \(w' R v'\). Now let \(s \in R[v']\). Then by assumption there exists some \(u \succeq w'\) such that \(s \in R[u] \subseteq R[v']\) Since \(w \Vdash p \sto q\) and \(R[u] \subseteq V(p)\) we find \(s \Vdash q\). This entails that \(R[v'] \subseteq V(q)\), so \(v \Vdash p \sto q\), as desired.

Conversely, if the frame condition does not hold then we can find \(w, v, s\) such that \(wRvRs\) and for all \(u \succeq w\) either \(R[u] \not\subseteq R[v]\) or \(s \notin R[u]\). Taking \(V(p) = R[v]\) and \(V(q) = R[v] \setminus {\downarrow}s\) then gives \(w \Vdash p \sto q\), because \(R[u] \not\subseteq V(p)\) for all \(u \succeq w\), while \(v \not\Vdash p \sto q\), so \(w \not\Vdash \top \sto (p \sto q)\). ◻

5.1 Reusing the full canonical model↩︎

We begin by focussing on \(\mathsf{em}, \mathsf{t_{\Box}}, \mathsf{str}\) and \(\mathsf{p_a}\). Towards proving completeness and the finite model property for some extensions of \(\mathsf{HLC^{\flat}}\) with these axioms, we give conditions on \(\Sigma\) that guarantee that the canonical frame \(\mathfrak{F}_{\mathrm{Ax}, \Sigma}\) satisfies the correspondence conditions derived in Lemma 9. To this end, we use the following definition of single negations: if \(\varphi\) is a formula then its single negation \(\mathord{\sim}\varphi\) is defined as \(\mathord{\sim}\varphi= \psi\) if \(\varphi= \neg\psi\) for some \(\psi \in \mathcal{L}_{\sto}\), and \(\mathord{\sim}\varphi= \neg\varphi\) otherwise. We say that a set \(\Sigma\) is closed under single negations if \(\varphi\in \Sigma\) implies \(\mathord{\sim}\varphi\in \Sigma\).

Lemma 10. Let \(\mathrm{Ax}\) be a set of axioms, \(\Sigma \subseteq \mathcal{L}_{\sto}\) a set of formulas that is closed under subformulas, and \(\mathfrak{F}_{\mathrm{Ax}, \Sigma} = (\mathrm{SEG}_{\mathrm{Ax}, \Sigma}, \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}, \mathcal{R})\) the canonical frame generated by \(\mathrm{Ax}\) and \(\Sigma\).

If \(\Sigma\) is closed under single negations and \(\mathsf{em}\in \mathrm{Ax}\), then \(\mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}\) is symmetric.
If \(\mathsf{t_{\Box}}\in \mathrm{Ax}\) then for all \((\Gamma, U) \in \mathrm{SEG}_{\mathrm{Ax}, \Sigma}\) there exists \((\Delta, D)\) such that \((\Gamma, U) \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}(\Delta, D) \mathcal{R} (\Gamma, U)\).
If \(\mathsf{str}\in \mathrm{Ax}\) then \((\Gamma, U) \mathcal{R} (\Gamma', U')\) implies \((\Gamma, U) \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}(\Gamma', U')\)
If \(\Sigma = \mathcal{L}_{\sto}\) and \(\mathsf{p_a}\in \mathrm{Ax}\) then \(\mathfrak{F}_{\mathrm{Ax}}\) satisfies the correspondence condition for \(\mathsf{p_a}\).

Proof. (1) Suppose \((\Gamma, U) \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}(\Gamma', U')\). Then \(\varphi\in \Gamma'\) implies \(\mathord{\sim}\varphi\notin \Gamma'\). Since \(\Gamma \subseteq \Gamma'\) this gives \(\mathord{\sim}\varphi\notin \Gamma\), hence \(\varphi\in \Gamma\).

(2) We can take \((\Delta, D) = (\Gamma, U_{\Gamma,\top})\). Then \((\Gamma, U) \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}(\Gamma, U_{\Gamma,\top})\), and it follows from \(\mathsf{t_{\Box}}\) that \(\Gamma \in U_{\Gamma,\top}\).

(3) Suppose \((\Gamma, U) \mathcal{R} (\Gamma', U')\). Then \(\varphi\in \Gamma\) implies \(\Gamma \vdash_{\mathrm{Ax}} \top \to \varphi\), hence using \(\mathsf{str}\) we get \(\Gamma \vdash_{\mathrm{Ax}} \top \sto \varphi\). By definition of an \((\mathrm{Ax}, \Sigma)\)-segment, this implies that \(\varphi\in \Delta\) for all \(\Delta \in U\). It follows that \(\Gamma \subseteq \Delta\) for all \(\Delta \in U\). In particular, this implies \(\Gamma \subseteq \Gamma'\), hence \((\Gamma, U) \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}(\Gamma', U')\).

(4) Suppose \((\Gamma, U) \mathcal{R} (\Delta, D)\). Then \(\varphi\sto \psi \in \Gamma\) implies \(\top \sto (\varphi\sto \psi) \in \Gamma\), so that \(\varphi\sto \psi \in \Delta\). It follows that \((\Gamma, D)\) is a segment. This implies the correspondence condition, because for any \(s\) is the correspondence condition we can take \(u = (\Gamma, D)\). ◻

Theorem 3. Let \(\mathrm{Ax}\subseteq \{ \mathsf{em}, \mathsf{t_{\Box}}, \mathsf{str}, \mathsf{p_a}\}\). Then \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) is sound and strongly complete with respect to the class of (upward-)flat frames on which they are valid.

Proof. Combine Lemma 8 [it:comp] and Lemma 10. ◻

Theorem 4. Let \(\mathrm{Ax}\subseteq \{ \mathsf{em}, \mathsf{t_{\Box}}, \mathsf{str}\}\). Then \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) has the finite model property.

Proof. Use Lemma 8 [it:fmp], taking \(\Sigma\) to be the closure under subformulas and under single negations of \(\Gamma \cup \{ \varphi\}\). This is finite when \(\Gamma\) is finite. Lemma 10 shows that \(\mathfrak{F}_{\mathrm{Ax}, \Sigma}\) validates the required axiom(s). ◻

Remark [rem:axmeaning] indicates that each of the axioms taken in separation and even several surprising combinations thereof (for example \(\mathsf{em}\oplus \mathsf{p_a}\)) are of independent interest. In the presence of \(\mathsf{str}\), however, certain careless combinations may degenerate. Still, such proofs of degeneracy may also illustrate convenience of our semantics.

We note that \(\mathsf{HLC^{\flat}}\oplus \mathsf{em}\oplus \mathsf{str}\) is rather degenerate, reducing not only to its own \(\Box\)-fragment, but in fact further still to the classical propositional calculus enriched with a single constant: One can show that \(p \sto q\) is equivalent to \((p \to q) \vee \Box\bot\). While the algebraic proof is very simple, our semantics allows an even more perspicuous argument: In upward-flat frames for this system, \(\preceq\) is an equivalence relation and \(R \subseteq {\preceq}\). In those clusters where \(R\) is non-empty, \(p \sto q\) is the same as \(p \to q\), and otherwise it reduces to \(\top \sto\bot\), which in such degenerate clusters is equivalent to \(\top\) (and elsewhere to \(\bot\)).

In the logic \(\mathsf{HLC^{\flat}}\oplus \mathsf{t_{\Box}}\oplus \mathsf{str}\) strict implication collapses to \(\to\). To see this, note that \(\mathsf{str}\) already gives \((p \to q) \to (p \sto q)\). Combining the correspondence conditions for \(\mathsf{str}\) and \(\mathsf{t_{\Box}}\) gives: \(R \subseteq {\preceq}\) and for every \(w \in W\) there exists some \(w'\) in the same \(\preceq\)-cluster (i.e. \(w \preceq w' \preceq w\)) such that \(R[w'] = {\uparrow}_{\preceq} w\). Let us verify that this entails \((p \sto q) \to (p \to q)\).

Let \(w\) be a world in an upward-flat model such that \(w \Vdash p \sto q\) and let \(v \succeq w\) be a world that satisfies \(p\). Then we can find some \(v'\) in the same cluster as \(v\) such that \(R[v'] = {\uparrow}_{\preceq}v\). By assumption and intuitionistic heredity we then get \(R[v'] \subseteq V(p)\), and since \(w \preceq v'\) and \(w \Vdash p \sto q\) this implies \(R[v'] \subseteq V(q)\). In particular, this gives \(v \Vdash q\), so it follows that \(w \Vdash p \to q\).

5.2 Modifying the full canonical model↩︎

We turn our attention to extensions of \(\mathsf{HLC^{\flat}}\) with sets of axioms that include \(\mathsf{4_a}\). Recall that on upward-flat frames, \(\mathsf{4_a}\) corresponds to transitivity of the modal accessibility relation. The following example illustrates that we cannot use the full canonical model construction from Section 4.

Example 1. Let \(\mathrm{Ax}= \{ \mathsf{4_a}\}\) and consider \(\Sigma = \{ \top, q \}\). Then we have two prime \(\Sigma\)-theories, \(\{ \top \}\) and \(\{ \top, q \}\). Let \(\{ \Gamma \} \cup U \subseteq \{ \{ \top \}, \{ \top, q \} \}\) and suppose \(U\) is upwards closed under inclusion. In order for \((\Gamma, U)\) to be an \((\mathrm{Ax},\Sigma)\)-segment, we need to show that for all \(\varphi, \psi \in \{ \top, q \}\), if \(\Gamma \vdash_{\mathrm{Ax}} \varphi\sto \psi\) and \(\varphi\in \Delta\) for all \(\Delta \in U\), then \(\psi \in \Delta\) for all \(\Delta \in U\). This gives four cases, \(\top \sto q\), \(q \sto \top\), \(q \sto q\) and \(\top \sto \top\). The desired condition is clearly satisfied for the latter three, and a simple countermodel shows that \(\Gamma \not\vdash_{\mathrm{Ax}} \top \sto q\) for either choice of \(\Gamma\). Therefore \((\Gamma, U)\) is an \((\mathrm{Ax}, \Sigma)\)-segment for any choice of \(\Gamma\) and \(U\).

In particular, this shows that for \(\Gamma := \{ \top \}\) and \(\Delta := \{ \top, q \}\) we have \((\Gamma, \{ \Delta \}) \mathcal{R} (\Delta, \{ \Gamma, \Delta \}) \mathcal{R} (\Gamma, \emptyset)\) while \((\Gamma, \emptyset)\) is not modally accessible from \((\Gamma, \{ \Delta \})\). So the modal accessibility relation \(\mathcal{R}\) of the full canonical frame \(\mathfrak{F}_{\mathrm{Ax},\Sigma}\) is not transitive, hence \(\mathfrak{F}_{\mathrm{Ax},\Sigma}\) does not validate \(\mathsf{4_a}\).

In order to prove completeness for extensions of \(\mathsf{HLC^{\flat}}\) with \(\mathsf{4_a}\), we used a trimmed version of the canonical model construction from Section 4. This is obtained by restricting the set \(\mathrm{SEG}_{\mathrm{Ax},\Sigma}\).

Definition 11. Let \(\mathrm{Ax}\) be a consistent set of axioms and \(\Sigma\) a set of formulas that is closed under subformulas and contains \(\top\). We call an \((\mathrm{Ax}, \Sigma)\)-segment \((\Gamma, U)\) pointed* if there exists a formula \(\gamma \in \Sigma\) such that \[U = U_{\Gamma, \gamma} := \{ \Delta \in \mathrm{Th}_{\mathrm{Ax},\Sigma} \mid \text{if } \psi \in \Sigma \text{ and } \Gamma \vdash_{\mathrm{Ax}} \gamma \sto \psi \text{ then } \psi \in \Delta \}.\] By Lemma 6, every prime \((\mathrm{Ax}, \Sigma)\)-theory can be extended to a pointed \((\mathrm{Ax}, \Sigma)\)-segment.*

Write \(\mathrm{SEG}^p_{\mathrm{Ax},\Sigma}\) for the set of pointed \((\mathrm{Ax},\Sigma)\)-segments, and \(\mathfrak{F}_{\mathrm{Ax},\Sigma}^p := (\mathrm{SEG}^p_{\mathrm{Ax},\Sigma}, \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}, \mathcal{R})\) and \(\mathfrak{M}_{\mathrm{Ax},\Sigma}^p := (\mathfrak{F}_{\mathrm{Ax},\Sigma}^p, V_{\mathrm{Ax},\Sigma})\) for the pointed canonical frame* and model. If \(\Sigma = \mathcal{L}_{\sto}\) we abbreviate \(\mathfrak{F}_{\mathrm{Ax}}^p := \mathfrak{F}_{\mathrm{Ax}, \mathcal{L}_{\sto}}^p\).*

Using precisely the same proof as Lemma 7, we get

Lemma 11. Let \(\mathrm{Ax}\subseteq \mathcal{L}_{\sto}\) be a set of axioms and \(\Sigma \subseteq \mathcal{L}_{\sto}\) a set of formulas that contains \(\top\) and is closed under subformulas. Then for all \(\varphi\in \Sigma\) and \((\Gamma, U) \in \mathrm{SEG}_{\mathrm{Ax},\Sigma}\) we have \(\mathfrak{M}_{\mathrm{Ax},\Sigma}, (\Gamma, U) \Vdash \varphi\) iff \(\varphi\in \Gamma\).

Theorem 5. Let \(\mathrm{Ax}\subseteq \{ \mathsf{em}, \mathsf{t_{\Box}}, \mathsf{str}, \mathsf{4_a}\}\). Then \(\mathsf{HLC^{\flat}}\oplus \mathrm{Ax}\) is sound and strongly complete with respect to the class of (upward-)flat frames on which \(\mathrm{Ax}\) is valid.

Proof. It suffices to show that \(\mathfrak{F}_{\mathrm{Ax}}^p\) validates each of the axioms in \(\mathrm{Ax}\). Using the same proof as in Lemma 10 shows that if \(\mathsf{em}, \mathsf{t_{\Box}}\) or \(\mathsf{str}\) is in \(\mathrm{Ax}\), then \(\mathfrak{F}_{\mathrm{Ax}}^p\) validates it, so we are left to consider \(\mathsf{4_a}\). Suppose \(\mathsf{4_a}\in \mathrm{Ax}\). We need to show that \(\mathcal{R}\) is transitive. To this end, let \((\Gamma, U_{\Gamma, \gamma}) \mathcal{R} (\Delta, U_{\Delta,\delta}) \mathcal{R} (\Pi, U_{\Pi,\pi})\) in \(\mathfrak{F}_{\mathrm{Ax}}^p\). Suppose \(\gamma \sto \psi \in \Gamma\). By \(\mathsf{4_a}\) we also have \(\psi \sto (\top \sto \psi) \in \Gamma\), so \(\mathsf{tr}\) gives \(\gamma \sto (\top \sto \psi) \in \Gamma\). This entails \(\top \sto \psi \in \Delta\), which by the definition of a segment gives \(\psi \in \Pi\). This proves that \(\Pi \in U_{\Gamma, \gamma}\), so that \((\Gamma, U_{\Gamma, \gamma}) \mathcal{R} (\Pi, U_{\Pi,\pi})\), as desired. ◻

Finally, using the same kind of canonical model we derive the finite model property for the logic \(\mathsf{HLC^{\flat}}\oplus \mathsf{t_{\Box}}\oplus \mathsf{4_a}\). The key insight towards this is that \(\top \sto \varphi\) is equivalent to \(\top \sto (\top \sto \varphi)\) in this logic, so that it suffices to close \(\Sigma\) under “single boxes.”

Lemma 12. We have \(\vdash_{\mathsf{t_{\Box}},\mathsf{4_a}} (\top \sto \varphi) \leftrightarrow (\top \sto (\top \sto \varphi))\).

Proof. As a substitution instance of \(\mathsf{t_{\Box}}\) we get \(\vdash_{\mathsf{t_{\Box}},\mathsf{4_a}} (\top \sto (\top \sto \varphi)) \to (\top \sto \varphi)\). Conversely, combining \(\top \sto \varphi\) with \(\mathsf{4_a}\) and \(\mathsf{tr}\) yields \(\top \sto (\top \sto \varphi)\). ◻

Definition 12. For \(\varphi\in \mathcal{L}_{\sto}\) we define \[\boxtimes\varphi := \begin{cases} \varphi&\text{if } \varphi= \top \sto \psi \text{ for some } \psi \in \mathcal{L}_{\sto}\\ \top \sto \varphi&\text{otherwise} \end{cases}\] A set \(\Sigma \subseteq \mathcal{L}_{\sto}\) is said to be closed under single boxes* if \(\varphi\in \Sigma\) implies \(\boxtimes\varphi\in \Sigma\).*

Closing a finite set \(\Sigma\) under single boxes at most doubles its size, hence it stays finite. This allows us to construct a finite model with a transitive modal relation.

Theorem 6. The logic \(\mathsf{HLC^{\flat}}\oplus \mathsf{t_{\Box}}\oplus \mathsf{4_a}\) has the finite model property.

Proof. Let \(\Gamma \Rightarrow\varphi\) be a finite consecution such that \(\Gamma \not\vdash_{\mathsf{t_{\Box}}, \mathsf{4_a}} \varphi\). Let \(\Sigma\) be the set of subformulas of \(\Gamma \cup \{ \top, \varphi\}\) closed under single boxes. Then \(\Sigma\) is finite, and we can use Lemmas 4 and 5 to extend \(\Gamma\) to a prime \((\mathrm{Ax},\Sigma)\)-theory \(\Gamma'\) containing \(\Gamma\) but not \(\varphi\). Lemma 6 then yields an \((\mathrm{Ax}, \Sigma)\)-segment \((\Gamma', U_{\Gamma',\top})\) which by Lemma 11, under the canonical valuation, invalidates \(\Gamma \Rightarrow\varphi\). Therefore \(\mathfrak{F}_{\mathrm{Ax}, \Sigma}^p = (\mathrm{SEG}_{\mathrm{Ax},\Sigma}^p, \mathrel{\substack{\textstyle\subset\\[-0.2ex]\textstyle\sim}}, \mathcal{R})\) invalidates \(\Gamma \Rightarrow\varphi\). To establish the finite model property, we now argue that \(\mathfrak{F}_{\mathrm{Ax},\Sigma}\) validates \(\mathsf{t_{\Box}}\) and \(\mathsf{4_a}\).

Using the same proof as Lemma 10 [it:axTb-canon] shows that \(\mathfrak{F}\) validates \(\mathsf{t_{\Box}}\). For \(\mathsf{4_a}\), let \((\Gamma, U_{\Gamma, \gamma})\), \((\Delta, U_{\Delta, \delta})\) and \((\Pi, U_{\Pi, \pi})\) be three \((\mathrm{Ax},\Sigma)\)-segments and suppose \((\Gamma, U_{\Gamma, \gamma}) \mathcal{R} (\Delta, U_{\Delta, \delta}) \mathcal{R} (\Pi, U_{\Pi, \pi})\). Let \(\gamma, \psi \in \Sigma\) and suppose \(\Gamma \vdash_{\mathrm{Ax}} \gamma \sto \psi\). By assumption we have \(\Gamma \vdash_{\mathrm{Ax}} \psi \sto (\top \sto \psi)\), hence by \(\mathsf{tr}\) we find \(\Gamma \vdash_{\mathrm{Ax}} \gamma \sto (\top \sto \psi)\). This entails \(\Gamma \vdash_{\mathrm{Ax}} \gamma \sto \boxtimes \psi\), and since \(\psi \in \Sigma\) we have \(\boxtimes\psi \in \Sigma\). Therefore we must have \(\boxtimes\psi \in \Delta\), hence \(\Delta \vdash_{\mathrm{Ax}} \top \sto \psi\). Finally, the definition of a segment and the fact that \((\Delta, U_{\Delta,\delta}) \mathcal{R} (\Pi, U_{\Pi, \pi})\) entails \(\psi \in \Pi\). Thus, we have shown that for any \(\psi \in \Sigma\), \(\Gamma \vdash_{\mathrm{Ax}} \gamma \sto \psi\) implies \(\psi \in \Pi\), so that \(\Pi \in U_{\Gamma,\gamma}\) hence \((\Gamma, U_{\Gamma,\gamma}) \mathcal{R} (\Pi, U_{\Pi,\pi})\). Therefore \(\mathcal{R}\) is transitive, so \(\mathfrak{F}_{\mathrm{Ax},\Sigma}^p \Vdash \mathsf{4_a}\). ◻

6 Open subframes and extension stability↩︎

Litak and Visser [@litvis24] note a direct connection between the syntactic notion of extension stability, motivated by arithmetical interpretations of \(\sto\), and a special type of nuclei on flat algebras, more specifically open nuclei [@FourmanS79; @Macnab81]. Recall that nuclei provide an algebraic perspective on subframes in modal logic [@Fine85:jsl; @Wolter1993; @BezhanishviliG07:apal]. In particular, quotienting an algebra by an open nucleus generated by a chosen element \(a\) produces an algebra (isomorphic to one) whose Heyting reduct is (isomorphic to) the ideal of elements below \(a\), with suitably restricted \(\sto\). In the classical setting with a unary box, applying this construction to dual algebras of Kripke frames produces the dual algebra of the (not necessarily modally generated!) subframe induced by \(a\); that is, a Kripke frame whose carrier and modal accessibility relation are restricted to \(a\). In the Heyting setting, the fact that \(a\) is an element of the upset algebra means that the carrier set of the corresponding subframe is \(\preceq\)-generated, i.e. an upset. When it comes to \(R\), Proposition [prop:upsame] indicates a certain subtlety: unlike the classical case, the dual algebras of our frames might fail to notice the presence/absence of certain \(R\)-edges. Let us reconsider the example of \(\mathsf{4_a}\) from Proposition [prop:fourcor]: the corresponding class of arbitrary flat frames does not appear closed with respect to the open subframe construction. However, over upward-flat frames, the situation changes: transitivity is well-known to be persistent with respect to subframes. Together with difficulties in presenting duality for flat subframes noted above (Remarks [rem:dualityhard] and [rem:nogmt]), this means that some care is needed. Given the space constraints of the present paper, we do not attempt a full discussion here. Nevertheless, it is illustrative to provide a semantic discussion of the failure of extension stability for \(\mathsf{HLC^{\sharp}}\).

Example 2. Consider the flat model \((W, \preceq, R)\) where \(W = \{ w, v, u, z \}\), the intuitionistic accessibility relation \(\preceq\) is the reflexive closure of the four worlds together with \(z \preceq v\) and \(z \preceq u\), and \(R\) is given by \(wRv\), \(wRz\) and \(wRu\): \[\begin{figure}\includegraphics[width=0.8\textwidth]{_pdflatex/vcajufsm.png}\label{hcgjekla}\end{figure}\qquad{(1)}\] This frame is clearly upward-flat. Moreover, it satisfies the sufficient condition of Lemma 3 to validate \(\mathsf{di}\). However, the open subframe obtained by removing \(z\) is precisely the one used in Example 1 to illustrate the failure of \(\mathsf{di}\).

In order to turn this counterexample into a formal proof, let us recall the syntactic characterisation of extension stability [@litvis24]. Given a formula \(\varphi\) and a fresh propositional variable \(p\), define the translation \(\varphi^{\lceil p \rceil}\) inductively as commuting with the propositional variables and the connectives of \(\mathsf{IPC}\), with the \(\sto\) clause being

\((\psi \sto\chi)^{\lceil p \rceil} := ((p\to \psi^{\lceil p \rceil}) \sto(p\to \chi^{\lceil p \rceil}))\).

As \(\Box\varphi\) is \(\top \sto\varphi\), we get \(\mathsf{HLC^{\flat}}\vdash (\Box\varphi)^{\lceil p \rceil}\) iff \(\mathsf{HLC^{\flat}}\vdash \Box(p\to \varphi^{\lceil p \rceil})\). Note that for any logic \(\Lambda\) and any \(\varphi\), if \(\Lambda \vdash \varphi^{\lceil p \rceil}\), then \(\Lambda \vdash \varphi\). A logic \(\Lambda\) is extension stable if, whenever \(\Lambda \vdash \varphi\) and \(p\) does not appear in \(\varphi\), we have \(\Lambda \vdash p \to \varphi^{\lceil p \rceil}\).

Theorem 7. The frame from Example 2 refutes \(s \to \mathsf{di}^{\lceil s \rceil}\), i.e. \[s \to (((s \to p) \sto (s \to r)) \wedge ((s \to q) \sto (s \to r)) \to ((s \to (p \vee q)) \sto (s \to r))).\] Thus, \(\mathsf{HLC^{\sharp}}\) is not extension stable, and neither is any of its extensions validated by this frame.

Proof. Define \(V(s)\) to be the complement of \(z\) and follow Example 1 for other atoms, i.e., \(V(p) = \{ v \}\), \(V(q) = \{ u \}\) and \(V(r) = \emptyset\). One can then follow the reasoning from Example 1, with \(s\) in the antecedent used to relativize reasoning to the three-state open subframe. ◻

For contrast, consider \(\mathsf{4_a}\). One can easily see that \(\mathsf{4_a}^{\lceil s \rceil}\) is equivalent to a substitution instance of \(\mathsf{4_a}\) itself, and hence \(s \to \mathsf{4_a}^{\lceil s \rceil}\) is a theorem of \(\mathsf{HLC^{\flat}}\oplus \mathsf{4_a}\). This shows that the closure of the corresponding upward-flat frames under open subframes is more important than the apparent failure of such closure in the broader class. In other words, narrowing down the class of frames might be essential for giving an appropriate duality account.

7 Conclusions and future work↩︎

We believe we have demonstrated the potential of the flat semantics for \(\mathsf{HLC^{\flat}}\). Future work needs to include general completeness and finite model property results (potentially also in the context of classical subsystems of various interpretability logics), a more systematic treatment of duality, and the open subframe construction, possibly generalising the subframe completeness result of Fine [@Fine85:jsl]. A tantalising perspective is to use the present semantics to study combinations of intuitionistic \(\sto\) with \(\Diamond\), especially on frames failing upward-flatness.

The first author was supported by Swiss National Science Foundation (SNSF) grant No. 200021_215157.↩︎
The second author would like to acknowledge the support of PNRR MUR projects PE0000013-FAIR and F53C25001420001-GAMEL.↩︎
Naming underwent several evolutions. Early references in the Utrecht school [@iemh:prov01; @iemh:pres03; @Zhou03; @IemhoffJZ05:igpl] denoted the base “flat” system as \(\mathsf{iP^-}\) and the base sharp system as \(\mathsf{iP}\), Litak and Visser [@LitVis18] replaced \(\mathsf{iP}\) with \(\mathsf{iA}\) (with \(\mathsf{P}\) standing for preservativity and \(\mathsf{A}\) standing for arrows), and in a subsequent paper the same authors [@litvis24] finally settled for the present notation.↩︎
It is worth noting here that in later years, having become aware of nascent study of non-classical calculi, Lewis not only followed closely the development of early multi-valued logics, but also on at least one occasion spoke favourably of Brouwer’s rejection of excluded middle. More information and detailed discussion can be found in Litak and Visser [@LitVis18].↩︎
We write \(\mathsf{L}-\mathrm{\small hae}\mathrm{s}\) for the class of all Lewisian Heyting Algebra Expansions, following Litak and Visser [@litvis24]. The same authors call the class of sharp algebras Lewisian Heyting Algebras with Operators* and discuss the reasons behind this terminology, whereas De Groot et al. [@grolitpat26-arxiv] call the sharp algebras simply Heyting-Lewis algebras, a name which would prove rather confusing in this context.*↩︎

Relational Semantics for Flat Heyting-Lewis Logic