Topological completeness of the provability logic GLP

TL;DR

This paper proves that the provability logic GLP is complete when interpreted through a specific class of topological spaces called GLP-spaces, resolving a longstanding incompleteness issue.

Contribution

It introduces constructions for nontrivial GLP-spaces and establishes the completeness of GLP with respect to these spaces, linking modal logic with topological semantics.

Findings

GLP is complete w.r.t. GLP-spaces

Constructed nontrivial GLP-spaces satisfying all axioms

Resolved the incompleteness of GLP in Kripke semantics

Abstract

Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces satisfying all the axioms of GLP are called GLP-spaces. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.