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öb formula $\Box(\Box p\supset p)\supset\Box p$. Following Dunn, a sequent is an expression of the form $ϕ\vdashψ$, where $ϕ$ and $ψ$ are positive modal formulas. We present a proof system $\mathsf{GL}_{+}^{\top\bot}$ for sequents with the property that a sequent $ϕ\vdashψ$ is provable in $\mathsf{GL}_{+}^{\top\bot}$, if and only if $ϕ\supsetψ$ is provable in $\mathsf{GL}$.