A proof system for the positive fragment of GL

Abstract

In this paper, we present a proof system $\mathsf{GL}_{+}^{\top\bot}$, which is based on a sequent system $\mathsf{K}_{+}^{\top\bot}$ given by Dunn, for the positive fragment of $\mathsf{GL}$. Positive modal formulas are modal formulas that contain neither negation symbols nor implication symbols. More precisely, they are modal formulas constructed from the connectives $\lor$, $\land$, $\Diamond$, $\Box$, $\bot$, $\top$, and propositional variables. The logic $\mathsf{GL}$ is the least normal modal logic that contains $\mathsf{K}$ and the L\"{o}b formula $\Box(\Box p\supset p)\supset\Box p$. Following Dunn, a sequent is an expression of the form $\phi\vdash\psi$, where $\phi$ and $\psi$ are positive modal formulas. We present a proof system $\mathsf{GL}_{+}^{\top\bot}$ for sequents with the property that a sequent $\phi\vdash\psi$ is provable in $\mathsf{GL}_{+}^{\top\bot}$, if and only if $\phi\supset\psi$ is provable in $\mathsf{GL}$.