Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nested Sequents for Provability Logic GLP

Daniyar Shamkanov

TL;DR

A proof system is presented for the provability logic GLP in the formalism of nested sequents and the cut elimination theorem for it is proved and the reduction of GLP to its important fragment called J syntactically is obtained.

Abstract

We present a proof system for the provability logic GLP in the formalism of nested sequents and prove the cut elimination theorem for it. As an application, we obtain the reduction of GLP to its important fragment called J syntactically.

Nested Sequents for Provability Logic GLP

TL;DR

A proof system is presented for the provability logic GLP in the formalism of nested sequents and the cut elimination theorem for it is proved and the reduction of GLP to its important fragment called J syntactically is obtained.

Abstract

We present a proof system for the provability logic GLP in the formalism of nested sequents and prove the cut elimination theorem for it. As an application, we obtain the reduction of GLP to its important fragment called J syntactically.

Paper Structure

This paper contains 5 sections, 21 theorems, 63 equations.

Table of Contents

  1. Preliminaries
  2. The Sequent Calculus
  3. Admissible rules
  4. Cut Elimination
  5. An application

Key Result

Lemma 2.1

For any formula $A$, we have $\mathsf{GLP_{NS}} \vdash \Gamma \{ A, \overline{A}\}$.

Theorems & Definitions (39)

  • Lemma 2.1
  • proof
  • Lemma 2.2
  • proof
  • Proposition 2.3
  • proof
  • Lemma 3.1: Admissibility of structural rules
  • proof
  • Lemma 3.2: Invertibility
  • proof
  • ...and 29 more