Provability Logics of Hierarchies

Abstract

The branch of provability logic investigates the provability-based behavior of the mathematical theories. In a more precise way, it studies the relation between a mathematical theory $T$ and a modal logic $L$ via the provability interpretation which interprets the modality as the provability predicate of $T$. In this paper we will extend this relation to investigate the provability-based behavior of a hierarchy of theories. More precisely, using the modal language with infinitely many modalities, $\{{\square }_n{\}}_{n=0}^{\infty }$, we will define the hierarchical counterparts of some of the classical modal theories such as $K4$, $KD4$, $\mathbf{GL}$ and $S4$. Then we will define their canonical provability interpretations and their corresponding soundness-completeness theorems.