A proof system for the positive fragment of GL

Abstract

In this paper, we present a proof system ${\mathsf{GL}}_{+}^{\top \perp }$, which is based on a sequent system ${\mathsf{K}}_{+}^{\top \perp }$ 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 $\vee$, $\wedge$, $◊$, $\square$, $\perp$, $\top$, and propositional variables. The logic $\mathsf{GL}$ is the least normal modal logic that contains $\mathsf{K}$ and the Löb formula $\square (\square p\supset p)\supset \square p$. Following Dunn, a sequent is an expression of the form $\varphi ⊢\psi$, where $\varphi$ and $\psi$ are positive modal formulas. We present a proof system ${\mathsf{GL}}_{+}^{\top \perp }$ for sequents with the property that a sequent $\varphi ⊢\psi$ is provable in ${\mathsf{GL}}_{+}^{\top \perp }$, if and only if $\varphi \supset \psi$ is provable in $\mathsf{GL}$.