Semantical cut-elimination for the provability logic of true arithmetic

TL;DR

This paper provides a semantic approach to cut-elimination in the provability logic GLS, enhancing understanding of its structure and enabling generalizations to other quasi-normal modal logics.

Contribution

It introduces semantical characterizations of GLS and offers a semantic proof of cut-elimination, extending applicability to other similar logics.

Findings

Semantic characterizations of GLS established

Semantic proof of cut-elimination provided

Framework generalizes to other quasi-normal modal logics

Abstract

The quasi-normal modal logic GLS is a provability logic formalizing the arithmetical truth. Kushida (2020) gave a sequent calculus for GLS and proved the cut-elimination theorem. This paper introduces semantical characterizations of GLS and gives a semantical proof of the cut-elimination theorem. These characterizations can be generalized to other quasi-normal modal logics.