Infinitary provability logic

Abstract

Gödel-Löb provability logic $\GL$ is a propositional modal system that on one hand enjoys completeness with respect to conversely well-founded Kripke frames and on the other hand captures all modal principles about $\PA$-provability that are provable in $\PA$ itself. In the present paper we carry out an initial investigation into the question of what the infinitary counterpart of $\GL$ is. We develop a non-well-founded deep inference proof system $\dgla$ for the modal language with at most countably infinite conjunctions and disjunctions. We show that the calculus is sound and complete for well-founded transitive Kripke frames. Using Kripke-Platek set theory we develop an interpretation of the infinitary modal language in terms of infinitary provability over admissible sets. Then we show that a natural Hilber-style variant of infinitary $\GL$ is sound for this interpretation. We leave open, however, the question if $\dgla$ proves any additional theorems in comparison with the Hilbert-style calculus. Nevertheless, under certain conditions we do show that the infinitary provability logic arising from certain admissible sets lies between the set of theorems of the Hilbert-style calculus and the non-well-founded deep inference system.