Modal logic, fundamentally

TL;DR

Using algebraic representation theorems, it is proved that a system of fundamental modal logic is sound and complete with respect to an elementary class of bi-relational structures $(X,\vartriangleleft, R)$.

Abstract

Non-classical generalizations of classical modal logic have been developed in the contexts of constructive mathematics and natural language semantics. In this paper, we discuss a general approach to the semantics of non-classical modal logics via algebraic representation theorems. We begin with complete lattices $L$ equipped with an antitone operation $\neg$ sending $1$ to $0$, a completely multiplicative operation $\Box$, and a completely additive operation $\Diamond$. Such lattice expansions can be represented by means of a set $X$ together with binary relations $\vartriangleleft$, $R$, and $Q$, satisfying some first-order conditions, used to represent $(L,\neg)$, $\Box$, and $\Diamond$, respectively. Indeed, any lattice $L$ equipped with such a $\neg$, a multiplicative $\Box$, and an additive $\Diamond$ embeds into the lattice of propositions of a frame $(X,\vartriangleleft,R,Q)$. Building on our recent study of "fundamental logic", we focus on the case where $\neg$ is dually self-adjoint ($a\leq \neg b$ implies $b\leq\neg a$) and $\Diamond \neg a\leq\neg\Box a$. In this case, the representations can be constrained so that $R=Q$, i.e., we need only add a single relation to $(X,\vartriangleleft)$ to represent both $\Box$ and $\Diamond$. Using these results, we prove that a system of fundamental modal logic is sound and complete with respect to an elementary class of bi-relational structures $(X,\vartriangleleft, R)$.

Figures (4)

• Figure 1: Illustration of the modal frame condition in Definition \ref{['ModalFrameDef']}. A solid line from $w$ to $v$ indicates $w\vartriangleright v$, and a dashed line from $w$ to $v$ indicates $wRv$.
• Figure 2: Illustration of the condition for $x\in \Diamond_QA$ from Proposition \ref{['BoxDiamond']}. The dotted line from $x'$ to $y'$ indicates $x'Qy'$.
• Figure 3: Illustration of the additivity condition in Definition \ref{['AddDef']}.
• Figure 4: Illustration of the negativity condition in Definition \ref{['NegativeFrameDef']}.

Theorems & Definitions (51)

• definition 1
• theorem 1: Aguilera2022
• proposition 1: Holliday2023
• proposition 2
• definition 2
• lemma 1
• proposition 3
• definition 3
• proposition 4
• proposition 5: Holliday2023, Proposition 4.14.1-2