Models of transfinite provability logic

TL;DR

This paper extends Kripke and topological models for transfinite provability logic GLP(Λ), demonstrating soundness and completeness of these models for the logic's closed fragment across arbitrary ordinals.

Contribution

It generalizes existing models for GLP(Λ) to arbitrary ordinals, providing new Kripke and topological models with completeness results.

Findings

Constructed Kripke models I(Θ,Λ) for arbitrary Θ and Λ.

Developed topological models T(Θ,Λ) for the same parameters.

Proved soundness and completeness of these models for the closed fragment of GLP(Λ).

Abstract

For any ordinal \Lambda, we can define a polymodal logic GLP(\Lambda), with a modality [\xi] for each \xi<\Lambda. These represent provability predicates of increasing strength. Although GLP(\Lambda) has no Kripke models, Ignatiev showed that indeed one can construct a Kripke model of the variable-free fragment with natural number modalities. Later, Icard defined a topological model for the same fragment which is very closely related to Ignatiev's. In this paper we show how to extend these constructions for arbitrary \Lambda. More generally, for each \Theta,\Lambda we build a Kripke model I(\Theta,\Lambda) and a topological model T(\Theta,\Lambda), and show that the closed fragment of GLP(\Lambda) is sound for both of these structures, as well as complete, provided \Theta is large enough.