M\"unchhausen provability

TL;DR

This paper extends the provability logic framework to transfinite levels by interpreting oracle formulas as consistency statements at lower levels, proving soundness and completeness for a broad class of theories.

Contribution

It generalizes the interpretation of provability modalities to the transfinite, overcoming syntactical challenges in the hyper-arithmetical hierarchy.

Findings

Proves soundness and completeness of the transfinite provability interpretation.

Extends Solovay's completeness results to a broader class of theories.

Provides insights on formalising the recursion into second order arithmetic.

Abstract

By Solovay's celebrated completeness result on formal provability we know that the provability logic $\mathrm GL$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable axiomatisation. Japaridze generalised this result by considering a polymodal version $\mathrm GLP$ of $\mathrm GL$ with modalities $[n]$ for each natural number $n$ referring to ever increasing notions of provability. Modern treatments of $\mathrm GLP$ tend to interpret the $[n]$ provability notion as "provable in a base theory $T$ together with all true $\Pi^0_n$ formulas as oracles". In this paper we generalise this interpretation into the transfinite. In order to do so, a main difficulty to overcome is to generalise the syntactical characterisations of the oracle formulas of complexity $\Pi^0_n$ to the hyper-arithmetical hierarchy. The paper exploits the fact that provability is $\Sigma^0_1$ complete and that similar results hold for stronger provability notions. As such, the oracle sentences to define provability at level $\alpha$ will recursively be taken to be consistency statements at lower levels: provability through provability whence the name of the paper. The paper proves soundness and completeness for the proposed interpretation for a wide class of theories; namely for any theory that can formalise the recursion described above and that has some further very natural properties. Some remarks are provided on how the recursion can be formalised into second order arithmetic and on lowering the proof-theoretical strength of these systems of second order arithmetic.