Heyting 代数

此页面尚不符合香蕉空间的百科写作风格, 并需要改进. 请编辑者参照已有的与之内容相近的条目, 以及香蕉空间:写作指引的要求, 对此页面进行修改. 具体问题如下:

• 术语使用不符合香蕉空间: 术语规范.

Heyting 代数是一类特殊的格结构, 它是直觉主义逻辑的代数语义模型, 与经典逻辑中的 Boole 代数形成对比. 在拓扑学、范畴论 (如拓扑斯理论) 和程序语义学中有重要应用. 一般而言, 形式逻辑中的命题可视为在逻辑运算符 (如 “且” 与 “或”) 下构成某种代数结构. 在此对应下, 不同的逻辑系统对应于不同的运算符集合与公理体系.

对于直觉主义命题演算, 其运算符 (包括零元运算符, 即常量) 包含 “且”、“或”、“真”、“假” 及 “蕴涵”. Heyting 代数的概念精确地囊括了这些运算符及其公理, 因此 Heyting 代数即构成直觉主义命题演算的模型.

若 Heyting 代数中满足排中律, 则该代数退化为 Boole 代数, 即经典命题演算的模型.

为对量词与变量建模 (即从命题逻辑扩展到一阶逻辑或谓词逻辑) , 需在 Heyting 代数上构造一种称为一阶超验理论的结构.

1定义

定义 1.1 (Heyting 代数). 设 $(H,\vee ,\wedge ,0,1)$ 是一个有界分配格, 若对任意 $a,b\in H$, 存在唯一元素 $a\to b\in H$ 满足: $$c\le a\to b\text{当且仅当}c\wedge a\le b(\forall c\in H)$$则称 $H$ 为 Heyting 代数, 其中运算 $\to$ 称为伪补运算 (或直觉主义蕴涵) .

2性质与证明

定理 2.1. 对任意 $a,b\in H$, 以下等式成立:

1.	$a\to a=1$
2.	$a\wedge (a\to b)=a\wedge b$
3.	$a\to (b\wedge c)=(a\to b)\wedge (a\to c)$

证明. (以性质 2 为例): 由定义, $a\wedge (a\to b)\le b$. 另一方面, 因 $b\le a\to b$ 当且仅当 $a\wedge b\le b$ (显然成立) , 故 $a\wedge b\le a\to b$. 结合 $a\wedge b\le a$ 得 $a\wedge b\le a\wedge (a\to b)$.

$\square$

与 Boole 代数的关系

定理 2.2. Boole 代数是 Heyting 代数, 其中伪补运算满足 $a\to b=\neg a\vee b$, 且所有元素满足双重否定律 $\neg \neg a=a$.

例子

例 2.3. 拓扑空间设 $X$ 为拓扑空间, 其所有开集构成的格 $(\mathcal{O}(X),\cap ,\cup ,\varnothing ,X)$ 构成 Heyting 代数, 其中伪补运算定义为: $$U\to V=\mathrm{int}((X\setminus U)\cup V)$$

例 2.4 (有限 Heyting 代数). 任何有限分配格都是 Heyting 代数, 例如线序集 $\{0,a,1\}$ 满足 $0<a<1$, 其伪补运算如下: $$\begin{array}{cccc}\to & 0& a& 1\\ 0& 1& 1& 1\\ a& 0& 1& 1\\ 1& 0& a& 1\end{array}$$

3参考文献

•	Arend Heyting (1930). “Die formalen Regeln der intuitionistischen Logik”. Sitzungsberichte der Preussischen Akademie der Wissenschaften, 42–56.

•	Garrett Birkhoff (1967). Lattice Theory, 3rded. American Mathematical Society.

•	Peter Johnstone (1986). Stone Spaces. Cambridge Studies in Advanced Mathematics 3. Cambridge University Press.

•	Francis Borceux (1994). Handbook of Categorical Algebra, Vol. 3. Encyclopedia of Mathematics and its Applications 52. Cambridge University Press.

4相关概念

术语翻译

Heyting 代数 • 英文 Heyting algebra • 德文 Heyting Algebra • 法文 algèbre de Heyting • 古希腊文 Άλγεβρα Heyting