斯科特信息系统

在数学和计算机科学分支域理论中，Scott 信息系统是经常用做表示斯科特域的替代方式的一种原始种类的逻辑演绎系统。

定义

Scott 信息系统 A 是有序三元组 $(T, Con, \vdash)$

• $T \,$ 是记号(信息的基本单位)的集合。
• $Con \subseteq \mathcal{P}_f(T)$ 是 T 的有限子集。
• $\vdash \subseteq Con\times T$。

满足

1. 如果 $a \in X \in Con$ 则 $X \vdash a$，
2. 如果 $X \vdash Y$ 并且 $Y \vdash a$ 则 $X \vdash a$，
3. 如果 $X \vdash a$ 则 $X \cup a \in Con$，
4. $\forall a \in T : \{ a\} \in Con$，
5. 如果 $X \in Con$ 并且 $X^\prime\, \subseteq X$ 则 $X^\prime \in Con$。

这里的 $X \vdash Y$ 意味着 $\forall a \in Y, X \vdash a$。

例子

命题演算

命题演算给我们一个非常简单的 Scott 信息系统如下:

• $T := \{ \phi \mid \phi$是可满足的$\} \,$
• $Con := \{ X \in \mathcal{P}_f(T) \mid X$是相容的 $\} \,$
• $X \vdash a$ 当且仅当在命题演算中 $X \vdash a$

Scott 域

设 D 是 斯科特域。接着我们定义信息系统如下

• $T := D^0 \,$ 是 D 的紧致元素的集合
• $Con := \{ X \in \mathcal{P}_f(T) \mid X$有上界$\} \,$
• $X \vdash d$ 当且仅当 $d \sqsubseteq \bigsqcup X$

设 $\mathcal{I}$ 是从 Scott 域 D 到上面定义的信息系统的映射。

信息系统和 Scott 领域

给定一个信息系统 $A = (T, Con, \vdash)$，我们可以建造斯科特域如下。

• 定义: $x \subseteq T$ 是一个点当且仅当
  • 如果 $X \subseteq_f x$ 则 $X \in Con$
  • 如果 $X \vdash a$ 并且 $X \subseteq_f x$ 则 $a \in x$

设 $\mathcal{D}(A)$ 指示 A 的点的集合并按子集排序。在 T 是可数的时候，$\mathcal{D}(A)$ 将是可数 Scott 域。一般的说，对于任何 Scott 域 D 和信息系统 A

• $\mathcal{D}(\mathcal{I}(D)) \cong D$
• $\mathcal{I}(\mathcal{D}(A)) \cong A$

这里的第二个全等给出自逼近映射。

参见

• 斯科特域
• 域理论