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.