Relational semantics for flat Heyting-Lewis Logic

TL;DR

This paper introduces relational semantics for flat Heyting-Lewis logic, extending intuitionistic logic with a Lewis-style strict implication, and proves key properties like completeness and finite model property.

Contribution

It develops a new relational semantics for flat Heyting-Lewis logic and establishes foundational completeness and model properties.

Findings

Proves completeness of flat Heyting-Lewis logic

Establishes finite model property for the logic and its extensions

Defines semantics that differ from the sharp counterpart in how meets and joins are handled

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.