Non-Wellfounded Proof Systems for Provability Logics and Their Metatheory
Guannan Mi

Abstract:
Many provability logics enjoy fixpoint theorems. This provides a natural motivation for studying non-wellfounded proof systems for such logics, as non-wellfounded proof systems are well-suited for defining proof systems for modal logics with fixpoints. Nevertheless, comparatively few provability logics have been equipped with non-wellfounded proof systems of their own. Moreover, even for those logics for which such systems are already available, non-trivial questions remain open, such as the existence of explicit cut reduction procedures. Against this background, this thesis investigates the non-wellfounded proof theory of the following provability logics: Gödel-Löb logic (GL), strong Löb’s logic (iSL_\box), and Kuznetsov-Muravitsky logic (KM).
For GL, building on existing one-sided non-wellfounded systems for this logic, this thesis provides both an infinitary system and a cyclic system based on two-sided multiset sequents. These systems are formulated in G3-style. The main contribution of the investigation of GL is a direct cut reduction procedure for the cyclic system developed in the thesis. For iSL_\box, novel non-wellfounded systems in both G3- and G4-styles are introduced. These systems are formulated using set sequents, and are shown to be sound and cut-free complete. Moreover, the G4-style systems admit terminating backward proof search. The existence of such systems for iSL_\box establishes that iSL_\box is a cyclic companion of intuitionistic doxastic logic. Additionally, the thesis also identifies the technical difficulties involved in adopting set sequents in the intuitionistic setting and discusses possible ways of addressing them. Lastly, for KM, sound G4-style systems are proposed.