# Connection between Provability Logic (GL) and geometry?

In Provability Logic (aka GL) we have

• The Beth definability theorem and
• De Jong-Sambin Fixed Point Theorem

The former has a vague similarity to the implicit function theorem in that you can loosely read it as saying that injective (in some sense) functions of sentences define equations with unique well-defined solutions.

The latter is also about equations having solutions and is vaguely suggestive of the contraction mapping theorem. For example the function $$P\mapsto\neg\Box P$$ has a fixed point and it has one because the $$P$$ appears inside a $$\Box$$ operation, suggesting $$\Box$$ is a bit like a contraction.

Is there a topological or metric space interpretation of these theorems?

• There seems to be an existing literature on topological semantics and provability logics. Thomas Icard has slides on this, and the Stanford Encyclopedia of Philosophy has a bit on the topic. I'm not sure how related this is to the specific topological/geometric intuitions you give here, but it might be of interest more broadly. – Noah Schweber Mar 18 at 19:00
• Maybe related, Maurice Herlihy uses Sperner's Lemma, along with other topological tools, to prove impossibility of distributed consensus in The Topological Structure of Asynchronous Computability. – eulerfx Mar 19 at 15:46