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?

  • 3
    $\begingroup$ 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. $\endgroup$ – Noah Schweber Mar 18 at 19:00
  • 1
    $\begingroup$ 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. $\endgroup$ – eulerfx Mar 19 at 15:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.