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?
