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$} $$

  • 1
    $\begingroup$ You might be interested in the work of Awodey and Kishida on Topological Semantics for First Order Modal Logic. See here or here for instance. The idea is to use a sheaves on a topological space in order to encode the first order parts of your logic. $\endgroup$ Oct 10, 2021 at 18:17
  • 1
    $\begingroup$ In general, you can let the equality relation be more interesting than the one you've chosen, by treating it as a non-logical symbol that is always required to be a Heyting-valued equivalence relation and requiring your other non-logical relations to interact with it appropriately. $\endgroup$ Oct 10, 2021 at 20:01
  • 1
    $\begingroup$ @MaliceVidrine, Hmm interesting. So we consider theories in the naive system shown that are $=$-free but have $\equiv$ and sufficient additional axioms to make $\equiv$ a congruence with respect to all functions? I thought about including something like that but didn't want to pollute the question with more than one concrete construction. Is that enough to give us a semantics of IFOL? (or perhaps the algebraic fragment of IFOL?) $\endgroup$ Oct 10, 2021 at 20:29
  • 2
    $\begingroup$ You might also want to look into topos theory, especially the internal language of a topos and its interpretation within a concrete topos. (This goes even a bit further than IFOL, in allowing you to use function types, "power set" types, product types, disjoint union types, subset types defined by a "selection axiom"-style construction, etc.) $\endgroup$ Oct 11, 2021 at 16:17
  • $\begingroup$ @GregoryNisbet In relation to your previous question: normally, you still keep $=$ in the FOL theory, but you specify that a Heyting-algebra-valued equivalence relation on the domain of discourse is the interpretation of the $=$ symbol, and also require that the interpretation of each function symbol is respectful of that equivalence relation (e.g. $R(x, y) \le R(f(x), f(y))$ for a unary function symbol) and similarly for the interpretation of each relation symbol. $\endgroup$ Oct 11, 2021 at 23:19

1 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).


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .