A continuous notion of realizability

Question

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.

Answer 1

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 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 https://research-portal.uu.nl/en/publications/realizability-categories. It contains a lot of information on realizability toposes.

Answer 2

To see how the realizability logic works in a topological model have a look at my PhD thesis where these things are explicitly spelled out (chapter on equilogical spaces, for example). Alternaltively you could look at my notes "Realizability as the Connection between Computable and Constructive Mathematics", which are shorter and written as a tutorial.

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.