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.
Related
- Mechanizing Gödel's Incompleteness Theorems and Provability Logic
- Completeness of the Gödel--Löb Provability Logic for Finite Derived Ordinal Topologies
- Omitting Types for Infinitary Real-Valued Logic: A Topological Perspective
- Infinitary real-valued logic and a refinement of the Kochen-Specker theorem
- Infinitary positive existential normal forms for modules
BibTeX
@misc{mojtahedi2026infinitary,
title = {{Infinitary provability logic}},
author = {Mojtaba Mojtahedi and Fedor Pakhomov and Giovanni Soldà},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.24795},
eprint = {2609.24795},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.24795},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Infinitary provability logic
AU - Mojtaba Mojtahedi
AU - Fedor Pakhomov
AU - Giovanni Soldà
PY - 2026
DA - 2026/09/21
PB - arXiv
DO - 10.48550/arxiv.2609.24795
UR - https://arxiv.org/abs/2609.24795
AB - 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.
ER -