In this answer to this question I asked recently, the answerer said that the tautologies in the Sierpiński space are a proper superset of the intuitionistic tautologies.

I'm wondering what I get when I take the intersection of the sets of tautologies associated with every topology. This intersection certainly contains $\top$ and $a \to a$, so it isn't empty. I'm curious whether the set of formulas I end up with is the same as the tautologies of intuitionistic propositional logic or is something else.

This question is vaguely inspired by the technique of building quasivarieties to give semantics for different logics presented in Blok and Pigozzi's Algebraizable Logic. I say vaguely inspired because I don't fully understand the construction in the book. This question is my attempt to puzzle through building a proper class (or grabbing one off the shelf like $\mathsf{top}$) and using it as a semantics for a propositional logic.

I nonstandardly use $\mathsf{top}$ to refer to the collection of all topologies, not the collection of all topological spaces.

Take the topological translation of intuitionistic propositional logic (IPC), which comes from the translation of modal logic S4.

Let $a^o$ represent the interior of the set $a$ and let $[a]$ be the topological interpretation of the well-formed formula $a$.

$$ [a \land b] = [a] \cap [b] $$ $$ [a \lor b] = [a] \cup [b] $$ $$ [a \to b] = ([a]^c \cup [b])^o $$ $$ [\bot] = \varnothing $$

In the topological interpretation I'm familiar with, the set of truth values is the standard topology over $\mathbb{R}$, lets call it $\tau^R$.

I'm wondering whether $\tau^R$ is special in some sense, or if we could also get an interpretation of IPC by looking at which statements hold in every topology.

Let $\tau$ be a topology. Let $\vec{v}$ be a mapping from variable symbols to elements of $\tau$.

Let $\tau, \vec{v} \models \varphi $ hold if and only if $[\varphi]$ is equal to $\cup \tau$ when every free variable $x_i$ in $\varphi$ is assigned the value $\vec{v}_i$.

Let $\tau \models \varphi$ hold if and only if $\tau, \vec{v} \models \varphi$ holds for all variable mappings $\vec{v}$.

I'm now going to define a set of formulas $E$ as follows. Let $\mathsf{top}$ be the collection of all topologies.

$$ E = \{ \varphi : (\forall \tau \in \mathsf{top} \mathop. \tau \models \varphi) \} $$

I'm wondering whether $E$ is the same as the set of tautologies in IPC.

The connectives $\land$ and $\lor$ and the truth value constants $\top$ and $\bot$ collectively give us that $\tau$ is a distributive lattice with $\le$ being inclusion. So far, so good. Picking any concrete topology $\tau$ can add new tautologies in the $\to$-free fragment of IPC, but it can never take them away.

With $\to$, I am not certain. As an operation, it is certainly well-defined because we are taking the interior of a well-formed expression. However, I don't know whether it behaves in the correct way for arbitrary topologies. It seems pretty clear that we have modus ponens by virtue of the fact that $(\cup \tau)^o$ is always equal to $\cup \tau$.


1 Answer 1


I could interpret this question in a couple of different ways. For simplicity, I'll answer each of my interpretations, ordering the answers from more general to more specific.

Are the propositional formulae $\varphi$ for which $\tau \models \varphi$ for every topology $\tau$ (where $\tau$ ranges over the topologies on any possible point set) precisely the intuitionistic tautologies?

Yes, these are precisely the intuitionistic tautologies. You can find this result stated in Kozen's slides or van Dalen's notes. The former also notes that, as you wrote, "$\rightarrow$ behaves in the correct way for arbitrary topologies".

If the propositional formula $\varphi$ is an intuitionistic tautology, then you can easily prove by induction on the structure of the derivation of the formula $\varphi$ that $\tau \models \varphi$ holds for all topologies $\tau$ (see e.g. Lemma 2.6 of Palmgren's notes for the Heyting algebra analogue). If, however, a propositional formula $\varphi$ is not an intuitionistic tautology, then we can

  1. invoke the completeness result for $\tau^R$ to conclude that $\tau^R \models \varphi$ fails; or
  2. use the finite model property (discussed in my answer to your previous question) to conclude that the universal closure of the equation $\varphi = \top$ is not satisfied in some finite Heyting algebra $H$. Since every finite Heyting algebra is the open set lattice of some finite topological space $S$, we get that $\tau^S \models \varphi$ fails.

The question was treated thoroughly by Rasiowa and Sikorski, who also identified the topological properties of $\mathbb{R}$ as a metric space that make it special, in the sense that the single topology $\tau^R$ suffices for completeness.

Can we find some set $P$ such that the propositional formulae $\varphi$ for which $\tau \models \varphi$ holds for every topology $\tau$ on the set $P$ precisely the intuitionistic tautologies?

Again, the answer is positive. Take $P= \mathbb{R}$. By the inductive argument mentioned above, if $\varphi$ is a tautology, then $\tau \models \varphi$ holds for all topologies $\tau$ on the set $P$. By the completeness result for $\tau^R$, we get that if $\varphi$ is not an intuitionistic tautology, then in particular $\tau^R \models \varphi$ fails.

Let $\Sigma$ denote the underlying set of the Sierpiński space. Are the propositional formulae $\varphi$ for which $\tau \models \varphi$ for every topology $\tau$ on the set $\Sigma$ precisely the intuitionistic tautologies?

The answer to this question is negative. Up to isomorphism, there are three different topologies on the two-element set. One of them is the Sierpiński topology itself, and you already know that one doesn't work by itself. The others two topologies are (in)discrete, so satisfy all Boolean identities. In fact, it follows from previously mentioned results (exercise!) that no other finite set $\Sigma$ is going to work either.


You must log in to answer this question.

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