A DUAL PROOF OF BLOK’S LEMMA · Ordered spaces and frames

Source textPage 1

1. Blok-Esakia Theorem

A modal companion of a superintuitionistic (si) logic $L$ is any normal modal logic above $S4$ in which $L$ fully and faithfully embeds via the Gödel translation. The notion of a modal companion has a rich theory [6, 8, 10, 7, 4, 12, 3], culminating in a result known as the Blok-Esakia theorem [7, 2]. The latter states that the lattice si logics is completely isomorphic to the lattice of normal extensions of $Grz$ , via the mapping that sends a si logic $L$ to the least normal extension of $Grz$ containing the Gödel translations of all theorems of $L$ .

Source textPage 1

The literature contains several proofs of the Blok-Esakia theorem. Blok’s original proof [2] is algebraic and notoriously involved (see also [11]). Esakia appears to have given a dual proof, which remains unpublished. Zacharyaschev later gave a proof using the machinery of canonical formulas [13], which Jeřábek [9] later extended to rule systems using canonical rules. More recently, Bezhanishvili and Cleani [1] (see also [5]) offered an alternative proof based on stable canonical rules, which are algebra-based rules that are to filtration what Jerabek’s canonical rules are to selective filtration.

Our contribution is to show that the proof by Bezhanishvili and Cleani can be carried out without the machinery of stable canonical rules. Moreover, the key idea of that proof can be adapted to obtain a dual, order-topological proof that resembles Blok’s original algebraic one, and gives some intuitions on it.

Source textPage 1

2. Blok’s Lemma

We begin with some preliminary definitions. Let $H$ be a Heyting algebra. The modal algebra $\sigma H$ is constructed by expanding the free Boolean extension $B(H)$ of $H$ with the operator

$\square a := \bigvee\{b\in H:b\leq a\}.$

It is well known that $\sigma H$ is always a $Grz$ -algebra.

Conversely, given an $S4$ -algebra $M$ , the skeleton $\rho M$ of $M$ is simply the Heyting algebra of open elements of $M$ . We recall that an element $a$ of $M$ is open when $\square a=a$ , and that the Heyting implication of $\rho M$ is given by $a\to b:=\square(a\to b)$ .

It is well-known that $\rho$ commutes with all variety operations. Sigma commutes with subalgebras and homomorphic images, and also finite products, but not with arbitrary products in general.

Source textPage 1

Dually, when $X$ is an Esakia space we let $\sigma X:=X$ . Conversely, when $Y$ is an $S4$ -space, we let $\rho Y$ be the Esakia space that results from $Y$ by collapsing all clusters, and endowing the result with the quotient topology under the cluster collapse mapping. The algebraic and topological versions of the mappings $\sigma,\rho$ are dual to one another.

Source textPage 1

A $Grz$ -algebra $M$ is called skeletal when it is isomorphic to $\sigma\rho M$ . Blok derives the Blok-Esakia theorem as a consequence of the following Lemma, now widely known as Blok’s Lemma.

Lemma 1 (Blok’s Lemma). Let $M$ be a $Grz$ -algebra. Then $M\in\mathrm{IS}\mathrm{P}_{\mathrm{U}}(\sigma\rho M)$ .

Our goal in this work is to provide a different, more geometric, proof of the same fact.

Source textPage 2

Let $M,N$ be modal algebras and let $A,B$ be Boolean subalgebras of $M,N$ respectively. A mapping $h:A\to B$ is called a $\square$ -homomorphism when it is a Boolean homomorphism and $h(\square a)=\square h(a)$ whenever $\square a\in A$ . The key step in Blok’s proof of Lemma 1 is the following result.

Lemma 2 (Algebraic embedding lemma). Let $M$ be a $Grz$ -algebra and let $N$ be a finite Boolean subalgebra of $M$ . Then there is a $\square$ -embedding $h:N\to\sigma\rho M$ .

Source textPage 2

The proof given in [1], in turn, makes use of stable maps between modal spaces:

Definition 3. Given modal spaces $X=(X,R)$ and $Y=(Y,R)$ , a continuous function $f:X\to Y$ is said to be stable if $f(x)Rf(y)$ holds whenever $xRy$ . Given $D\subseteq\mathrm{Clop}(Y)$ we say that $f$ satisfies the bounded domain condition (BDC) with respect to $D$ if for all $U\in D$ , if $f(x)Ry$ and $y\in U$ , then there is some $x'$ such that $xRx'$ and $f(x')\in U$ .

Given $Y$ a finite $S4$ -space, and $D$ a domain, $\mathcal{J}(Y,D)$ denotes the stable canonical rule. Bezhanishvili and Cleani show that for a $Grz$ -space $X$ , $X\nVdash\mathcal{J}(Y,D)$ implies $\rho X\nVdash\mathcal{J}(Y,D)$ , which amounts to showing the following lemma:

Lemma 4. Given a $Grz$ -space $X=(X,R)$ , a finite $S4$ -space $Y=(Y,R)$ , and a surjective stable map $p:X\to Y$ satisfying the BDC for a domain $D$ , there is a stable surjection $p':\rho X\to Y$ satisfying the BDC for the domain $D$ .

Source textPage 2

One can then show the following:

Proposition 5. The following statements are equivalent:

Blok’s Lemma;
The algebraic stable embedding lemma;
The stable surjection lemma.

Proof

The equivalence of (2-3) follows strictly from duality. Given the algebraic stable embedding lemma, one can obtain Blok’s lemma by model theoretic reasoning: to show that $M$ embeds into an ultrapower of $\sigma\rho(M)$ , pick a finite collection of elements from $M$ . Form a finite Boolean subalgebra of $M$ with these elements, say $N$ ; note that $N$ then is a partial modal algebra. Using the algebraic stable embedding lemma, we find a $\Box$ -preserving injection to $\sigma\rho(M)$ . This ensures that the finite diagram can be realized. By classical model theory results, this shows that $M$ embeds into an ultrapower of $\sigma\rho(M)$ .

For the converse, assume Blok’s lemma. It is known that satisfying the same universal class means that each finite diagram embeds into an algebra in the target, which yields the algebraic stable embedding lemma.

Source textPage 2

3. Step-by-Step Proofs of Blok’s Lemma

By considering the specifics of the algebraic proof of Blok’s lemma and the order-topological one of [1], we will obtain a new dual proof which closely mirrors the original one of Blok. This starts with the following:

Lemma 6 (Algebraic one-step embedding). Let $M$ be a $Grz$ -algebra and let $N$ be a finite Boolean subalgebra, such that $h:N\to\sigma\rho M$ is a $\square$ -embedding fixing all open elements. If $x\in M$ is arbitrary, then there are finitely many open elements $C$ , and a $\square$ -embedding $h':\langle N\cup\{x\}\cup C\rangle\to\sigma\rho M$ such that $h'\upharpoonright_N=h$ .

Source textPage 2

Indeed, having this lemma, and an arbitrary finite Boolean subalgebra $N$ , one enumerates $N=N_{op}\cup\{x_1,...,x_n\}$ where $N_{op}=\langle\{\square a:\square a\in N\}\rangle$ . Then one sets $N_0=N_{op}$ , and successively adds one element, creating a sequence of algebras:

$N_0\to N_1\to...\to N_n$

Source textPage 2

where $N\subseteq N_n$ . Having a $\square$ -embedding of the latter algebra gives us a $\square$ -embedding of $N$ . It is the way that such elements are picked which demands the Grz-axiom: given $N_k$ , to extend the embedding to $\langle N_k\cup\{x_{k+1}\}\rangle$ one needs only define the image of $x_{k+1}$ . This is done by picking, for each $c\in N_k$ , an element element $w_c$ which is defined, by letting $u_c=\neg x_{k+1}\lor c$ as:

$w_c:=\neg(\square(u\to\square u)\to\square u).$

Source textPage 3

The use of the Grz-axiom lies in ensuring that $\square(\square(u\to\square u)\to\square u)\leq u$ ; dually, this follows if:

$u\leq\Diamond\pi u$

where $\pi u=u\land\neg\Diamond(\Diamond u\land\neg u)$ . This is called by Esakia the rest of $u$ ; dually, given a clopen $U$ , $\pi U$ is called the set of passive points of $U$ , and it is known that the Grz-axiom corresponds to every point in $U$ being below a passive point.

The picture on the right illustrates how the Grz axiom is used.

Source textPage 3

Applying the key idea of the proof of [1, Main Lemma], one can obtain a dual step-by-step proof of Blok’s lemma. Given a space $X$ , let $\rho:X\to\rho X$ be the cluster collapse continuous map. Moreover, a surjection $\varrho:X\to Y$ is called a cluster-reducing map when it is the quotient map induced by some equivalence relation on $Y$ that never relates points belonging to different clusters in $X$ .

Source textPage 3

Lemma 7 (Dual one-step surjection). Let $X=(X,R),Y=(Y,R)$ and $Y'=(Y',R)$ be $S4$ spaces with the following properties.

$X=(X,R)$ is a Grz space;
$Y'=Y\sqcup\{\bullet\}$ and there is a cluster-reducing map $\varrho:Y'\to Y$ which identifies $\bullet$ with some point in its cluster, but does not identify any other points;
There is a stable surjection $f:X\to Y'$ satisfying the BDC for some $D\subseteq Y'$ ;
There is a stable surjection $g:\sigma\rho X\to Y$ satisfying the BDC for $\varrho[D]$ .

Then there is a stable map $h:\sigma\rho X\to Y'$ satisfying the BDC for $D$ .

Source textPage 3

Note $\max(f^{-1}[\bullet])$ and $\max(f^{-1}[x])$ are disjoint and closed. Moreover, because $X$ is a Grz-space, both these sets consist entirely of passive elements.

Source textPage 3

Having obtained Lemma 7, we prove Blok’s lemma following the algebraic proof strategy. Given a finite $S4$ -space $Y=(Y,R)$ , we set $Y_0=\sigma\rho Y$ and form the inverse chain

$Y_0\leftarrow Y_1\leftarrow...\leftarrow Y_n$

where $Y_n=Y$ , and $Y_{i+1}$ is obtained as some cluster-expansion of $Y_i$ by one additional element; the existence of the surjections in the chain being guaranteed by Lemma 7. The algebra $N_0$ is the dual of $Y_0$ , and the posets $Y_k$ – whilst not being isomorphic to the dual of $N_k$ – can be seen as refinements of the decomposition given by the algebraic construction.