Relational Semantics for Flat Heyting-Lewis Logic

We introduce relational semantics for "flat Heyting-Lewis logic" HLC-flat.

This logic arises as the extension of intuitionistic logic with a Lewis-style strict implication modality that, contrary to its "sharp" counterpart HLC-sharp, does not turn meets into joins in its first argument.

We prove completeness and the finite model property for HLC-flat and for several extensions with additional axioms.