A cut-free proof system for a predicate extension of the logic of provability

TL;DR

This paper presents a new cut-free proof system, NQGL, for a predicate extension of the provability logic GL, featuring a non-compact rule and completeness for certain Kripke frames.

Contribution

It introduces NQGL, a novel modal sequent calculus for predicate provability logic that avoids cuts and uses a non-compact rule, expanding proof-theoretic methods.

Findings

NQGL is cut-admissible and complete.

NQGL uses a non-compact rule with countably many premises.

The system characterizes Kripke frames with finite path lengths.

Abstract

In this paper, we introduce a proof system $\mathsf{NQGL}$ for a Kripke complete predicate extension of the logic $\mathbf{GL}$, that is, the logic of provability, which is defned by $\mathbf{K}$ and the L\"{o}b formula $\Box(\Box p\supset p)\supset\Box p$. $\mathsf{NQGL}$ is a modal extension of Gentzen's sequent calculus $\mathsf{LK}$. Although the propositional fragment of $\mathsf{NQGL}$ axiomatizes $\mathbf{GL}$, it does not have the L\"{o}b formula as its axiom. Instead, it has a non-compact rule, that is, a derivation rule with countably many premises. We show that $\mathsf{NQGL}$ enjoys cut admissibility and is complete with respect to the class of Kripke frames such that for each world, the supremum of the length of the paths from the world is finite.