Deducibility and Independence in Beklemishev's Autonomous Provability Calculus

TL;DR

This paper introduces the Bracket Calculus (BC), a new provability logic extending Beklemishev's ordinal notation system, and demonstrates its equivalence to a fragment of GLP, also establishing an independence result relative to ATR_0.

Contribution

The paper develops the logic BC, linking ordinal notation with a positive modal language, and proves its equivalence to a fragment of GLP, providing new tools for provability and independence results.

Findings

BC is equivalent to the strictly positive fragment of GLP_{Γ_0}

A combinatorial statement based on BC is independent of ATR_0

BC extends ordinal notation to a positive modal language

Abstract

Beklemishev introduced an ordinal notation system for the Feferman-Sch\"utte ordinal $\Gamma_0$ based on the autonomous expansion of provability algebras. In this paper we present the logic $\textbf{BC}$ (for Bracket Calculus). The language of $\textbf{BC}$ extends said ordinal notation system to a strictly positive modal language. Thus, unlike other provability logics, $\textbf{BC}$ is based on a self-contained signature that gives rise to an ordinal notation system instead of modalities indexed by some ordinal given a priori. The presented logic is proven to be equivalent to $\textbf{RC}_{\Gamma_0}$, that is, to the strictly positive fragment of $\textbf{GLP}_{\Gamma_0}$. We then define a combinatorial statement based on $\textbf{BC}$ and show it to be independent of the theory $\textbf{ATR}_0$ of Arithmetical Transfinite Recursion, a theory of second order arithmetic far more powerful than Peano Arithmetic.