  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.
