Topological completeness of the provability logic GLP
arXiv:1106.5693 · doi:10.1016/j.apal.2013.07.006
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.