How do you extend the topological semantics for intuitionistic propositional logic (IPC) to a semantics for intuitionistic first order logic (IFOL)?

Question

How do you extend the topological semantics for intuitionistic propositional logic (IPC) to a semantics for intuitionistic first order logic (IFOL)?

I tried the simplest thing that could possibly work, with a classical-like domain of discourse and classical-like functions.

However, doing this has some weird consequences, like validating all classical tautologies when every atomic formula is headed by $=$.

So my question is severalfold:

• Does this naive construction actually describe some kind of predicate logic?
• Is the predicate logic that it describes the predicate logic usually referred to as intuitionistic first-order logic (assuming that there is only one)? (I think the answer is "no".)
• Assuming that this construction fails to describe IFOL, how do you actually build a semantics for it out of the topological semantics for IPC?
• Am I correct in thinking that the "tricky parts" of this construction are the exact type of collection we use for the domain of discourse and the restrictions that we place on functions?

---

Let $\tau^R$ be the standard topology on $\mathbb{R}$.

The following shows how to inductively interpret a propositional well-formed formula in ordinary IPC using the topological semantics. A primitive propositional variable $p$ ranges over the open sets of $\tau^R$. $\mathbb{R} = \cup \tau^R$ is the sole designated truth value. We get the topological semantics for IPC by translating into S4, and then invoking the topological semantics of S4.

$$[a \land b] = [a] \cap [b]$$ $$[a \lor b] = [a] \cup [b] $$ $$[a \to b] = \text{int}\!\left([a]^\complement \cup [b]\right) $$ $$[\bot] = \varnothing $$

So, here's the simplest thing that could possibly work for extending this to IFOL.

I have a model $M$, with a non-empty domain of discourse $D$. $D$ is just a set. It isn't anything fancier than a set like a fuzzy set or topological space.

If $c$ is a constant symbol, the interpretation of $c$ is an element of $D$.

If $f$ is a constant symbol of arity $n$, the interpretation of $f$ is a function from $D^n$ to $D$. I am not insisting that $f$ be computable, continuous, or imposing any other constraints that intuitively seem related to intuitionisticness.

If $R$ is a relation symbol of arity $n$, then the interpretation of $R$ is a function from $D^n$ to $\tau^R$.

With that out of the way, we can add new cases for our semantics.

$$ [t_1 = t_2] = \mathbb{R} \;\; \text{if and only if the interpretation of $t_1$ is equal to the interpretation of $t_2$} $$ $$ [t_1 = t_2] = \varnothing \;\; \text{if and only if the interpretation of $t_1$ is not equal to the interpretation of $t_2$} $$ $$ [R(t_1, t_2, \cdots t_n)] \;\; \text{is equal to the interpretation of $R$ applied to the tuple $(t_1, t_2, \cdots t_n)$ } $$

As a semantics this is well-defined, but is very weird. In particular, any expression headed by $=$ either has the truth value $\mathbb{R}$ or $\varnothing$, which means that:

$$ t_1 = t_2 \lor t_1 \neq t_2 \;\;\text{is valid for all terms $t_1, t_2$} $$

Answer 1

One approach (though far from the only one), coming mostly from categorical logic (specifically from Pitts's tripos theory), is to change the basic idea of what the underlying universe of a model is. Instead of it being an unstructured set $X$, with true equality as your basic notion of equality, you take sets paired with a Heyting-valued partial equivalence relation $\cdot\approx\cdot:X\times X\to \tau^R$ (using this specific example of topology) requiring

• $x\approx y\subseteq y\approx x$
• $x\approx y\,\cap\,y\approx z\subseteq x\approx z$

Note the absence of reflexivity here, meaning that the kind of equality relations being considered here are more general than the ones I suggested in the comments.

One then requires that all predicates interpreted in this new notion of domain (as functions $X^n\to \tau^R$) respect the equality relation in two ways. I show the unary case, but the adaptation to the $n$-ary case is simple:

• $P(x)\subseteq x\approx x$
• $x\approx y\,\cap\,P(x)\subseteq P(y)$

It's even possible to get more robust interpretations of function symbols by interpreting them as $\tau^R$-valued functional relations, where $\exists x P(x,\vec{y})$ (you need existential quantification to say "is a total function") is interpreted by $\bigcup_{x\in X}P(x,\vec{y})$.

To see that you get non-classical models this way, let $X=\{0,1\}$ with $1\approx 1=\mathbb{R}$, $0\approx 0=1\approx 0=0\approx 1=(0,1)$. You can verify that $\approx$ satisfies the requirements above, and it should also be clear that $0\approx 1\vee 0\not\approx 1$ is not equal to $\mathbb{R}$.

The fun thing about this approach is that the category of objects of the form $(X,\approx)$, with morphisms taken to be (equivalence classes of) functional $\tau^R$-valued relations, not only form a topos, but a topos which is equivalent to the category of sheaves on $\tau^R$. If you want to dig into this construction in a little more detail, I recommend Hyland, Johnstone, & Pitts's "Tripos Theory", which is still a pretty good introduction to the full construction (though requiring a bit of familiarity with category theory).