The polytopologies of transfinite provability logic

TL;DR

This paper extends the topological completeness results of transfinite provability logic GLP(ω) to arbitrary ordinals, introducing provability ambiances based on Icard polytopologies to model these systems.

Contribution

It generalizes the completeness of GLP(\Lambda) for all ordinals \\Lambda, and introduces provability ambiances with Icard polytopologies for modeling provability logic.

Findings

Proves completeness of GLP(\\Lambda) for topological models for any ordinal \\Lambda.

Introduces provability ambiances as a new class of topological models.

Establishes the use of Icard polytopologies in modeling provability logic.

Abstract

Provability logics are modal or polymodal systems designed for modeling the behavior of G\"odel's provability predicate in arithmetical theories and its natural extensions. If \Lambda is any ordinal, the G\"odel-L\"ob calculus GLP(\Lambda) contains one modality [\lambda] for each \lambda<\Lambda, representing provability predicates of increasing strength. GLP(\Lambda) has no Kripke models, but Beklemishev and Gabelaia recently proved that GLP(\omega) is complete for its class of topological models. In this paper we generalize Beklemishev and Gabelaia's result to GLP(\Lambda) for arbitrary \Lambda. We also introduce provability ambiances, which are topological models where valuations of formulas are restricted. With this we show completeness of GLP(\Lambda) for the class of provability ambiances based on Icard polytopologies.