A proof system for the positive fragment of GL

TL;DR

This paper introduces a new proof system for the positive fragment of the modal logic GL, enabling proof verification for sequents involving only positive modal formulas.

Contribution

It provides a sequent-based proof system for the positive fragment of GL, establishing a correspondence with the existing logic's provability.

Findings

The proof system $ extsf{GL}_{+}^{ opot}$ is sound and complete for the positive fragment of GL.

A sequent $ extsf{ extit{phi}} vdash extsf{ extit{psi}}$ is provable iff $ extsf{ extit{phi}} o extsf{ extit{psi}}$ is provable in GL.

The system simplifies proof procedures for positive modal formulas in 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}$.