| | 在数学中，heyting 代数是构成对布尔代数的推广的特殊的偏序集。heyting 代数为直觉逻辑而提出，它是在其中排中律一般不成立的逻辑。完全heyting代数是无点拓扑学研究的中心对象。
形式定义
heyting 代数 h 是满足如下条件的有界格，对于在 h 中的所有 a 和 b 有最大的 h 元素 x 使得
<math> a wedge x le b</math>。
这个元素 x 是 a 关于 b 的相对伪补元(pseudo-complement)，并指示为 <math>a
ightarrow b</math> (或 <math> a
ightarrow b</math>)。
可以通过如下映射给出等价定义：对于 h 中某个固定的 a，
<math>f_a: h o h</math> 定义为 <math>f_a(x)=awedge x</math>。
有界格 h 是 heyting 代数，当且仅当所有映射 <math>f_a</math> 都是单调的伽罗瓦连接的下共轭(adjoint)。在这种情况下各自的上共轭 <math>g_a</math> 通过 <math>g_a(x)= (a
ightarrow x)</math> 给出，这里的 <math>
ightarrow</math> 定义同上。
完全heyting代数是是完全格的 heyting 代数。
在任何 heyting 代数中，你可以通过设立 <math>lnot x = (x
ightarrow 0)</math> 定义某个元素 x 的伪补元 <math>lnot x</math>，这里的 0 是 heyting 代数的最小元素。
heyting 代数的一个元素 x 叫做正规的，如果 <math>x=lnotlnot x</math>。元素 x 是正规的，当且仅当对于 heyting 代数的某个元素 y 有 <math>x=lnot y</math>。
性质
heyting 代数总是符合分配律。这有时被陈述为公理，但实际上可以从相对伪补元的存在性得到。道理是作为伽罗瓦连接的下共轭，<math>wedge</math> 保持所有现存的上确界。所以分配律就是 <math>wedge</math> 对二元最小上界的保持。
进一步的，通过类似的论证，下列无限分配律在任何完全 heyting 代数中都成立:
<math>xwedgeigvee y = igvee {xwedge 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 lnotlnot x = 1</math>。
对于 h 中的所有 x y 有 <math>lnotlnot (x vee y) = lnotlnot x vee lnotlnot y</math>。
h 的一个元素 x 的伪补元是集合 <math>{ y : y wedge x = 0}</math> 的上确界，并且属于这个集合(就是说，<math>x wedge lnot x = 0</math> 成立)。
布尔代数准确的是如下成立的 heyting 代数：对于所有 x 有 <math> x = lnotlnot x</math>，或等价的说，布尔代数准确的是如下成立的 heyting 代数：对于所有 x 有 <math>xveelnot x=1</math>。在这种情况下，元素 <math>a
ightarrow 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
ightarrow 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> op</math>，是'真'的同义词，普通二值逻辑系统是 heyting 代数的最简单的例子，在这个代数中两个元素是<math> op</math>(真)和<math>ot</math>(假)。用抽象的术语说，两元素布尔代数也是 heyting 代数。
经典有效的公式是在这种布尔代数中在对公式的变量的任意可能的真假指派下有 <math> op</math> 值的公式 — 就是说，它们是在普通真值表意义上的重言式。直觉有效的公式是在任何 heyting 代数中在对公式变量的值的任何指派下有<math> op</math>值的公式。
你可以构造在其中 peirce 定律不总是<math> op</math>的 heyting 代数。考虑 sierpinski 空间的开集(不是布尔代数的 heyting 代数的最简单的例子)，并观察如果我们释义 p 为 、q 为 <math>varnothing</math>，则 peirce 定律 ((p → q) → p) → p 的释义是 <math>{1}
e {0,1} = op</math>。从我们刚才所说的，这不能是直觉推导出来的。详情参见curry-howard同构和类型论。 | | 在数学中，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)=awedge 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=lnotlnot x</math>。元素 x 是正规的，当且仅当对于 Heyting 代数的某个元素 y 有 <math>x=lnot y</math>。
性质
Heyting 代数总是符合分配律。这有时被陈述为公理，但实际上可以从相对伪补元的存在性得到。道理是作为伽罗瓦连接的下共轭，<math>wedge</math> 保持所有现存的上确界。所以分配律就是 <math>wedge</math> 对二元最小上界的保持。
进一步的，通过类似的论证，下列无限分配律在任何完全 Heyting 代数中都成立:
<math>xwedgebigvee Y = bigvee {xwedge 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 lnotlnot x = 1</math>。
对于 H 中的所有 x y 有 <math>lnotlnot (x vee y) = lnotlnot x vee lnotlnot y</math>。
H 的一个元素 x 的伪补元是集合 <math>{ y : y wedge x = 0}</math> 的上确界，并且属于这个集合(就是说，<math>x wedge lnot x = 0</math> 成立)。
布尔代数准确的是如下成立的 Heyting 代数：对于所有 x 有 <math> x = lnotlnot x</math>，或等价的说，布尔代数准确的是如下成立的 Heyting 代数：对于所有 x 有 <math>xveelnot 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}ne {0,1} = top</math>。从我们刚才所说的，这不能是直觉推导出来的。详情参见Curry-Howard同构和类型论。 |
|
|