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.



A continuous notion of realizability
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.


To generalize this example, you should consider the category [*equilogical spaces*](http://ncatlab.org/nlab/show/equilogical+space) as an interesting category to develop such a continuous model theory in. In this category realizers can be points of arbitrary T\_0-spaces. I am unsure how much research has been done in this area.


Realizability models can be extended to realizability toposes, if and only if they have *(order) partial combinatory algebras* as object of realizers. This can be gathered from Streicher and Lietz's "Impredicativity entails untypedness" in combination with Hofstra's "All realizability is Relative". In order to get all realized functions to be continuous, I would suggest looking into topological partial combinatory algebras. Some research on these has been done by Ingemarie Bethke.


I invite you to have a look at my PhD. thesis, which can be downloaded from <http://woupiestek.nl>. It contains a lot of information on realizability toposes.


