Co-lifting of Heyting algebras and its S4 analogue
Kanako KOBAYASHI
Kyoto University

CRECOGI meeting 2018, 8 Oct.

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

1 / 35

Introduction

In logic:
Intuitionistic logic

Girard translation/ Modal logic S4

Kleisli construction

S4 algebras

In algebra:
Heyting algebras oThis can be extended to all intermediate logics and extensions of themodal logic S4.
(A logic L is called an intermediate logic if Int ⊆ L ⊆ Cl)

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

2 / 35

Introduction

A. Wroński, ”Intermediate logics and Disjunction Property”(1973)’There are 2ω intermediate logics with the disjunction property’.
In the paper, two constructions of Heyting algebras appear:
co-lifting of Heyting algebras H⊤
quotient modulo the monolith H/µH

We propose an S4 analogue of these constructions.
We show that they correspond to each other via the Kleisli
construction.
As an application, we get new logics having the disjunction property.

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/083 / 35

Introduction
Definition
S4 : the category of S4 algebras and homomorphisms.
Hey : the category of Heyting algebras and homomorphisms.

Boolntemb × S4embg&

∼
=S4SI

S4(−)□

(−)□

(−)□

(−)⊤



Heyembf∼
=&

HeySI



Hey−/µKanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

4 / 35

Outline

1

Introduction

2

Basic Definitions

3

Co-lifting of Heyting Algebras

4S4 analogue of co-lifting

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

5 / 35Outline

1

Introduction

2

Basic Definitions

3

Co-lifting of Heyting Algebras

4S4 analogue of co-lifting

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

6 / 35Heyting algebra
Definition
A Heyting algebra H = ⟨H, ∧, ∨, 1, 0, →⟩ is a bounded distributive latticeequipped with a binary operation → s.t. a ∧ b ≤ c ⇔ a ≤ b → c.
Remark: any Heyting algebra can be seen as a posetal Cartesian closed
category with finite coproducts.
Example:Any bounded chain can be regarded as a Heytingalgebra with{1 a≤ba→b=b o.w .

H• 1H••ba• 0H
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

7 / 35

S4 algebra

Definition
An S4 algebra B = ⟨B, ∧, ∨, −, 1, 0, □⟩ is a Boolean algebra equipped witha unary operation □ s.t. □(a ∧ b) = □a ∧ □b, □1 = 1, □a ≤ a and□a ≤ □□a.
Remark: any S4 algebra can be seen as a posetal category with a comonad□ which preserves finite products.
Example:Let X = ⟨X , τ ⟩ be a topological space and int an interior operator.
Then ⟨P(X ), ∩, ∪, ∼, X , ∅, int⟩ is an S4 algebra.

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

8 / 35

Kleisli construction

Definition
B : an S4 algebra.
A Kleisli order ≤□ on B is defined by a ≤□ b ⇔ □a ≤ b.
B□ := ⟨B, ≤□ ⟩/ ∼ where a ∼ b ⇔ a ≤□ b and b ≤□ a.
B□ := ⟨B□ , ∨□ , ∧□ , 1□ , 0□ , →□ ⟩ where[a] ∧□ [b] = [a ∧ b],[a] ∨□ [b] = [□a ∨ □b],1□ = [1],0□ = [0], and[a] →□ [b] = [□a → b].

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

9 / 35

Kleisli constructionLemma
B : an S4 algebra.
Then, B□ is a Heyting algebra.
Remark: B□ is a Kleisli category of □. (In this case, the Kleisli-cat. and theEM-cat. of a posetal category B are categorically equivalent.)

The Kleisli construction can be extended to a functor (−)□ : S4 −→ Hey.

Lemma
B1 , B2 : S4 algebras, f : B1 → B2 : an S4 homomorphism.
Define a map f□ : B1□ → B2□ by f□ ([a]1 ) = [f (a)]2 .
Then f□ is a Heyting homomorphism.

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

10 / 35

Kleisli construction
Definition
S4 : the category of S4 algebras and homomorphisms.
Hey : the category of Heyting algebras and homomorphisms.
S4emb : the category of S4 algebras and embeddings.
Heyemb : the category of Heyting algebras and embeddings.
S4emb

S4SI

S4(−)□(−)□

Heyemb

Kanako KOBAYASHI (Kyoto Univ.)

HeySI

Co-lifting and its S4 analogueHey

2018/10/08

11 / 35

Kleisli construction
Definition
S4 : the category of S4 algebras and homomorphisms.
Hey : the category of Heyting algebras and homomorphisms.
S4emb : the category of S4 algebras and embeddings.
Heyemb : the category of Heyting algebras and embeddings.
Boolntemb × S4emb

S4SIS4p



(−)□

S4emb
(−)□



Heyemb
Kanako KOBAYASHI (Kyoto Univ.)

HeySI
Co-lifting and its S4 analogueHey
2018/10/08

11 / 35

Kleisli construction
Definition
S4 : the category of S4 algebras and homomorphisms.
Hey : the category of Heyting algebras and homomorphisms.
S4emb : the category of S4 algebras and embeddings.
Heyemb : the category of Heyting algebras and embeddings.
Boolntemb × S4emb

S4SIS4(−)□(−)□

Heyemb

Kanako KOBAYASHI (Kyoto Univ.)

HeySI

Co-lifting and its S4 analogueHey

2018/10/08

11 / 35

Kleisli construction

The Kleisli construction (−)□ : S4 −→ Hey preservescongruence lattices andsubdirect irreducibility.

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

12 / 35

Congruence lattice
Definition (Universal algebra)
A : an algebra.
An equivalence relation θ on A is called congruence on A if it
preserves algebraic operations of A.
Write Con(A) for the congruence lattice of A.
In general:

Example: bounded chain (as a Heyting algebra).
H• 1Con(A)A2θa∆Kanako KOBAYASHI (Kyoto Univ.)• a′• a• 0Co-lifting and its S4 analogueCon(H)•θ0 = H 2••θa ′θa•θ1 = ∆
2018/10/08

13 / 35

Congruence lattice

The Kleisli construction (−)□ : S4 −→ Hey preserves congruence lattices.

Lemma
B : an S4 algebra, θ ∈ Con(B).
Con(B) ∼= Con(B□ )∼(B/θ)□ = B□ /θ□Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

14 / 35

Subdirectly irreducible
Definition (Universal algebra)
A, Ai (i ∈ I ): algebras.
We call A a subdirect product of {Ai }i∈I if e : A ↣each pi ◦ e is surjective.
A /ep◦e/∏∏i∈I Ai wherei∈I Ai&& pAi

A is called subdirectly irreducible (s.i. for short) if A cannot be
decomposed as a subdirect product.
Example: Every finite chain is s.i. as a Heyting algebra.
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

15 / 35

Subdirectly irreducible

Theorem (Fundamental Theorem of Universal Algebra)
Every algebra is isomorphic to a subdirect product of s.i. algebras.
Example:
• ω/

• 2
• 1
• 0

Kanako KOBAYASHI (Kyoto Univ.)

/

• n
• n−1

∏
n∈ω

•
•
•

Co-lifting and its S4 analogue

210

2018/10/08

16 / 35

Monolith
Definition (Universal algebra)
A : an algebra.
A monolith of A (write µA ) is the 2nd-minimum congruence of A (if any).

Lemma (Universal algebra)
A : an algebra.
A is s.i. ⇔ A has a monolith.

Con(A)A2µA∆

The Kleisli construction (−)□ : S4 −→ Hey preserves s.i.

Corollary
B : an S4 algebra. Then, B is s.i. ⇔ B□ is s.i.
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

17 / 35

OpremumDefinition
H : a Heyting algebra.
An opremum of H (write ⋆H ) is the 2nd-largest element of H (if exists).

Definition
B : an S4 algebra.
An opremum of B is (intuitively) a 2nd-largest element of B according
to the Kleisli order ≤□(i.e. an elements a ∈ B \ {1B } s.t. ∀b ∈ B \ {1B } □b ≤ a if exists).
Write Op(B) for the set of oprema of B.
Write ⋆B for the minimum opremum of B (if exists).
(Op(B) ̸= ∅ ⇒ ⋆B exists.)

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

18 / 35

OpremumLemma
A : an algebra (Heyting or S4).
A is s.i. ⇔ A has a monolith ⇔ A has an opremum.
s.i. Heyting algebras.i. S4 algebra

1B1H⋆HOp(B)⋆B

0H
0B
The Kleisli construction (−)□ : S4 −→ Hey preserves oprema.

Lemma
B : an s.i. S4 algebra. Then, ⋆B□ = Op(B) = [⋆B ].
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

19 / 35

What we have obtained so far
Definition
S4SI : the category of s.i. S4 algebras and opremum preserving
homomorphisms.
HeySI : the category of s.i. Heyting algebras and opremum preserving
homomorphisms.
S4embS4SI(−)□

S4(−)□(−)□



Heyemb

Kanako KOBAYASHI (Kyoto Univ.)



HeySI

Co-lifting and its S4 analogue

Hey

2018/10/08

20 / 35

Outline

1Introduction

2

Basic Definitions

3

Co-lifting of Heyting Algebras

4S4 analogue of co-lifting

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

21 / 35

Co-lifting of Heyting algebras
Definition
Heyemb : the category of Heyting algebras and embeddings.
HeySI : the category of s.i. Heyting algebras and opremum-preserving
homomorphisms.
Here, we will describe the following equivalence:S4emb(−)□

S4SI

$ 

∼
=(−)□

(−)□

(−)⊤

HeyembdS4HeySI

Hey−/µKanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

22 / 35

Co-lifting (−)⊤ : Heyemb −→ HeySIDefinition
H : a Heyting algebra.
A co-lifting of H (write H⊤ ) is obtained by adding a new top-element
above the top of H.
• ⊤
• 1H
• 1H


/

• 0H

• 0H

This is an s.i. Heyting algebra.
Remark: H⊤ is the subscone (injective scone) of H:H⊤

/ Sub(Sets)HKanako KOBAYASHI (Kyoto Univ.)

H(1,−)

cod/ Sets

Co-lifting and its S4 analogue

2018/10/08

23 / 35

Co-lifting (−)⊤ : Heyemb −→ HeySI
Co-lifting can be extended to a functor (−)⊤ : Heyemb −→ HeySI .

Lemma
H1 , H2 : Heyting algebras, f : H1 → H2 : Heyting homomorphism.
⊤If f is an embedding, then the natural extension f ⊤ : H⊤
1 → H2 is an
opremum-preserving hom.
•f⊤

•

/•H1
•
Kanako KOBAYASHI (Kyoto Univ.)•f/H2•

Co-lifting and its S4 analogue

2018/10/08

24 / 35

Quotient modulo the monolith −/µ : HeySI −→ Heyemb•

Quotient modulo the monolith:•

•/µ/••LemmaH : an s.i. Heyting algebra.
(H/µH )⊤ ∼= H.
This can be extended to a functor −/µ : HeySI −→ Heyemb .

Lemma
H1 , H2 : s.i. Heyting algebras, f : H1 → H2 Heyting homomorphism,
If f preserves the opremum, then there is f ′ : H1 /µH1 ↣ H2 /µH2 .

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

25 / 35

Consequence
Definition
Heyemb : the category of Heyting algebras and embeddings.
HeySI : the category of s.i. Heyting algebras and opremum-preserving
homomorphisms.

TheoremHeyemb ∼= HeySI .
S4emb
(−)□

S4SI

∼
=(−)□

(−)□

(−)⊤

HeyembcS4$ HeySIHey−/µKanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

26 / 35

Outline

1

Introduction

2

Basic Definitions

3

Co-lifting of Heyting Algebras

4S4 analogue of co-lifting

Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

27 / 35

S4 analogue of co-lifting
Definition
Boolntemb : the category of non-trivial Boolean algebras and embeddings.
Here, we will show the following equivalence and commutativity(up-to-iso) of the diagram:
Boolntemb × S4embg&

∼
=S4SI

S4(−)□

(−)□

(−)□

(−)⊤



Heyembf∼
=&

HeySI



Hey−/µKanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

28 / 35• construction: S4-analogue of co-lifting (−)⊤
Definition
I : a non-trivial Boolean algebra, B = ⟨B, □B ⟩ : an S4 algebra.
Let I • B := ⟨I × B, □⟩ where □ : I × B → I × B is defined by{⟨1I , 1B ⟩⟨i, a⟩ = ⟨1I , 1B ⟩□⟨i, a⟩ =⟨0I , □B a⟩ o.w .
⟨1I ,1B ⟩•
•I•b•

□

•• c□□••□B

B
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

29 / 35• construction: S4-analogue of co-lifting (−)⊤
Lemma
I: a non-trivial Boolean algebra, B: an S4 algebra.
I • B is an s.i. S4 algebra with Op(I • B) = {⟨i, 1B ⟩ | i ∈ I \ {1I }}•Op(I•B) ••
•I

B

Lemma
I: a non-trivial Boolean algebra, B: an S4 algebra.
(I • B)/µI•B ∼=B
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

30 / 35

Decomposition into • algebra
Lemma
B: an s.i. S4 algebra.
IB • (B/µB ) ∼= B where the Boolean algebra IB is defined bybase set IB := Op(B) ∪ {1B }∧, ∨, 1I are same as those of B
−i = −B i ∨ ⋆B
0I = ⋆B
1BIB⋆B
0B
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

31 / 35

Consequence
Definition
Boolntemb : the category of non-trivial Boolean algebras and embeddings.
S4emb : the category of S4 algebras and embeddings.
S4SI : the category of s.i. S4 algebras and opremum-preserving
homomorphisms.
(−)•(−)

Boolntemb × S4embg&

∼
=

S4SI

S4

⟨I(−) ,(−)/µ⟩
(−)□

(−)□

(−)□

(−)⊤

Heyembf∼=&

HeySI

Hey−/µKanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

32 / 35Commutativity of co-lifting and Kleisli construction
Lemma
I : a non-trivial Boolean algebra, B : an S4 algebra.
(I • B)□ ∼= (B□ )⊤ .
Remark: B□ is same as a sublattice of B that consists of box-stableelements {a ∈ B | □a = a} (i.e. EM-cat. of ⟨B, □⟩).
•
•
I•b
•

□

•

•

•

Kanako KOBAYASHI (Kyoto Univ.)=⊤□• cB□•□

Co-lifting and its S4 analogue•= B□

2018/10/08

33 / 35

SummaryWe refined the co-lifting of Heyting algebras (appeared in Wrónski1973) as a categorical equivalence,
proposed the • construction as S4 analogue of co-lifting,and showed correspondence of co-lifting and • construction via theKleisli construction.
Boolntemb × S4emb

∼
=S4SI

S4(−)□

(−)□

(−)□



Heyemb

Kanako KOBAYASHI (Kyoto Univ.)∼=HeySICo-lifting and its S4 analogue

Hey

2018/10/08

34 / 35

Application
Theorem (Wrónski, 1973)
There are 2ω intermediate logics having the disjunction property (DP).
There is a map τ : Ext(Int) → NExt(S4) preserving the disjunction
property. So, as an immediate consequence of Wrónski’s theorem, we get:Corollary
There are 2ω extensions of the modal logic S4 with the disjunction
property.
As an application of our work, we get new logics with DP:

Proposition (new result)
There are infinitely many extensions of S4 which have the disjunction
property and cannot be expressed as τ L.
Kanako KOBAYASHI (Kyoto Univ.)

Co-lifting and its S4 analogue

2018/10/08

35 / 35