在数学中，Heyting代数是构成对布尔代数的推广的特殊的偏序集。Heyting代数为直觉逻辑而提出，它是在其中排中律一般不成立的逻辑。完全Heyting代数是无点拓扑学研究的中心对象。

海廷代数

滤子

形式定义

性质

例子

海廷代数

在数学中，Heyting 代数是构成对布尔代数的推广的特殊的偏序集。Heyting 代数为直觉逻辑而提出，它是在其中排中律一般不成立的逻辑。完全Heyting代数是无点拓扑学研究的中心对象。

滤子

Heyting代数是作为直觉主义命题逻辑的代数模型而引进的，使得逻辑排中律一般不再成立，Heyting代数可以被看作是Lindenbaum代数的推广。从逻辑的角度讲，Heyting代数是通常的二值逻辑系统的一种基本的推广，通常的二值逻辑系统是Heyting代数的一个最简单的例子，这种代数只有两个元素：“真”和“假”。在数学方面，Heyting代数是一个Boole代数一般化的偏序集，完备Heyting代数（即Frame）是研究无点化拓扑的中心主体。 下面介绍本文的结构和主要内容： 第一章 研究了Heyting代数中的各种滤子。首先回顾了Heyting代数的定义和有关性质，以及它与Boole代数的关系；其次，研究了Heyting代数中滤子的性质，给出了Heyting代数的滤子格的具体结构以及由子集生成的滤子的结构；最后定义了Heyting代数的一些特殊滤子，如极大滤子，次极大滤子，强滤子，素滤子等。对它们之间能够成立的蕴含关系给出了证明，对于不成立的蕴涵关系分别给出了反例予以说明。此外特别研究了次极大滤子的性质，以次极大滤子为桥梁证明了Heyting代数的滤子格是素元生成的Frame,即空间式Frame。 第二章 研究了由滤子生成的同余关系，以及Heyting代数同态和同构定理。首先，在Heyting代数中定义了关于滤子的一个等价关系，并证明它是同余关系，以及Heyting代数关于这个同余关系的商仍然是Heyting代数，并证明Heyting代数的滤子与Heyting代数上的同余关系一一对应。其次，给出了Heyting代数同态和子Heyting代数的定义，并指出滤子是子Heyting代数，研究了各种滤子在同态映射下的保持和逆保持的问题。第三，仿照代数学中的做法，将子Heyting代数视为子群，滤子视为不变子群，同态视为群同态，三大同构定理在Heyting代数中的相应结论得以顺利证明。最后，定义了Heyting代数可解Heyting代数，证明了Heyting代数中元素的唯一分解定理，并通过构造指出阶为合数的集合上一定存在一个格结构使之成为可解Heyting代数。 第三章 研究了Heyting代数中的模糊滤子。首先，定义了Heyting代数的模糊滤子，证明了模糊滤子等价于保有限交的模糊集，并从截集、强截集的方面考察了模糊滤子的性质，得到了模糊滤子的另外两个等价刻画；其次，通过对模糊滤子的观察，给出了关于模糊滤子的同余关系以及商代数；最后，研究了一些特殊的。

形式定义

Heyting 代数 H 是满足如下条件的有界格，对于在 H 中的所有 a 和 b 有最大的 H 元素 x 使得

<math> a \\wedge x \\le b</math>。

这个元素 x 是 a 关于 b 的相对伪补元(pseudo-complement)，并指示为 <math>a \\Rightarrow b</math> (或 <math> a \\rightarrow b</math>)。

可以通过如下映射给出等价定义：对于 H 中某个固定的 a，

<math>f_a: H \\to H</math> 定义为 <math>f_a(x)=a\\wedge x</math>。

有界格 H 是 Heyting 代数，当且仅当所有映射 <math>f_a</math> 都是单调的伽罗瓦连接的下共轭(adjoint)。在这种情况下各自的上共轭 <math>g_a</math> 通过 <math>g_a(x)= (a \\Rightarrow x)</math> 给出，这里的 <math>\\Rightarrow</math> 定义同上。

完全Heyting代数是是完全格的 Heyting 代数。

在任何 Heyting 代数中，你可以通过设立 <math>\\lnot x = (x \\Rightarrow 0)</math> 定义某个元素 x 的伪补元 <math>\\lnot x</math>，这里的 0 是 Heyting 代数的最小元素。

Heyting 代数的一个元素 x 叫做正规的，如果 <math>x=\\lnot\\lnot x</math>。元素 x 是正规的，当且仅当对于 Heyting 代数的某个元素 y 有 <math>x=\\lnot y</math>。

性质

Heyting 代数总是符合分配律。这有时被陈述为公理，但实际上可以从相对伪补元的存在性得到。道理是作为伽罗瓦连接的下共轭，<math>\\wedge</math> 保持所有现存的上确界。所以分配律就是 <math>\\wedge</math> 对二元最小上界的保持。

进一步的，通过类似的论证，下列无限分配律在任何完全 Heyting 代数中都成立:

<math>x\\wedge\\bigvee Y = \\bigvee \\{x\\wedge y : y \\in Y\\}</math>

对于 H 中的任何元素 x 和H 的子集 Y。

不是所有 Heyting 代数都满足两个De Morgan 定律。但是，对于所有 Heyting 代数 H 下列陈述都是等价的:

H 满足两个 De Morgan 定律。

对于 H 中的所有 x y 有 <math>\\lnot(x \\wedge y)=\\lnot x \\vee \\lnot y</math>。

对于 H 中的所有 x 有 <math>\\lnot x \\vee \\lnot\\lnot x = 1</math>。

对于 H 中的所有 x y 有 <math>\\lnot\\lnot (x \\vee y) = \\lnot\\lnot x \\vee \\lnot\\lnot y</math>。

H 的一个元素 x 的伪补元是集合 <math>\\{ y : y \\wedge x = 0\\}</math> 的上确界，并且属于这个集合(就是说，<math>x \\wedge \\lnot x = 0</math> 成立)。

布尔代数准确的是如下成立的 Heyting 代数：对于所有 x 有 <math> x = \\lnot\\lnot x</math>，或等价的说，布尔代数准确的是如下成立的 Heyting 代数：对于所有 x 有 <math>x\\vee\\lnot x=1</math>。在这种情况下，元素 <math>a \\Rightarrow b</math> 等价于 <math>\\lnot a \\vee b</math>。

在任何 Heyting 代数中，最小 0 和最大元素 1 都是正规的。

任何 Heyting 代数的正规元素都构成一个布尔代数。除非 Heyting 代数的所有元素都是正规的，这个布尔代数都不会是这个 Heyting 代数的子格，因为交运算将是不同的。

例子

所有是有界格的全序集合也是 Heyting 代数，在这里对于不是 0 的所有 a 有 <math>\\lnot 0 = 1</math> 和 <math>\\lnot a = 0</math>。

所有的拓扑都以它的开集格的形式提供完全 Heyting 代数。在这种情况下，元素 <math>A \\Rightarrow B</math> 是 <math>A_c</math> 和 B 的并的内部，这里的 <math>A_c</math> 指示开集 A 的补。不是所有完全 Heyting 代数都有这种形式。这些问题在无点拓扑学中研究，这里完全 Heyting 代数也叫做 frame 或 locale。

命题直觉逻辑的Lindenbaum 代数是 Heyting 代数。它被定义为所有命题逻辑公式的集合，并通过逻辑蕴涵来排序: 对于任何两个公式 F 和 G 我们有 <math>F \\le G</math> ，当且仅当 <math>F \\models G</math>。在这个阶段 <math>\\le</math> 只是诱发 Heyting 代数所需要的偏序的预序。

应用于直觉逻辑的 Heyting 代数

Arend Heyting (1898年-1980年)自己感兴趣于以这种类型的结构来澄清直觉逻辑的基础地位。Peirce 定律的案例说明了 Heyting 代数的语义角色。没有简单的证明能证明 Peirce 定律不能从直觉逻辑的基本定律中推导出来。

Heyting 代数，从逻辑的立场来说，本质上是普通真值系统的一般化。同其他性质一起，最大元素，在逻辑中叫做 <math>\\top</math>，是'真'的同义词，普通二值逻辑系统是 Heyting 代数的最简单的例子，在这个代数中两个元素是<math>\\top</math>(真)和<math>\\bot</math>(假)。用抽象的术语说，两元素布尔代数也是 Heyting 代数。

经典有效的公式是在这种布尔代数中在对公式的变量的任意可能的真假指派下有 <math>\\top</math> 值的公式 — 就是说，它们是在普通真值表意义上的重言式。直觉有效的公式是在任何 Heyting 代数中在对公式变量的值的任何指派下有<math>\\top</math>值的公式。

你可以构造在其中 Peirce 定律不总是<math>\\top</math>的 Heyting 代数。考虑 Sierpinski 空间的开集(不是布尔代数的 Heyting 代数的最简单的例子)，并观察如果我们释义 P 为 {1}、Q 为 <math>\\varnothing</math>，则 Peirce 定律 ((P → Q) → P) → P 的释义是 <math>\\{1\\}\e \\{0,1\\} = \\top</math>。从我们刚才所说的，这不能是直觉推导出来的。详情参见Curry-Howard同构和类型论。