在数学里,海廷代数(Heyting algebra)是一特殊的偏序集,经由广义化布尔代数而成,得名于阿兰德·海廷。海廷代数是作为直觉主义逻辑的模型而产生的,是一种排中律不总是成立的逻辑。完全海廷代数是无点拓扑学的核心。
形式定义
海廷代数H为一有界格,满足如下条件:对于在H中的所有a和b,存在一属于H的最大元素x,使得
- 。
元素x被称为a对应于b的相对伪补元(relative pseudo-complement),并标记为。H中最大和最小元素分别写成1和0。
任一海廷代数,皆可定义出任一元素x的伪补元¬x为¬x = (x → 0)。依定义,a ∧ ¬a = 0,,且¬a是具有此一性质的最大元素。不过,因为a ∨ ¬a = 1,并不总是真的,所以¬只是一个伪补运算,而不是像在布尔代数中所见真正的补元。
海廷代数H的子代数是指H的子集H1,包含0和1,并在∧、∨和→等运算下是封闭的。这表示在¬下也是封闭的。
其他等价的定义
海廷代数的等价定义可由如下映射给出:对于H中的某些固定元素a,
- 定义为,
有界格H是海廷代数,当且仅当所有的映射fa都是单调伽罗瓦连接的下伴随(lower adjoint)。在这种情况下,其相对应的上伴随是由给出的,其中的定义同上。
性质
海廷代数总是符合分配律。就是说,给定格A和二元运算它们形成一个海廷代数,当且仅当如下成立:
- (分配律)
这有时被陈述为公理,但实际上可以从相对伪补元的存在性得到。道理是作为伽罗瓦连接的下伴随,保持所有现存的上确界。所以分配律就是对二元最小上界的保持。
进一步的,通过类似的论证,下列无限分配律在任何完全海廷代数中都成立:
对于任何H中的元素x和任何H的子集Y。
不是所有海廷代数都满足两个德·摩根定律。但是,对于所有海廷代数H下列陈述都是等价的:
- H满足两个德·摩根定律。
- ,对于所有H中的x y。
- ,对于所有H中的x。
- ,对于所有H中的x y。
H的一个元素x的伪补元是集合的上确界,并且属于这个集合(就是说,成立)。
海廷代数H的一个元素x叫做正规的,如果如下等价条件之一成立:
- 。
- ,对于H的某个元素y。
海廷代数H是布尔代数,如果下列等价条件之一成立的:
- 所有H中的x都是正规的。
- ,对于所有H中的x。在这种情况下,元素等价于。
在任何海廷代数中,最小0和最大元素1都是正规的。
任何海廷代数的正规元素都构成一个布尔代数。除非海廷代数的所有元素都是正规的,这个布尔代数都不会是这个海廷代数的子格,因为并运算将是不同的。
例子
- 所有是有界格的全序集合也是海廷代数,在这里对于不是0的所有a有和。
- 不是布尔代数的最简单的海廷代数是线性有序集合{0, ½, 1}带有如下运算:
|
|
|
- 注意½ ½ = ½ (½ 0) = ½ 0 = ½不满足排中律。
应用于直觉主义逻辑的海廷代数
阿兰德·海廷(1898年-1980年)自己感兴趣于以这种类型的结构来澄清直觉主义逻辑的基础地位。皮尔士定律的案例说明了海廷代数的语义角色,并给出皮尔士定律不能从直觉主义逻辑的基本定律中推导出来的最简单的已知证明。
如果用海廷代数的术语解释直觉主义命题逻辑的公理,则对于任何值到公式变量的指派下的任何海廷代数,它们将求值得到最大元素1。例如,通过伪补元的定义,是最大元素x使得。这个不等式对任何x都满足,所以最大的这种x是1。
进一步的,肯定前件规则允许从公式P和P → Q导出公式Q。在任何海廷代数中,如果P有值1,并且P → Q有值1,因为它意味着,所以;因此Q只能有值1。
这意味着如果一个公式可以从直觉主义逻辑中演绎出来,即从它的公理通过肯定前件推导出来,则在任何值到公式变量的指派下的任何海廷代数中,它总是有值1。但是你可以一个海廷代数在其中皮尔士定律的值不总是1。考虑上面给出的三元素代数{0,½,1}。如果我们指派½到P并指派0到Q,则皮尔士定律 ((P → Q) → P) → P的值是½。这得出了皮尔士定律是不能直觉主义逻辑推导的。这在类型论中的蕴涵详情请参见柯里-霍华德同构。
反过来也是可证明的:如果一个公式总是有值1,则它是可以从直觉主义逻辑的公理系统演绎出来的,所以“直觉主义有效”的公式严格的是永远有值1的公式。这类似于“经典有效”公式是在两元素布尔代数中在对公式变量的任何可能真和假指派下永远有值1的公式,它们在通常的真值表意义上是重言式。从逻辑的立场,海廷代数是普通真值系统的推广,它的最大元素1可比拟于真。平常的二值逻辑系统是海廷代数的特殊情况,和最小的非平凡的系统,在其中仅有的代数元素是1(真)和0 (假)。
参见
注
引用
外部链接
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.