The categorical equivalence between disjunctive sequent calculi and algebraic L-domains

TL;DR

This paper demonstrates a categorical equivalence between disjunctive sequent calculi and algebraic L-domains, using logical states and consequence relations to connect syntactic and semantic structures.

Contribution

It introduces a purely syntactic representation of algebraic L-domains and establishes a categorical equivalence with disjunctive sequent calculi via consequence relations.

Findings

Categorical equivalence between disjunctive sequent calculi and algebraic L-domains.

Logical states as a bridge between syntax and semantics.

Representation of Scott-continuous functions through consequence relations.

Abstract

This paper establishes a purely syntactic representation for the category of algebraic L-domains with Scott-continuous functions as morphisms. The central tool used here is the notion of logical states, which builds a bridge between disjunctive sequent calculi and algebraic L-domains. To capture Scott-continuous functions between algebraic L-domains, the notion of consequence relations between disjunctive sequent calculi is also introduced. It is shown that the category of disjunctive sequent calculi with consequence relations as morphisms is categorical equivalent to that of algebraic L-domains with Scott-continuous functions as morphisms.

Equations

$$\{d\in P\mid (\exists x\in X)d\le x\},$$

$$\{d\in P\mid (\exists x\in X)x\le d\}.$$

$$\left(\text{At}\right)\frac{\varphi \in P}{\varphi \in \mathcal{L}(P)}$$

$$\left(\text{Conj}\right)\frac{\varphi ,\psi \in \mathcal{L}(P)}{\varphi \wedge \psi \in \mathcal{L}(P)}$$

$$\left(\text{Ax}\right)\frac{(\Gamma ⊢\text{F})\in {\mathcal{A}}_P}{\Gamma ⊢\text{F}}$$

$$\left(\text{Lwk}\right)\frac{\Gamma ⊢\psi \varphi \in \mathcal{L}(P)}{\Gamma ,\varphi ⊢\psi }$$

$$\left(\text{LF}\right)\frac{\varphi \in \mathcal{L}(P)}{\text{F}⊢\varphi }$$

$$\left(\text{L}\wedge \right)\frac{\Gamma ,\varphi ,\psi ⊢\theta }{\Gamma ,\varphi \wedge \psi ⊢\theta }$$

$$\left(\text{L}\dot{\vee }\right)\frac{\Gamma ,{\varphi }_i⊢\theta (alli\in I){\varphi }_i,{\varphi }_j⊢\text{F}(alli\ne j\in I)}{\Gamma ,{\dot{\bigvee }}_{i\in I}{\varphi }_i⊢\theta }$$

$$\left(\text{R}\dot{\vee }\right)\frac{\Gamma ⊢{\varphi }_{i_0}(some{i}_0\in I){\varphi }_i,{\varphi }_j⊢\text{F}(alli\ne j\in I)}{\Gamma ⊢{\dot{\bigvee }}_{i\in I}{\varphi }_i}.$$

$$(\Gamma ,\phi )\in ⊩\mathrm{if}\mathrm{and}\mathrm{only}\mathrm{if}\mathrm{the}\mathrm{sequent}\Gamma ⊢\phi \mathrm{is}\mathrm{valid}.$$

$$X[⊢]=\{\phi \in \mathcal{L}(P)\mid (\exists \Gamma ⊑X)\Gamma ⊢\phi \in \mathbf{T}(P)\}$$

$$[X{]}_S=\bigcap \{W\in |(\mathcal{L}(P),⊢)|\mid X\subseteq W\subseteq S\}$$

$$\sup \{S_i\mid i\in I\}=\bigcup \{S_i\mid i\in I\}.$$

$$P_D=\{\uparrow x\mid x\in K^{\ast }(D)\}$$

$$\mathcal{A}=\{p_1,p_2,\dots ,p_n{⊢}_D\mathrm{F}\mid p_i\in P_D,p_1\cap p_2\cap \dots \cap p_n=\varnothing \}$$

$$(\Gamma ,\phi )\in {⊢}_D\mathrm{if}\mathrm{and}\mathrm{only}\mathrm{if}\widehat{{\psi }_1}\cap \widehat{{\psi }_2}\cap \cdots \cap \widehat{{\psi }_n}\subseteq \hat{\phi }$$

$$\{\hat{\phi }\mid \phi \in \mathcal{L}(P_D)\}=\mathcal{U}(D).$$

$$\hat{S}=\{\hat{\phi }\mid \phi \in S\}.$$

$$f:(D,\le )\to (|(\mathcal{L}(P_D),{⊢}_D)|,\subseteq ),$$

$$d\mapsto \{\phi \in \mathcal{L}(P_D)\mid d\in \hat{\phi }\}.$$

$$\{\phi \in \mathcal{L}(P_D)\mid \hat{\phi }\in \mathcal{U}(D),d_1\in \hat{\phi }\}\subseteq \{\phi \in \mathcal{L}(P_D)\mid \hat{\phi }\in \mathcal{U}(D),d_2\in \hat{\phi }\}.$$

$$\Theta [X]=\{\phi \in \mathcal{L}(Q)\mid (\exists \mu \in X\cap \mathcal{I}\mathcal{C}(P))(\mu ,\phi )\in \Theta \}.$$

$$f_{\Theta }(S)=\Theta [S].$$

$$(\mu ,\psi )\in {\Theta }_f\iff \psi \in f(\{\mu \}[{⊢}_P]).$$

$$(\mu ,\phi )\in {\Theta }_{f_{\Theta }}$$

$$\iff \phi \in \Theta [\{\mu \}[{⊢}_P]]$$

$$\iff (\exists \nu \in \mathcal{I}\mathcal{C}(Q)((\mu ,\phi )\in \Theta ,\mu {⊢}_P\nu \in \mathbf{T}(P)))$$

$$\iff (\mu ,\phi )\in \Theta .$$

$$f_{{\Theta }_f}(S)$$

$$=\{\phi \in \mathcal{L}(Q)\mid (\exists \mu \in S\cap \mathcal{I}\mathcal{C}(P))(\mu ,\phi )\in {\Theta }_f\}$$

$$=\{\phi \in \mathcal{L}(Q)\mid (\exists \mu \in S\cap \mathcal{I}\mathcal{C}(P))\phi \in f(\{\mu \}[{⊢}_P])\}$$

$$=\bigcup \{f(\{\mu \}[{⊢}_P])\mid \mu \in S\cap \mathcal{I}\mathcal{C}(P)\}$$

$$=f(\bigcup \{\{\mu \}[{⊢}_P]\mid \mu \in S\cap \mathcal{I}\mathcal{C}(P)\}$$

$$=f(S).$$

$$(\mu ,\psi )\in {\Omega }_h\iff f(\mu )\subseteq \psi .$$

Full text

1 Introduction

Domains with Scott-continuous functions, introduced by Scott and Strachey in the 1970s (see[1, 2]), form a foundational denotational semantics for functional programming languages in computer science. Apart from the extensive applications in computer science, domains are the important objects discussed in mathematics and have overlaps with order theory, topology, logic, formal concept analysis and category theory (see[3, 4, 5, 6, 7, 8]). The connection between logic and domains is intricate and well-known. One aspect of the connection between logic and domains is that domains can be presented by logical languages, and this connection has demonstrated by Scott’s information systems [9] and Amramsky’s domain logic [10, 11].

Scott first demonstrated the possibility of logic syntactic representation for Scott domains by the notion of information systems [9]. An information system is a triple $(X,Con,\vdash)$, which is introduced and used to substitute for the domain-theoretical approach to the semantics of functional programming languages. Here $X$ is a set of atomic formulae and $Con$ is a collection of finite subsets of atomic formulae. $\vdash$ is an entailment relation from $Con$ to $X$ and tells us what atomic formulae can be entailed from a member of $Con$. A Scott domain can be formed by taking those subsets of $X$ closed under the entailment relation $\vdash$ as the points, and this kind of construction of domains is easy to understand for computer scientists [9]. In [12], the category of Scott domains with Scott-continuous functions as morphisms was also shown to be equivalent to that of Scott’s information systems with approximable mappings as morphisms. Now, a lots of information systems have been introduced and used to represent various domains (see[13, 14, 15, 16]).

In a logical semantics theoretical development, Abramsky devised a complete logic description for Scott domains and show how the domain logic can be usefully employed in denotational semantics [10]. Abramsky’s domain logic, as well as Scott’s information system, is made by extracting an appropriate logical language from the category of Scott domains with Scott-continuous functions as morphisms. However, it allows logical formulae can be combined by connectives, and it has more functional properties than information systems from a perspective of program logic interpretation. His work was technically demanding but rewarding, recognised in the first LICS ”test of time” award. Many researchers have tried to apply Abramsky’s program to other classes of domains (see [17, 18, 19, 20, 21]). The most related work for us is due to Chen and Jung’s paper [22], in which they developed a framework of disjunctive propositional logic and provided a logic algebraic representation for the category of algebraic L-domain with stable functions as morphisms using its Lindenbaum algebra.

This paper aims to introduce a logical syntactic representation for algebraic $L$-domains from the categorical viewpoint. Although the investigation is inspired by the work of Chen and Jung [22], our approach differs greatly. We not only provide a purely syntactic representation of algebraic $L$-domains, but also we are particularly interest in the suitable logical representation of Scott-continuous functions between algebraic $L$-domains.

In Section 3.1, based on the analysis of some properties of contradiction, tautology, satisfiable formula and conjunction in a disjunctive propositional logic, the concept of logical states in a disjunctive propositional logic is proposed. A logical state is a pattern of formulae that satisfies two conditions, and there are two methods for generating logical states. In Section 3.2, it is shown that the collection of all logical states of a disjunctive propositional logic ordered by set inclusion forms an algebraic $L$-domain. Conversely, each algebraic $L$-domain can be generated in this way, up to isomorphism. Then a new representation theorem for algebraic L-domains is obtained: instead of making use of the Lindenbaum algebra of the disjunctive propositional logic, the whole process simply employs the satisfies formulae of disjunctive propositional logic.

There is another difference from the work by Chen and Jung [22]: the morphisms between algebraic L-domains that they discussed was stable functions, which are fairly strict about the Scott-continuous functions between algebraic L-domains. It is well known that Scott-continuous functions are typically used as morphisms between algebraic L-domains to form a cartesian closed category $\mathbf{ALD}$. In Section 4, we introduce a consequence relation between expressive disjunctive sequent calculi, which has some similar features to a consequence relation between multi lingual sequent calculi introduced in [17]. We show that there is a one to one correspondence between consequence relations on expressive disjunctive sequent calculi and Scott-continuous functions on algebraic $L$-domains. Finally, we establish a logic category which is cartesian closed and equivalent to $\mathbf{ALD}$. This result provides a logical characterization for denotational semantics of functional programming languages and a potential valuable application in theoretical computer science.

2 Preliminaries

We first recall some basic definitions and notations which will be used in this article.

2.1 Order and domain theoretical notations

Our order and domain theoretical notation and terminology are standard, most of them come from [23, 24, 25].

Let $P$ be a poset. If $P$ has a least element $\bot$, then $P$ is called pointed. A nonempty subset $D$ of a $P$ is said to be directed if every pair of elements of $D$ has an upper bound in $D$. We use $\mathord{\downarrow}X$ to denote the down set

[TABLE]

where $X$ is a subset of $P$. Similarly, we write $\mathord{\uparrow}X$ for the upper set

[TABLE]

If $X$ is a singleton $\{x\}$, then we just write $\mathord{\downarrow}x$ or $\mathord{\uparrow}x$. $X$ is a pairwise inconsistent subset of $P$ if $\mathord{\uparrow}x\cap\mathord{\uparrow}y=\emptyset$ for all $x\neq y\in X$. $P$ is said to be a complete lattice if each subset $X$ of it has a supremum $\mathrm{sup}X$. A dcpo $P$ is a poset in which every directed subset $D$ has a supremum $\mathrm{sup}D$.

Let $P$ be a dcpo and $x\in P$. If for all directed subset $D$ of $P$ the relation $x\leq\mathrm{sup}D$ always implies the existence of some $d\in D$ with $x\leq d$, then $x$ is called a compact element of $P$. We write $K(P)$ for the set of compact elements of $P$ and write $K^{*}(P)$ for $K(P)-\{\bot\}$.

Definition 2.1

[25]**

1. (1)

A pointed dcpo $P$ is called an algebraic domain if every element $x$ of $P$ is the directed supremum of the compact elements below $x$. 2. (2)

An algebraic $L$-domain $P$ is any algebraic domain in which for all element $x\in P$, $\mathord{\downarrow}x$ is a complete lattice.

Noting that an algebraic $L$-domain $P$ satisfies the following property: For all nonempty finite subset $\{x_{1},x_{2},\cdots,x_{n}\}$ of $K(P)$ with an upper bound in $P$, there exists a unique nonempty pairwise inconsistent subset $A\subseteq K(P)$ such that $\mathord{\uparrow}x_{1}\cap\mathord{\uparrow}x_{2}\cap\cdots\cap\mathord{\uparrow}x_{n}=\bigcup_{a\in A}\mathord{\uparrow}a$. In fact, the set $A$ just is the minimal upper bounds of $\{x_{1},x_{2},\cdots,x_{n}\}$.

Definition 2.2

[25]**

Let $P$ and $Q$ be algebraic $L$-domains. A function $f:P\rightarrow Q$ is Scott-continuous if and only if for all directed subset $D$ of $P$, $f(\mathrm{sup}D)=\mathrm{sup}\{f(x)\mid x\in D\}.$

2.2 Disjunctive propositional logic

Based on the work by Chen on stable domains [26] and the work by Zhang on disjunctive information systems [27], a disjunctive propositional logic was introduced in [22, Definition 2.1].

The connectives of a disjunctive propositional logic consists of two unitary constant connectives T and F, a binary conjunctive connective $\wedge$ and an arbitrary, but provably disjoint, disjunctive connective $\dot{\bigvee}$. Starting with a set of atomic formulae and a set of atomic disjointness assumptions, disjunctive formulae are built. And in a disjunctive propositional logic, a sequent is an object $\Gamma\vdash\varphi$, in which $\Gamma$ is a finite set of formulae and $\varphi$ is a single formula. In the sequel, we use $A\sqsubseteq B$ to denote $A$ is a finite subset of $B$.

Definition 2.3

([22])**

Let $P$ be a set, every element of which is called an atomic formula. Likewise, let $\mathcal{A}_{P}$ be a set of sequents of the form $p_{1},p_{2},\ldots,p_{n}\vdash F$ where the $p_{i}$ are atomic formulae, and F is the syntactic constant for “false”. Each element of $\mathcal{A}_{P}$ is called an atomic disjointness assumptions, and the pair $(P,\mathcal{A}_{P})$ is called a disjunctive basis.

The set $\mathcal{L}(P)$ of formulae, and the set $\mathbf{T}(P)$ of valid sequents are generated by mutual transfinite induction by the following rules:

1. $\bullet$

Disjunctive formulae

[TABLE] 2. $\bullet$

Valid sequents

[TABLE]

[TABLE]

[TABLE]

The proof system of a disjunctive propositional logic is sound and complete with respect to its Lindenbaum algebra [22].

With respect to the disjunctive propositional logic proposed in Definition 2.3, we can define a binary relation $\Vdash$ between the finite subsets of $\mathcal{L}(P)$ and the set $\mathcal{L}(P)$ as following:

[TABLE]

In other words, a valid sequent $\Gamma\vdash\varphi$ and $(\Gamma,\varphi)\in\Vdash$ are mutual determined. Then the disjunctive propositional logic can be seen as a pair $(\mathcal{L}(P),\Vdash)$ such that $\mathcal{L}(P)$ and $\Vdash$ are closed under the rules of disjunctive formulae and valid sequents. In this article no differentiation between $\Vdash$ and $\vdash$ is made for convenience, and the pair $(\mathcal{L}(P),\vdash)$ is called a disjunctive sequent calculus.

Proposition 2.1

([22])**

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus. Then the following statements hold.

1. (1)

$\Gamma,\varphi,\psi\vdash\phi$* is a valid sequent if and only if $\Gamma,\varphi\wedge\psi\vdash\phi$ is a valid sequent.* 2. (2)

$\Gamma\vdash\varphi$* and $\Gamma\vdash\psi$ are valid sequents if and only if $\Gamma\vdash\varphi\wedge\psi$ is a valid sequent.* 3. (3)

Assuming $\phi_{i},\phi_{j}\vdash\emph{F}$ are valid sequents for all $i\neq j\in I$, then $\Gamma,\phi_{i}\vdash\theta$ are valid sequents if and only if $\Gamma,\dot{\bigvee}_{i\in I}\phi_{i}\vdash\theta$ is a valid sequent.

In the scheme of the Lindenbaum algebra of a disjunctive propositional logic, Chen studies the Stone duality and a logic algebraic representation for the category of algebraic L-domain with stable functions as morphisms [26].

Instead of using the Linderbaum algebra of a disjunctive propositional logic, we turn to provide a logical syntactic representation of algebraic $L$-domains using the proof system of a disjunctive propositional logic. Moreover, in viewpoint of category, the morphisms between algebraic $L$-domains what we focus on are Scott-continuous functions which are typically employed in domain theory.

3 Logical representation

In this section, we show how to use the disjunctive sequent calculi to represent algebraic L-domains. We unfold completely in the class $\mathcal{L}(P)$ of a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$, without assistance of any object except valid sequents.

3.1 Logical states

We begin by introducing some common terms in a disjunctive sequent calculus.

Definition 3.1

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus.

1. (1)

A formula $\varphi$ is said to be a tautology if the sequent $\emph{T}\vdash\varphi$ is valid. 2. (2)

A formula $\varphi$ is said to be a contradiction if the sequent $\varphi\vdash\emph{F}$ is valid. 3. (3)

A formula $\varphi$ is said to be satisfiable if it is neither a tautology nor a contradiction.

Given an atomic formula $p$ of a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$, it is easy to see that the formula $\mathrm{F}\wedge p$ is a contradiction and the formula $\mathrm{T}\dot{\bigvee}(\mathrm{F}\wedge p)$ is a tautology. We denote by Tau$(P)$ and Cont$(P)$ the set of all tautologies and the set of all contradictions, respectively.

Definition 3.2

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus and $\varphi,\psi\in\mathcal{L}(P)$. If both $\varphi\vdash\psi$ and $\psi\vdash\varphi$ are valid sequents, then $\varphi$ and $\psi$ are said to be logically equivalent.

Noting that in [22], two logically equivalent formulae are called interderivable.

Definition 3.3

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus.

1. (1)

A conjunction is a satisfiable formula that built up from atomic formulae only by conjunctive connectives. 2. (2)

A flat formula is a satisfiable formula that has the form $\dot{\bigvee}_{i\in I}\mu_{i}$, where $\mu_{i}$ are conjunctions and $\mu_{i},\mu_{j}\vdash\emph{F}$ are valid for all $i\neq j\in I$.

Proposition 3.1

([22])**

Every satisfiable formula in a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$ is logically equivalent to a flat formula $\dot{\bigvee}_{i\in I}\mu_{i}$, where $I$ is a nonempty set and $\mu_{i}$ are conjunctions for all $i\in I$.

We denote by $\mathcal{N}(P)$ the set of all flat formulae in a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$. Next we will present the notion of a logical state, which constructs an important bilateral link between disjunctive sequent calculi and algebraic $L$-domains. The name of a logical state borrows from the notion of a “state” in information systems(see [13, 14]).

Definition 3.4

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus. A logical state of $(\mathcal{L}(P),\vdash)$ is a nonempty proper subset $S$ of $\mathcal{L}(P)$ such that the following conditions hold:

1. (S1)

If $\dot{\bigvee}_{i\in I}\mu_{i}\in S\cap\mathcal{N}(P)$, then there exists some $i_{0}\in I$ such that $\mu_{i_{0}}\in S,$. 2. (S2)

$S[\vdash]\subseteq S$, where

[TABLE]

for all $X\subseteq\mathcal{L}(P)$.

We denote by $|(\mathcal{L}(P),\vdash)|$ the set of all logical states of a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$.

Let $\varphi$ be a satisfiable formula in $S$. As we have seen in Proposition 3.1 there is a flat formula $\dot{\bigvee}_{i\in I}\mu_{i}$ logically equivalent to the formula $\varphi$. Condition (S2) suggests that the formula $\dot{\bigvee}_{i\in I}\mu_{i}$ is a member of $S$. Then by condition (S1) we have some $i_{0}\in I$ such that the conjunction $\mu_{i_{0}}$ is also a member of $S$. Moreover, condition (S2) indicates that a logical state $S$ is closed under $\vdash$. The following proposition shows that $S$ is closed under $\wedge$.

Proposition 3.2

Let $S$ be a logical state of a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$. Then the following statements hold.

1. (1)

If $\varphi,\psi\in S$, then $\varphi\wedge\psi\in S$. 2. (2)

The constant F does not belong to $S$. 3. (3)

$S=S[\vdash]$. 4. (4)

If $\varphi\in S$ and $\varphi\wedge\psi\vdash\emph{F}$ is valid, then $\psi\notin S$. 5. (5)

If $X$ is a subset of $S$, then

[TABLE]

is also a logical state.

$\mathbf{Proof.}$

(1) By Definition 2.3 and Proposition 2.1, $\varphi,\psi\vdash\varphi\wedge\psi$ is a valid sequent. Then according to Equation 3.1 and condition (S2), we have $\varphi\wedge\psi\in S$.

(2) Suppose not, then $\text{F}\in S$. By the rule (LF), $\text{F}\vdash\psi$ is valid for any $\psi\in\mathcal{L}(P)$. Thus $\mathcal{L}(P)\subseteq S\subseteq\mathcal{L}(P)$. This contradicts the fact that $S$ is a proper subset of $\mathcal{L}(P)$.

(3) $S[\vdash]\subseteq S$ just is an application of condition $(S2)$, and $S\subseteq S[\vdash]$ follows immediately by Equation 3.1 and the rule (Id).

(4) This follows from parts (2) and (3).

(5) According to Equation 3.1 and the rule (RT), it follows that the constant $\mathrm{T}$ is a member of $S$. This implies that $[X]_{S}$ is nonempty.

Assume that $\dot{\bigvee}_{i\in I}\mu_{i}\in[X]_{S}\cap\mathcal{N}(P)$. Then by Equation 3.2, we have $\dot{\bigvee}_{i\in I}\mu_{i}\in W$ for all $W\in|(\mathcal{L}(P),\vdash))|$ with $X\subseteq W\subseteq S$. Since $W$ is a logical state, there exists some $i_{W}\in I$ such that $\mu_{i_{W}}\in W\subseteq S$. Thus $\{\mu_{i_{W}}\mid W\in|(\mathcal{L}(P),\vdash)|,X\subseteq W\subseteq S\}$ is a subset of $S$. Note that $\mu_{i},\mu_{j}\vdash\text{F}$ is valid for all $i\neq j\in I$ and $S$ is a logical state, it is not difficult to show that the set $\{\mu_{i_{W}}\mid W\in|(\mathcal{L}(P),\vdash)|,X\subseteq W\subseteq S\}$ is a singleton. This implies that there exists some $i_{0}\in I$ such that $\mu_{i_{0}}\in[X]_{S}$. Therefore, we have shown that $[X]_{S}$ satisfies condition (S1).

For condition (S2), assume that $\varphi\in[X]_{S}[\vdash]$. Then there exists some $\Gamma\sqsubseteq[X]_{S}$ such that $\Gamma\vdash\varphi$. Thus $\Gamma\sqsubseteq W$ for any $W\in|(\mathcal{L}(P),\vdash)|$ with $X\subseteq W\subseteq S$. Since $W$ is a logical state and $\Gamma\vdash\varphi$, it follows that $\varphi\in W$, and therefore $\varphi\in[\Gamma]_{S}$. $\square$

Proposition 3.3

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus. Then the following statements hold.

1. (1)

Tau$(P)$* is a logical state but Cont$(P)$ is not.* 2. (2)

The union of a directed subset of logical states is a logical state.

$\mathbf{Proof.}$

(1) Since Tau$(P)\cap\mathcal{N}(P)=\emptyset$, Tau$(P)$ naturally fulfills condition (S2). By the definitions of a tautology and Tau$(P)[\vdash]$, it is easy to see that Tau$(P)[\vdash]\subseteq\text{Tau}(P)$. Consequently, Tau$(P)$ is a logical state.

According to part (3) of Proposition 3.2, it follows that Cont$(P)$ is not a logical state .

(2) For a directed set of logical states $\{S_{i}\mid i\in I\}$, set $S=\bigcup\{S_{i}\mid i\in I\}$. We show that $S$ is a logical state by checking that $S$ satisfies conditions $(S1)$ and $(S2)$.

To prove condition $(S1)$, let $\dot{\bigvee}_{j\in J}\mu_{j}\in S\cap\mathcal{N}(P)$. Then $\dot{\bigvee}_{j\in J}\mu_{j}\in S_{i}\cap\mathcal{N}(P)$ for some $i\in I$. Thus there exists some $j_{i}\in J$ such that $\mu_{j_{i}}\in S_{i}\subseteq S$ because $S_{i}$ is a logical state.

For condition $(S2)$, let $\varphi\in S[\vdash]$. By equation (3.1), there exists some $\Gamma\sqsubseteq S$ such that $\Gamma\vdash\varphi$. From the fact that $\Gamma\sqsubseteq S$ and the set $\{S_{i}\mid i\in I\}$ is directed, it follows that $\Gamma\sqsubseteq S_{i_{0}}$ for some $i_{0}\in I$. Since $S_{i_{0}}$ is a logical state, we have $\varphi\in S_{i_{0}}\subseteq S$. Therefore, $S[\vdash]\subseteq S$. $\square$

Part (5) of Proposition 3.2 and part (2) of Proposition 3.3 present two methods for deriving new logical states. Part (1) of Proposition 3.3 shows there is a trivial logical state Tau$(P)$ for all disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$. We now show there are enough many nontrivial logical states. To this end, we need a further definition.

Definition 3.5

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus.

1. (1)

A conjunction $\mu$ is said to be irreducible if, whenever $\mu\vdash\dot{\bigvee}_{i\in I}\phi_{i}$ is valid, where $\phi_{i},\phi_{j}\vdash\emph{F}$ are valid for all $i\neq j\in I$, then $\mu\vdash\phi_{i_{0}}$ is valid for some $i_{0}\in I$. 2. (2)

A flat formula $\dot{\bigvee}_{i\in I}\mu_{i}$ is irreducible if each conjunction $\mu_{i}$ is irreducible.

For a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$, we denote by $\mathcal{IC}(P)$ the set of all irreducible conjunctions. Obviously, each irreducible conjunction is an irreducible flat formula.

Proposition 3.4

If $\mu$ is an irreducible conjunction in a disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$, then $\{\mu\}[\vdash]$ is a logical state.

$\mathbf{Proof.}$

Assume that $\dot{\bigvee}_{i\in I}\mu_{i}$ is a flat formula in $\{\mu\}[\vdash]$. Then $\mu\vdash\dot{\bigvee}_{i\in I}\mu_{i}$. Since $\mu$ is an irreducible conjunction, there exists some $i_{0}\in I$ such that $\mu\vdash\mu_{i_{0}}$. Therefore, $\mu_{i_{0}}\in\{\mu\}[\vdash]$.

Using the rule (Cut), it is trivial to check that the set $(\{\mu\}[\vdash])[\vdash]$ is a subset of $\{\mu\}[\vdash]$. $\square$

3.2 Representation of algebraic $L$-domains

In this subsection, we establish a satisfactory correspondence between disjunctive sequent calculi and algebraic $L$-domains. Before stating and proving our representation theorem, we require further lemmas which are of interest in their own right.

Lemma 3.1

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus. Then the family $|(\mathcal{L}(P),\vdash)|$ forms a point dcpo under the set inclusion.

$\mathbf{Proof.}$

It is easy to see that Tau$(P)$ is the least element of $(|(\mathcal{L}(P),\vdash)|,\subseteq)$.

Let $\{S_{i}\mid i\in I\}$ be a directed set of $(|(\mathcal{L}(P),\vdash)|,\subseteq)$. By part (2) of Proposition 3.3, the union $\bigcup\{S_{i}\mid i\in I\}$ is a logical state. Then the supremum of the set $\{S_{i}\mid i\in I\}$ exists in $(|(\mathcal{L}(P),\vdash)|,\subseteq)$, and

[TABLE]

As a result, $(|(\mathcal{L}(P),\vdash)|,\subseteq)$ forms a pointed dcpo. $\square$

Lemma 3.2

For any logical state $S$ and finite subset $\Gamma$ of $S$, the set $[\Gamma]_{S}$ defined by equation (3.2) is a compact element of the dcpo $(|(\mathcal{L}(P),\vdash)|,\subseteq)$.

$\mathbf{Proof.}$

Let $\{S_{i}\mid i\in I\}$ be a directed subset in the dcpo $(|(\mathcal{L}(P),\vdash)|,\subseteq)$ with $[\Gamma]_{S}\subseteq\bigcup\{S_{i}\mid i\in I\}$. Since $\bigcup\{S_{i}\mid i\in I\}$ is a logical state, it is evident that $[\Gamma]_{S}=[\Gamma]_{\bigcup\{S_{i}\mid i\in I\}}$. Because $\Gamma\sqsubseteq\bigcup\{S_{i}\mid i\in I\}$, there exists some $i_{0}\in I$ such that $\Gamma\subseteq S_{i_{0}}$. Whence, $[\Gamma]_{S}=[\Gamma]_{\bigcup\{S_{i}\mid i\in I\}}\subseteq S_{i_{0}}$, which implies that $[\Gamma]_{S}$ is a compact element of the dcpo $(|(\mathcal{L}(P),\vdash)|,\subseteq)$. $\square$

Lemma 3.3

If $S$ is a logical state, then the set $\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}$ is directed and $S$ is its union.

$\mathbf{Proof.}$

Let $\Gamma_{1},\Gamma_{2}\sqsubseteq S$. Then $[\Gamma_{1}\cup\Gamma_{2}]_{S}\in\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}$. Obviously, $[\Gamma_{1}]_{S},[\Gamma_{2}]_{S}\subseteq[\Gamma_{1}\cup\Gamma_{2}]_{S}$, which implies the set $\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}$ is directed.

We next show $S=\bigcup\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}$. It is clear that $\bigcup\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}\subseteq S$, since $[\Gamma]_{S}\subseteq S$ for any $\Gamma\sqsubseteq S$. Conversely, suppose that $\varphi\in S$. Then $\varphi\in[\{\varphi\}]_{S}\subseteq\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}$. This yields that $S\subseteq\bigcup\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}$. $\square$

Theorem 3.1

Let $(\mathcal{L}(P),\vdash)$ be a disjunctive sequent calculus. Then $(|(\mathcal{L}(P),\vdash)|,\subseteq)$ is an algebraic $L$-domain.

$\mathbf{Proof.}$

According to the above lemmas, it follows that $(|(\mathcal{L}(P),\vdash)|,\subseteq)$ forms an algebraic domain. To complete the proof, it suffices to show that for all logical state $S$, the principle ideal $\mathord{\downarrow}_{\subseteq}S$ is a complete lattice. For this, suppose that $\mathcal{T}$ is a subset of $\mathord{\downarrow}_{\subseteq}S$. Just as the proof of part (5) of Proposition 3.2, we can verify the intersection $\bigcap_{T\in\mathcal{T}}T$ is also a logical state. Clearly, $\bigcap_{T\in\mathcal{T}}T\in\mathord{\downarrow}_{\subseteq}S$, and therefore, $\bigcap_{T\in\mathcal{T}}T$ is an infimum of $\mathcal{T}$ in $\mathord{\downarrow}_{\subseteq}S$. $\square$

Theorem 3.1 tells us that each disjunctive sequent calculus associates an algebraic $L$-domain. We now consider the inverse direction.

Definition 3.6

Let $(D,\leq)$ be an algebraic L-domain. A subset $U$ of $D$ is said to be decomposable if it is a down set $\mathord{\uparrow}A$ with $A$ is a pairwise inconsistent subset of $K(D)$.

The notation $\mathcal{U}(D)$ will denote the collection of all decomposable subsets of $D$. It is obvious that every decomposable set is Scott open and $\mathcal{U}(D)$ is closed under finite intersections $\cap$ and arbitrary disjoint unions $\dot{\bigcup}$, since $(D,\leq)$ is an algebraic L-domains.

Thus we can make a concrete disjunctive sequent calculus as follows.

Theorem 3.2

Associated with a given algebraic $L$-domain $(D,\leq)$, a disjunctive sequent calculus $(\mathcal{L}(P_{D}),\vdash_{D})$ can be defined in the following three stages:

First, let

[TABLE]

be the set of atomic formulae, $\mathrm{F}$ the syntactic constant for“false” and

[TABLE]

the set of atomic disjointness assumptions.

Second, define the set $\mathcal{L}(P_{D})$ of formulae by induction:

1. (L1)

each atomic formula is an element of $\mathcal{L}(P_{D})$, and the constant connectives $\mathrm{T}$ and $\mathrm{F}$ are elements of $\mathcal{L}(P_{D})$, 2. (L2)

if $\varphi,\psi\in\mathcal{L}(P_{D})$, then $\varphi\wedge\psi\in\mathcal{L}(P_{D})$, 3. (L3)

if a subset $\{\varphi_{i}\mid i\in I\}$ of $\mathcal{L}(P_{D})$ satisfies $\widehat{\varphi_{i}}\cap\widehat{\varphi_{j}}=\emptyset$ for all $i\neq j\in I$, then $\dot{\bigvee}_{i\in I}\varphi_{i}\in\mathcal{L}(P_{D})$, where $\widehat{\varphi}$ is the set generated by replacing the connectives $\mathrm{F},\mathrm{T},\wedge$ and $\dot{\bigvee}$ in $\varphi$ by $\emptyset,D,\cup$ and $\dot{\bigcup}$, respectively.

Finally, define the relation $\vdash_{D}$ by

[TABLE]

where, $\Gamma=\{\psi_{1},\psi_{2},\cdots,\psi_{n}\}\subseteq\mathcal{L}(P_{D})$ and $\varphi\in\mathcal{L}(P_{D})$.

$\mathbf{Proof.}$

It is clear that $\widehat{p}=p$ for all $p\in P_{D}$, and $(\{p_{1},p_{2},\ldots,p_{n}\},\mathrm{F)\in\vdash_{D}}$ whenever $p_{1},p_{2},\ldots,p_{n}\vdash_{D}\mathrm{F}$ is an element of $\mathcal{A}$.

We first show that the class $\mathcal{L}(P_{D})$ of all formulae is closed under the rules of disjunctive formulae proposed in Definition 2.3. To this end, we claim that

[TABLE]

In fact, given a decomposable set $U\in\mathcal{U}(D)$, let

\overleftarrow{U}=\left\{\begin{array}[]{ll}\mathrm{T},\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if$~{}U=D;\\ \mathrm{F},\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \$if$~{}U=\emptyset;\\ \dot{\bigvee}_{a\in A}\mathord{\uparrow}a,\ \ \ \ \ \ \$if$~{}U=\dot{\bigcup}_{a\in A}\mathord{\uparrow}a${}for{}some~{}A\subseteq K^{*}(D).\end{array}\right.

Then by the construction of $\mathcal{L}(P_{D})$, the expression $\overleftarrow{U}$ defined above is a member of $\mathcal{L}(P_{D})$.

Assume that $\varphi\in\mathcal{L}(P_{D})$, then by Definition 3.6, it is clear that $\widehat{\varphi}\in\mathcal{U}(D)$, which means that $\{\widehat{\varphi}\mid\varphi\in\mathcal{L}(P_{D})\}\subseteq\mathcal{U}(D)$. For the converse inclusion, let $U\in\mathcal{U}(D)$. Then $\overleftarrow{U}\in\mathcal{L}(P_{D})$, and hence $\widehat{\overleftarrow{U}}\in\{\widehat{\varphi}\mid\varphi\in\mathcal{L}(P_{D})\}$. This shows that $\mathcal{U}(D)\subseteq\{\widehat{\varphi}\mid\varphi\in\mathcal{L}(P_{D})\}$.

Now we check the class $\mathcal{L}(P_{D})$ of formulae is closed under the rules of disjunctive formulae proposed in Definition 2.3.

From condition (L1) and (L2), it follows that $\mathcal{L}(P_{D})$ is closed under the rules (Const), (At) and (Conj). Since $D$ is an algebraic $L$-domain, the class $\mathcal{U}(D)$ is closed under disjoint union. This implies that $\mathcal{L}(P_{D})$ is closed under the rule (Disj).

Next, we have to check the rules of valid sequents. But all these rules can be shown routinely because of equation (3.3). We only illustrate this for the rule (Lwk):

Assume that $\Gamma\vdash\phi$ is a valid sequent, where $\Gamma=\{\psi_{1},\psi_{2},\cdots,\psi_{n}\}$. Then $\widehat{\psi_{1}}\cap\widehat{\psi_{2}}\cap\cdots\cap\widehat{\psi_{n}}\subseteq\widehat{\phi}$. Thus $\widehat{\psi_{1}}\cap\widehat{\psi_{2}}\cap\cdots\cap\widehat{\psi_{n}}\cap\widehat{\psi}\subseteq\widehat{\phi}$ for all formula $\psi$. This means that the sequent $\Gamma,\psi\vdash\phi$ is valid. $\square$

Proposition 3.5

For the disjunctive sequent calculus $(\mathcal{L}(P_{D}),\vdash_{D})$ associated with a given algebraic L-domain $(D,\leq)$, we have

1. (1)

a formula $\varphi$ is a tautology if and only if $\widehat{\varphi}=D$; 2. (2)

a formula $\varphi$ is a contradiction if and only if $\widehat{\varphi}=\emptyset$; 3. (3)

a formula $\varphi$ is a satisfiable formula if and only if $\widehat{\varphi}=\mathord{\uparrow}A$, where $A$ is a nonempty pairwise inconsistent subset of $K^{*}(D)$. 4. (4)

two formulae $\varphi$ and $\psi$ are logically equivalent if and only if $\widehat{\varphi}=\widehat{\psi}$: 5. (5)

for any finite subset $\{x_{1},x_{2},\cdots,x_{n}\}$ of $K^{*}(D)$, $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$ is a conjunction if and only if $\{x_{1},x_{2},\cdots,x_{n}\}$ has an upper bound in $D$.

$\mathbf{Proof.}$

Straightforward from Theorem 3.2. $\square$

For any nonempty proper subset $S$ of $\mathcal{L}(P_{D})$, let

[TABLE]

Then we have the following alternative characterization for a logical state of the disjunctive sequent calculi $(\mathcal{L}(P_{D}),\vdash_{D})$.

Proposition 3.6

Given an algebraic $L$-domain $(D,\leq)$, a subset $S$ of $\mathcal{L}(P_{D})$ is a logical state of $(\mathcal{L}(P_{D}),\vdash_{D})$ if and only if there exists some $d\in D$ such that $\widehat{S}=\{U\in\mathcal{U}(D)\mid d\in U\}$.

$\mathbf{Proof.}$

Let $S$ be a subset of $\mathcal{L}(P_{D})$ satisfying $\widehat{S}=\{U\in\mathcal{U}(D)\mid d\in U\}$ for some $d\in D$. We prove that $S$ is a logical state of $(\mathcal{L}(P_{D}),\vdash_{D})$ by showing $S$ satisfies conditions (S1) and (S2).

To prove condition (S1), assume that $\dot{\bigvee}_{i\in I}\mu_{i}$ is a flat formula in $S$. Since $d\in\dot{\bigcup}_{i\in I}\widehat{\mu_{i}}$, there exists some $i_{0}\in I$ such that $d\in\mu_{i_{0}}$. This implies that $\mu_{i_{0}}\in S$. For condition (S2), assume that $\psi\in S[\vdash_{D}]$. By Equation 3.1, there exists some finite subset $\Gamma=\{\varphi_{1},\varphi_{2},\cdots,\varphi_{n}\}$ of $S$ such that $\Gamma\vdash\psi$ is a valid sequent. If $\Gamma=\emptyset$, then $\psi\in$Tau$(P_{D})$, and thus $d\in\widehat{\psi}=D$. If $\Gamma\neq\emptyset$, then $d\in\widehat{\varphi_{1}}\cap\widehat{\varphi_{2}}\cap\cdots\cap\widehat{\varphi_{n}}\subseteq\widehat{\psi}$. This implies that $d\in\widehat{\psi}$ and hence $\psi\in S$. Condition (S2) follows.

For the converse implication, assume that $S$ is a logical state of $(\mathcal{L}(P_{D}),\vdash_{D})$. Then $\widehat{S}\subseteq\mathcal{U}(D)$. We are now ready to look for an element $d_{S}$ of $D$ such that $\widehat{S}=\{U\in\mathcal{U}(D)\mid d_{S}\in U\}$. This process is divided into three steps.

Step 1, for any $\psi\in S$, noting that $\widehat{\psi}\neq\emptyset$, there exists some pairwise inconsistent subset $A$ of $K(D)$ such that $\widehat{\psi}=\dot{\bigcup}_{a\in A}\mathord{\uparrow}a$. By condition (S2), we have $\mathord{\uparrow}a_{0}\in S$ for some $a_{0}\in A$. This implies that $\bigcap\widehat{S}=\bigcap\{\mathord{\uparrow}a\mid\mathord{\uparrow}a\in S\}$.

Step 2, we prove $\{a\mid\mathord{\uparrow}a\in S\}$ is a directed set of $D$. Let $a_{1},a_{2}\in\{a\mid\mathord{\uparrow}a\in S\}$. Since $\mathord{\uparrow}a_{1},\mathord{\uparrow}a_{2}\in S$, by part (1) of Proposition 3.2, $\mathord{\uparrow}a_{1}\cap\mathord{\uparrow}a_{2}\in\widehat{S}$. This implies $\mathord{\uparrow}a_{1}\cap\mathord{\uparrow}a_{2}\neq\emptyset$. Suppose $\mathord{\uparrow}a_{1}\cap\mathord{\uparrow}a_{2}=\bigcup_{b\in B}\mathord{\uparrow}b$, where $B$ is a nonempty set of pairwise incompatible elements of $K(D)$. By condition (S2), $\mathord{\uparrow}b\in S$ for some $b\in B$. Therefor, $b\in\{a\mid\mathord{\uparrow}a\in S\}$ and $a_{1},a_{2}\leq b$.

Step 3, put $d_{S}=\mathrm{sup}\{a\mid\mathord{\uparrow}a\in S\}$. Then $d_{S}\in D$ and $\bigcap\widehat{S}=\bigcap\{\mathord{\uparrow}a\mid\mathord{\uparrow}a\in S\}=\mathord{\uparrow}d_{S}$. Thus $d_{S}\in U$ for all $U\in\widehat{S}$. Therefore, $\widehat{S}\subseteq\{U\in\mathcal{U}(D)\mid d_{S}\in U\}$. Conversely, for any $U\in\mathcal{U}(D)$ with $d_{S}\in U$, there exists some $d\in K(D)$ such that $d_{S}\in\mathord{\uparrow}d\subseteq U$. Since $d_{S}=\mathrm{sup}\{a\mid\mathord{\uparrow}a\in S\}$ and $\{a\mid\mathord{\uparrow}a\in S\}$ is directed, $d\leq a_{0}$ for some $a_{0}\in\{a\mid\mathord{\uparrow}a\in S\}$. Let $\varphi\in\mathcal{L}(P_{D})$ such that $\widehat{\varphi}=U$. Then $\mathord{\uparrow}a_{0}\subseteq\widehat{\varphi}$, and hence $\mathord{\uparrow}a_{0}\vdash\varphi$ is a valid sequent. By condition (S1), we have $U\in\widehat{S}$. $\square$

With the above preparations, we obtain the representation theorem of algebraic $L$-domains.

Theorem 3.3

Each algebraic $L$-domain $(D,\leq)$ is isomorphic to $(|(\mathcal{L}(P_{D}),\vdash_{D})|,\subseteq)$.

$\mathbf{Proof.}$

Define a function as follows:

[TABLE]

[TABLE]

By Proposition 3.6, the set $\{\varphi\in\mathcal{L}(P_{D})\mid d\in\widehat{\varphi}\}$ is a logical state of $(\mathcal{L}(P_{D}),\vdash_{D})$, then the function $f$ is well-defined. For all logical state $S$ of $(\mathcal{L}(P_{D}),\vdash_{D})$, as we have known in the proof of Proposition 3.6, it is not difficult to see that $f(d_{S})=S$, where $d_{S}=\mathrm{sup}\{a\mid\mathord{\uparrow}a\in S\}$. This means that the function $f$ is surjective.

Moreover, it is easy to show that $d_{1}\leq d_{2}$ if and only if

[TABLE]

Therefore, the function $f$ is an order-isomorphism from $(D,\leq)$ to $(|(\mathcal{L}(P_{D}),\vdash_{D})|,\subseteq)$. $\square$

We now see that there are technical advantages to investigating disjunctive sequent calculi rather than its Lindenbaum algebra. First, logical states of a disjunctive sequent calculus use the language of set theory. Second, the features of algebraic $L$-domains can be obtained directly by logical inference. It further demonstrates its advantages by representing the category of algebraic $L$-domains with Scott-continuous functions as morphisms in the next section.

4 A Categorical view

From a categorical viewpoint, Section 3.2 has built an object part correspondence between algebraic $L$-domains and disjunctive sequent calculi. We now aim to look for appropriate morphisms so as to obtain an categorical equivalence.

4.1 Expressive disjunctive sequent calculi

In the rest of the article, a special class of disjunctive sequent calculi are considered as objects to construct a category equivalent to $\mathbf{ALD}$.

As we have always seen in Proposition 3.2, each algebraic $L$-domain $(D,\leq)$ associated with a disjunctive sequent calculus $(\mathcal{L}(P_{D}),\vdash_{D})$. In this case, a conjunction is of the form $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$, where $\{x_{1},x_{2},\cdots,x_{n}\}\subseteq K^{*}(D)$ and $\{x_{1},x_{2},\cdots,x_{n}\}$ has an upper bound in $D$.

The following result gives a sufficient and necessary condition for a conjunction being irreducible in $(\mathcal{L}(P_{D}),\vdash_{D})$.

Proposition 4.1

Let $(D,\leq)$ be an algebraic $L$-domain and $\{x_{1},x_{2},\cdots,x_{n}\}$ a nonempty subset of $K^{*}(D)$. Then a conjunction $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$ in $(\mathcal{L}(P_{D}),\vdash_{D})$ is irreducible if and only if $\mathrm{sup}\{x_{1},x_{2},\cdots,x_{n}\}\in D$.

$\mathbf{Proof.}$

For any conjunction $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$, we have seen that the set $\{x_{1},x_{2},\cdots,x_{n}\}$ has an upper bound in $D$. Since $D$ is an algebraic $L$-domain, there is a nonempty pairwise inconsistent subset $A$ of $K^{*}(D)$ such that $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$ is logically equivalent to $\dot{\bigvee}_{a\in A}\mathord{\uparrow}a$ in $(\mathcal{L}(P_{D}),\vdash_{D})$. In this case, the set $A$ just is the minimal upper bounds of $\{x_{1},x_{2},\cdots,x_{n}\}$.

Assume that $\mathrm{sup}\{x_{1},x_{2},\cdots,x_{n}\}\in D$, then $A$ must be a singleton, say $\{d\}$. The elements $x_{1},x_{2},\cdots,x_{n}$ are compact in $D$ and so is $d$. This implies that $\mathord{\uparrow}d$ is a formula in $(\mathcal{L}(P_{D}),\vdash_{D})$, and thus, $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$ is logically equivalent to $\mathord{\uparrow}d$ in $(\mathcal{L}(P_{D}),\vdash_{D})$. Let $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}\vdash\dot{\bigvee}_{i\in I}\phi_{i}$ be a valid sequent, where $\widehat{\phi_{i}}\cap\widehat{\phi_{j}}=\emptyset$ for all $i\neq j\in I$. Then $\mathord{\uparrow}d\subseteq\dot{\bigcup}_{i\in I}\widehat{\phi_{i}}$, and hence there exists some $i_{0}\in I$ such that $\mathord{\uparrow}d\subseteq\widehat{\phi_{i_{0}}}$. Therefore, $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}\vdash\phi_{i_{0}}$ is valid. So $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$ is an irreducible conjunction, as required.

Conversely, if $\mathrm{sup}\{x_{1},x_{2},\cdots,x_{n}\}$ does not exists in $K^{*}(D)$, then there are at least two elements in $A$. Therefore, $\bigcup_{a\in A}\mathord{\uparrow}a$ is not a subset of $\mathord{\uparrow}a$ for all $a\in A$. Thus $\dot{\bigvee}_{a\in A}\mathord{\uparrow}a\vdash\mathord{\uparrow}a$ is not a valid sequent. But $\dot{\bigvee}_{a\in A}\mathord{\uparrow}a\vdash\dot{\bigvee}_{a\in A}\mathord{\uparrow}a$ is valid. Hence $\mathord{\uparrow}x_{1}\wedge\mathord{\uparrow}x_{2}\wedge\cdots\wedge\mathord{\uparrow}x_{n}$ is not an irreducible conjunction. $\square$.

Definition 4.1

A disjunctive sequent calculus $(\mathcal{L}(P),\vdash)$ is said to be expressive if, for any satisfiable formula $\psi$, there exists an irreducible flat formula $\dot{\bigvee}_{i\in I}\mu_{i}$ such that $\psi\vdash\dot{\bigvee}_{i\in I}\mu_{i}$ is valid and $\mu_{i}\vdash\psi$ are valid for all $i\in I$.

Proposition 4.2

For any algebraic $L$-domain $(D,\leq)$, the associated disjunctive sequent calculus $(\mathcal{L}(P_{D}),\vdash_{D})$ is expressive.

$\mathbf{Proof.}$

Let $(\mathcal{L}(P_{D}),\vdash_{D})$ be the disjunctive sequent calculus associated with an algebraic $L$-domian $(D,\leq)$. Proposition 4.1 reveals that every atomic formula of $(\mathcal{L}(P_{D}),\vdash_{D})$ is an irreducible conjunction. For any satisfiable formula $\psi$ of $(\mathcal{L}(P_{D}),\vdash_{D})$, the set $\widehat{\psi}$ has a form $\mathord{\uparrow}A$, where $A$ is a nonempty pairwise inconsistent subset of $K^{*}(D)$. Then $\dot{\bigvee}_{a\in A}\mathord{\uparrow}a$ is a flat formula such that $\psi\vdash\dot{\bigvee}_{a\in A}\mathord{\uparrow}a$ and $\mathord{\uparrow}a\vdash\psi$ are valid for all $a\in A$. $\square$

With respect to an expressive disjunctive sequent calculus  $(\mathcal{L}(P),\vdash)$, a logical state has another alternative characterization.

Theorem 4.4

Let $(\mathcal{L}(P),\vdash)$ be an expressive disjunctive sequent calculus and $S$ a nonempty proper subset of $\mathcal{L}(P)$. Then $S$ is a logical state if and only if the set $\{\{\mu\}[\vdash]\mid\mu\in S\cap\mathcal{IC}(P)\}$ is directed and $S$ is its union.

$\mathbf{Proof.}$

Assume that the set $\{\{\mu\}[\vdash]\mid\mu\in S\cap\mathcal{IC}(P)\}$ is directed and $S$ is its union. We may appeal to part (2) of Proposition 3.3 and Proposition 3.4 to deduce that $S$ is a logical state. So that the only interesting thing is the “only if ” part of the proof.

Let $S$ be a logical state. We first claim that for any $\Gamma\sqsubseteq S$ there exists some $\mu\in S\cap\mathcal{IC}(P)$ such that $[\Gamma]_{S}\subseteq\{\mu\}[\vdash]$. Indeed, if $\Gamma=\emptyset$, then $[\Gamma]_{S}\subseteq\{\mu\}[\vdash]$ for any $\mu\in S\cap\mathcal{IC}(P)$. If $\Gamma\neq\emptyset$, then $\Gamma\sqsubseteq S$ implies that $\bigwedge\Gamma\in S$. Since $(\mathcal{L}(P),\vdash)$ is an expressive disjunctive sequent calculus, there exists some irreducible flat formula $\dot{\bigvee}_{i\in I}\mu_{i}$ such that $\bigwedge\Gamma\vdash\dot{\bigvee}_{i\in I}\mu_{i}$ and $\mu_{i}\vdash\bigwedge\Gamma$ are valid for all $i\neq j\in I$. Then $\dot{\bigvee}_{i\in I}\mu_{i}\in S$, and hence $\mu_{i_{0}}\in S$ for some $i_{0}\in I$. From $\mu_{i_{0}}\vdash\bigwedge\Gamma$ it follows that $\Gamma\subseteq\{\mu_{i_{0}}\}[\vdash]$, which implies that $[\Gamma]_{S}\subseteq\{\mu\}[\vdash]$.

We next claim that for any $\mu\in S\cap\mathcal{IC}(P)$ there exists some $\Gamma\subseteq S$ such that $\{\mu\}[\vdash]\subseteq[\Gamma]_{S}$. Indeed, taking $\Gamma=\{\mu\}$, since $[\Gamma]_{S}$ is a logical state, $\{\mu\}[\vdash]\subseteq[\Gamma]_{S}$, by condition (S1).

Finally, as we have seen from the proof of Theorem 3.1, the set $\{[\Gamma]_{S}\mid\Gamma\sqsubseteq S\}$ is directed and $S$ is its union. Then the set $\{\{\mu\}[\vdash]\mid\mu\in S\cap\mathcal{IC}(P)\}$ is directed and $S$ is its union. $\square$

4.2 Morphisms between expressive disjunctive sequent calculi

A main contribution of this subsection is the introduction of a notion of consequence relation between expressive disjunctive sequent calculi, which can be used to represent Scott-continuous functions between algebraic $L$-domains.

Definition 4.2

Let $(\mathcal{L}(P),\vdash_{P})$ and $(\mathcal{L}(P),\vdash_{Q})$ be two expressive disjunctive sequent calculi. A binary relation $\Theta\subseteq\mathcal{IC}(P)\times\mathcal{L}({Q})$ is called a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(P),\vdash_{Q})$ if, for all $\mu\in\mathcal{IC}(P)$ and $\psi\in\mathcal{L}({Q})$, the following conditions hold:

1. (R1)

whenever there is some $(\nu,\psi)\in\Theta$ such that $\mu\vdash_{P}\nu$ is a valid sequent, then $(\mu,\psi)\in\Theta$; 2. (R2)

whenever there is some $(\mu,\varphi)\in\Theta$ such that $\varphi\vdash_{Q}\psi$ is a valid sequent, then $(\mu,\psi)\in\Theta$; 3. (R3)

whenever $(\mu,\psi)\in\Theta$, then $(\mu,\nu)\in\Theta$ and the sequent $\nu\vdash_{Q}\psi$ is valid for some $\nu\in\mathcal{IC}({Q})$.

We use $\Theta:(\mathcal{L}(P),\vdash_{P})\rightarrow(\mathcal{L}(P),\vdash_{P})$ to denote the consequence relation $\Theta$ from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(P),\vdash_{Q})$ defined above.

Proposition 4.3

Let $\Theta:(\mathcal{L}(P),\vdash_{P})\rightarrow(\mathcal{L}(P),\vdash_{P})$ be a consequence relation. Then the following conditions are equivalent.

1. (1)

$(\mu,\psi)\in\Theta$. 2. (2)

There exists some $\nu\in\mathcal{IC}({P})$ such that $\mu\vdash_{P}\nu$ is valid and $(\nu,\psi)\in\Theta$. 3. (3)

There exists some $\varphi\in\mathcal{L}({Q})$ such that $\varphi\vdash_{Q}\psi$ is valid and $(\mu,\varphi)\in\Theta$. 4. (4)

There exists $\nu\in\mathcal{IC}({Q})$ such that $\nu\vdash_{Q}\psi$ is valid and $(\mu,\nu)\in\Theta$.

$\mathbf{Proof.}$

Straightforward from Definition 4.2. $\square$

For all consequence relation $\Theta$ from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(P),\vdash_{P})$ and all subset $X$ of $\mathcal{L}({P})$, set

[TABLE]

Then it is clear that $\Theta[X_{1}]\subseteq\Theta[X_{2}]$ for any $X_{1}\subseteq X_{2}\subseteq\mathcal{L}({P})$.

The following proposition shows that a consequence relation provides a passage from logical states of an expressive disjunctive sequent calculus to those of another one.

Proposition 4.4

Let $\Theta$ be a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(P),\vdash_{P})$.

1. (1)

If $S$ is a logical state of $(\mathcal{L}(P),\vdash_{P})$, then $\Theta[S]$ is a logical state of $(\mathcal{L}(Q),\vdash_{Q})$. 2. (2)

If $\mu\in\mathcal{IC}({P})$, then $\Theta[\{\mu\}]=\Theta[\{\mu\}[\vdash_{P}]]$.

$\mathbf{Proof.}$

(1) Let $\dot{\bigvee}_{i\in I}\mu_{i}\in\Theta[S]\cap\mathcal{N}({P})$. Then there exists $\mu\in S\cap\mathcal{IC}({P})$ such that $(\mu,\dot{\bigvee}_{i\in I}\mu_{i})\in\Theta$. By condition (R3), there exists some $\nu\in\mathcal{IC}({Q})$ such that $(\mu,\nu)\in\Theta$ and $\nu\vdash_{Q}\dot{\bigvee}_{i\in I}\mu_{i}$ is valid. Since $\nu$ is an irreducible conjunction, $\nu\vdash_{Q}\mu_{i_{0}}$ is valid for some $i_{0}\in I$. Using condition (R2) again, $(\mu,\mu_{i_{0}})\in\Theta$, and thus $\mu_{i_{0}}\in\Theta[S]$.

Assume that $\varphi\in(\Theta[S])[\vdash_{Q}]$. Then there exist $\mu\in S\cap\mathcal{IC}({P})$ and $\psi\in\mathcal{L}({Q})$ such that $(\mu,\psi)\in\Theta$ and $\psi\vdash_{Q}\varphi$ is valid. By condition (R2), we have $(\mu,\varphi)\in\Theta$. This implies that $\varphi\in\Theta[S]$ and hence $(\Theta[S])[\vdash_{Q}]\subseteq\Theta[S]$.

(2) It is clear $\Theta[\{\mu\}]\subseteq\Theta[\{\mu\}[\vdash_{P}]]$. Conversely, let $\varphi\in\Theta[\{\mu\}[\vdash_{P}]]$. Then there exists some $\nu\in\{\mu\}[\vdash_{P}]\cap\mathcal{IC}({P})$ such that $(\nu,\varphi)\in\Theta$. But $\nu\in\{\mu\}[\vdash_{P}]$ implies that $\mu\vdash_{P}\nu$ is valid. By condition (R1), we have $(\mu,\varphi)\in\Theta$, and thus $\varphi\in\Theta[\{\mu\}]$. $\square$

Now we consider the relationship between consequence relations and Scott-continuous functions.

Theorem 4.5

Let $(\mathcal{L}(P),\vdash_{P})$ and $(\mathcal{L}(Q),\vdash_{Q})$ be expressive disjunctive sequent calculi. For all consequence relation $\Theta:(\mathcal{L}(P),\vdash_{P})\rightarrow(\mathcal{L}(Q),\vdash_{Q})$, define a function $f_{\Theta}:|(\mathcal{L}(P),\vdash_{P})|\rightarrow|(\mathcal{L}(Q),\vdash_{Q})|$ by

[TABLE]

Then $f_{\Theta}$ is Scott-continuous.

Conversely, for all Scott-continuous function $f:|(\mathcal{L}(P),\vdash_{P})|\rightarrow|(\mathcal{L}(Q),\vdash_{Q})|$, define $\Theta_{f}\subseteq\mathcal{C}_{0}({P})\times\mathcal{L}({Q})$ by

[TABLE]

Then $\Theta_{f}$ is a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(Q),\vdash_{Q})$. Moreover, $\Theta_{f_{\Theta}}=\Theta$ and $f_{\Theta_{f}}=f$.

$\mathbf{Proof.}$

We divided the proof into three claims.

Claim 1: The function $f_{\Theta}$ is Scott-continuous.

By part (2) of Proposition 4.4, the function $f_{\Theta}$ is well-defined. Let $\{S_{i}\mid i\in I\}$ be a directed subset of logical states. Then $\bigcup_{i\in I}S_{i}$ is a logical state. From Equation 3.1 it follows that the function $f_{\Theta}$ is monotone, and hence $\bigcup_{i\in I}f_{\Theta}(S_{i})\subseteq f_{\Theta}(\bigcup_{i\in I}S_{i})$. To prove the function $f_{\Theta}$ is Scott-continuous, it suffices to show that $f_{\Theta}(\bigcup_{i\in I}S_{i})\subseteq\bigcup_{i\in I}f_{\Theta}(S_{i})$. If $\varphi\in f_{\Theta}(\bigcup_{i\in I}S_{i})=\Theta[\bigcup_{i\in I}S_{i}]$, then there exists some $\mu\in\bigcup_{i\in I}S_{i}\cap\mathcal{IC}(P)$ such that $(\mu,\varphi)\in\Theta$. From $\mu\in\bigcup_{i\in I}S_{i}$, it follows that $\mu\in S_{i_{0}}$ for some $i_{0}\in I$. Thus $\varphi\in f_{\Theta}(S_{i_{0}})$, and therefore, $f_{\Theta}(\bigcup_{i\in I}S_{i})\subseteq\bigcup_{i\in I}f_{\Theta}(S_{i})$.

Claim 2. $\Theta_{f}$ is a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(Q),\vdash_{Q})$.

It suffices to show that $\Theta_{f}$ satisfies conditions (R1–R3).

For condition (R1), assume that $\nu\in\mathcal{IC}(P)$ such that $\mu\vdash_{P}\nu$ is valid and $(\nu,\psi)\in\Theta_{f}$. Then $\psi\in f(\{\nu\}[\vdash_{P}])$. From $\mu\vdash_{P}\nu$ it follows that $\{\nu\}[\vdash_{P}]\subseteq\{\mu\}[\vdash_{P}]$. Since $f$ is monotone, $\psi\in f(\{\mu\}[\vdash_{P}])$. This means that $(\mu,\psi)\in\Theta_{f}$.

For condition (R2), assume that $(\mu,\varphi)\in\Theta_{f}$ and $\varphi\vdash_{Q}\psi$ is valid. Then $\varphi\in f(\{\mu\}[\vdash_{P}])$. Since $f(\{\mu\}[\vdash_{P}])$ is a logical state and $\varphi\vdash_{Q}\psi$ is valid, $\psi\in f(\{\mu\}[\vdash_{P}])$. That is $(\mu,\psi)\in\Theta_{f}$.

For condition (R3), assume that $(\mu,\psi)\in\Theta_{f}$. Then $\psi\in f(\{\mu\}[\vdash_{P}])$. Since the disjunctive sequent calculus $(\mathcal{L}(Q),\vdash_{Q})$ is expressive, there exists an irreducible flat formula $\dot{\bigvee}_{i\in I}\mu_{i}$ such that $\psi\vdash\dot{\bigvee}_{i\in I}\mu_{i}$ and $\mu_{i}\vdash\psi$ are all valid for all $i\in I$. Note that $f(\{\mu\}[\vdash_{P}])$ is a logical state, it follows that $\dot{\bigvee}_{i\in I}\mu_{i}\in f(\{\mu\}[\vdash_{P}])$. Thus $\mu_{i_{0}}\in f(\{\mu\}[\vdash_{P}])$ for some $i_{0}\in I$. Let $\mu_{i_{0}}=\nu$. Then we obtain some $\nu\in\mathcal{IC}(Q)$ such that $(\mu,\nu)\in\Theta$ and $\nu\vdash_{Q}\psi$ is valid.

Claim 3. $\Theta_{f_{\Theta}}=\Theta$ and $f_{\Theta_{f}}=f$.

For any $\mu\in\mathcal{IC}(P)$ and $\varphi\in\mathcal{L}(Q)$, we have

[TABLE]

This proves that $\Theta_{f_{\Theta}}=\Theta$.

For any $S\in|(\mathcal{L}(P),\vdash_{P})|$, we have

[TABLE]

This proves that $f_{\Theta_{f}}=f$. $\square$

Similar to the result presented in Theorem 4.5, there is also a one-to-one correspondence between Scott-continuous functions from algebraic $L$-domain $(D_{1},\leq_{1})$ to algebraic $L$-domain $(D_{2},\leq_{2})$ and consequence relations from $(\mathcal{L}(P_{D_{1}}),\vdash_{D_{1}})$ to $(\mathcal{L}(P_{D_{2}}),\vdash_{D_{2}})$. But familiarity with this is not essential for our investigation that follows, so we omit the proof and only state the result.

Theorem 4.6

Let $(D_{1},\leq_{1})$ and $(D_{2},\leq_{2})$ be algebraic $L$-domains. For all Scott-continuous function $h:D_{1}\rightarrow D_{2}$, define $\Omega_{h}\subseteq\mathcal{IC}(P_{D_{1}})\times\mathcal{L}(P_{D_{2}})$ by

[TABLE]

Then $\Omega_{h}$ is a consequence relation from $(\mathcal{L}(P_{D_{1}}),\vdash_{D_{1}})$ to $(\mathcal{L}(P_{D_{2}}),\vdash_{D_{2}})$.

Conversely, for any consequence relation $\Omega:(\mathcal{L}(P_{D_{1}}),\vdash_{D_{1}})\rightarrow(\mathcal{L}(P_{D_{2}}),\vdash_{D_{2}})$, define an assignment $h_{\Omega}$ by

[TABLE]

Then $h_{\Omega}$ is a Scott-continuous function from $D_{1}$ to $D_{2}$. Moreover, $\Omega_{h_{\Omega}}=\Omega$ and $h_{\Omega_{h}}=h$.

4.3 Categorical equivalence

It remains to consider the category of expressive disjunctive sequent calculi. What we want to do is to show this category is equivalent to the category $\mathbf{ALD}$ of algebraic $L$-domain with Scott continuous functions as morphisms.

Proposition 4.5

Expressive disjunctive sequent calculi with consequence relations form a category $\mathbf{EDSC}$.

$\mathbf{Proof.}$

Let $\Theta$ be a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(Q),\vdash_{Q})$, and $\Theta^{\prime}$ a consequence relation from $(\mathcal{L}(Q),\vdash_{Q})$ to $(\mathcal{L}(R),\vdash_{R})$. Define $\Theta^{\prime}\circ\Theta\subseteq\mathcal{IC}(P)\times\mathcal{L}(R)$ by

[TABLE]

and id${}_{P}\subseteq\mathcal{IC}(P)\times\mathcal{L}(P)$ by

[TABLE]

Then routine checks verify that $\Theta^{\prime}\circ\Theta$ is a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(R),\vdash_{R})$ and $\text{id}_{P}$ is a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to itself.

Using the same argument as checking the associative law of a traditional relation composition, we can carry out the composition $\circ$ defined by Equation 4.6 is associative. Conditions (R1) and (R2) yield that $\text{id}_{P}$ is the identity morphism of $(\mathcal{L}(P),\vdash_{P})$. So $\mathbf{EDSC}$ is a category, as required. $\square$

We use the following well known fact to establish a categorical equivalence.

Lemma 4.1

([28])

Let $\mathbf{C}$ and $\mathbf{D}$ be two categories. Then $\mathbf{C}$ and $\mathbf{D}$ are categorically equivalent if and only if there exists a functor $\mathcal{G}:\mathbf{C}\rightarrow\mathbf{D}$ such that $\mathcal{G}$ is full, faithful and essentially surjective on objects, that is for every object $D$ of $\mathbf{D}$, there exists some object $C$ of $\mathbf{C}$ such that $\mathfrak{F}(C)\cong D$.

Proposition 4.6

$\mathcal{G}:\mathbf{EDSC}\rightarrow\mathbf{ALD}$* is a functor which maps every expressive disjunctive sequent calculi $(\mathcal{L}(P),\vdash_{P})$ to $(|(\mathcal{L}(P),\vdash_{P})|,\subseteq)$ and consequence relation $\Theta:(\mathcal{L}(P),\vdash_{P})\rightarrow(\mathcal{L}(Q),\vdash_{Q})$ to $f_{\Theta}$, where $f_{\Theta}$ is defined by equation (4.2).*

$\mathbf{Proof.}$

By Theorems 3.1 and 4.5, $\mathcal{G}$ is well-defined. For all $S\in|(\mathcal{L}(P),\vdash_{P})|$, we have

[TABLE]

This implies that $\mathcal{G}$ preserves the identity morphism.

Let $\Theta:(\mathcal{L}(P),\vdash_{P})\rightarrow(\mathcal{L}(Q),\vdash_{Q})$ and $\Theta^{\prime}:(\mathcal{L}(Q),\vdash_{Q})\rightarrow(\mathcal{L}(R),\vdash_{R})$ be consequence relations. For all $S\in|(\mathcal{L}(P),\vdash)|$, we have

[TABLE]

This implies that $\mathcal{G}(\Theta^{\prime}\circ\Theta)=\mathcal{G}(\Theta^{\prime})\circ\mathcal{G}(\Theta)$, and then $\mathcal{G}$ preserves the composition. $\square$

Theorem 4.7

$\mathbf{EDSC}$* and $\mathbf{ALD}$ are categorically equivalent.*

$\mathbf{Proof.}$

According to Theorem 3.3 and Lemma 4.1, it suffices to show that the functor $\mathcal{G}$ defined in Proposition 4.6 is full and faithful.

For any Scott-continuous function $f:|(\mathcal{L}(P),\vdash_{P})|\rightarrow|(\mathcal{L}(Q),\vdash_{Q})|$, by Theorem 4.5, the relation $\Theta_{f}$ defined by equation (4.3) is a consequence relation from $(\mathcal{L}(P),\vdash_{P})$ to $(\mathcal{L}(Q),\vdash_{Q})$ and $\mathcal{G}(\Theta_{f})=f_{\Theta_{f}}=f$. This implies that $\mathcal{G}$ is full.

Let $\Theta_{1},\Theta_{2}:(\mathcal{L}(P),\vdash_{P})\rightarrow(\mathcal{L}(Q),\vdash_{Q})$ be two consequence relations with $f_{\Theta_{1}}=f_{\Theta_{2}}$, where $f_{\Theta_{1}}$ and $f_{\Theta_{2}}$ are defined by equation (4.2). For any $\mu\in\mathcal{IC}(P)$, since

[TABLE]

it follows that $\Theta_{1}=\Theta_{2}$, and hence $\mathcal{G}$ is faithful. $\square$

Combining Theorem 4.7 with the fact that $\mathbf{ALD}$ is a cartesian closed category, we have the following result:

Corollary 4.1

$\mathbf{EDSC}$* is a cartesian closed category.*

5 Funding

This study was funded by the National Natural Science Foundation of China(11771134).