On topological models of GLP

Abstract

We develop topological semantics of a polymodal provability logic GLP. Our main result states that the bimodal fragment of GLP, although incomplete with respect to relational semantics, is topologically complete. The topological (in)completeness of GLP remains an interesting open problem.