Deducibility and Independence in Beklemishev's Autonomous Provability Calculus

Abstract

Beklemishev introduced an ordinal notation system for the Feferman-Schütte ordinal ${\Gamma }_0$ based on the autonomous expansion of provability algebras. In this paper we present the logic $\text{BC}$ (for Bracket Calculus). The language of $\text{BC}$ extends said ordinal notation system to a strictly positive modal language. Thus, unlike other provability logics, $\text{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 ${\text{RC}}_{{\Gamma }_0}$, that is, to the strictly positive fragment of ${\text{GLP}}_{{\Gamma }_0}$. We then define a combinatorial statement based on $\text{BC}$ and show it to be independent of the theory ${\text{ATR}}_0$ of Arithmetical Transfinite Recursion, a theory of second order arithmetic far more powerful than Peano Arithmetic.