# A continuous notion of realizability

I have been interested in non-classical logics, off and on, for quite a while. This question is probably very basic, and I hope it is not too low-level for MO. My question stems from an attempt to define a notion of "continuous truth" in a topological structure.

Suppose I have a topological structure $(M, \tau)$ - that is, a first-order structure $M$ with a topology $\tau$ on the underlying set. Usually - i.e., as Abraham Robinson does in "A note on topological model theory" (Fundamenta Mathematicae, 1974) - one demands that the topology and the first-order structure be compatible in some way, and then goes on to formulate a version of classical first-order logic augmented by some topological quantifiers. I'm interested in going a slightly different direction. I do want to demand that my first-order and topological structures be compatible - specifically, I will demand that the interpretations of function symbols be continuous functions from the relevant product topology to the structure, and the interpretations of relation symbols be closed sets in the relevant product topology - but I want to wind up with a non-classical logic at the end. Specifically, motivated by Kleene's notion of realizability, I will say that a topological structure $(M, \tau)$ continuously realizes a formula $\phi$ in prenex normal form if Skolem functions for $\phi$ can be found which are continuous according to $\tau$.

For example, consider any map $m: X\rightarrow Y$ between two topological spaces which is continuous and bijective but has no continuous inverse. Consider the structure $M$ with underlying set $X\sqcup Y\sqcup\lbrace o\rbrace$, topologized naturally, with a unary relation $U$ representing $X$, a unary relation symbol $V$ representing $Y$, and a unary function symbol $f$ representing $m$ which sends all $x\in X$ to $m(x)$ and all other points to $o$. Then the statement "$\forall x\exists y(V(x)\implies f(y)=x)$" is not continuously realized, although classically it should be true.

If I understand things correctly, this is a situation generalized by the construction of first-order logic internal to a topos; however, I know virtually nothing about topos theory. My question is the following: what am I talking about? That is, what is this notion generally called, and when did it originate? Also, am I correct in thinking that it is generalized by (the logical side of) topos theory?

(Additionally, as a minor subquestion: is my reasoning in the example two paragraphs prior correct?)

Thank you all in advance, and I hope this question is not too elementary.

• @Wouter and Andrej: thank you both very much! Your answers are very helpful. – Noah Schweber Oct 27 '12 at 1:31

Kleene defined a continuous realizability over Baire space, i.e. $\mathbb N^{\mathbb N}$ with the product topology. In this model $\forall x\exists y\phi(x,y)$ is valid, if there is a continuous function $f$ such that $\forall x\phi(x,f(x))$ is valid. That sounds like what you are looking for. A realizability model assigns a set of realizers to each formula, and $p\models q$ is valid if there is a suitable partial function mapping realizers of $p$ to realizers $q$. In Kleene's example the realizers are members of Baire space and the functions are the partial continuous ones.
In short, Kleene's realizability intepretation of logic works for a wide class of "computatonal models" known as (typed) combinatory algebras. Kleene's number realizability is just one such model, but there are topological models as well, for example Scott's graph model $\mathcal{P}{\omega}$ (which is closely related to equilogical spaces). In fact, the topological spaces themselves form a (large) type combinatory algebra which allows us to write down a realizability interpretation of logic in which the realizers are elements of topological spaces.