Relational semantics for flat Heyting-Lewis Logic

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