ebooksgratis.com

See also ebooksgratis.com: no banners, no cookies, totally FREE.

CLASSICISTRANIERI HOME PAGE - YOUTUBE CHANNEL
Privacy Policy Cookie Policy Terms and Conditions
Heyting代数 - Wikipedia

Heyting代数

维基百科,自由的百科全书

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

目录

[编辑] 形式定义

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

 a \wedge x \le b

这个元素 xa 关于 b相对伪补元(pseudo-complement),并指示为 a \rightarrow b

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

f_a: H \to H 定义为 f_a(x)=a\wedge x

有界格 H 是 Heyting 代数,当且仅当所有映射 fa 都是单调的伽罗瓦连接的下伴随(adjoint)。在这种情况下各自的上伴随 ga 通过 g_a(x)= a \rightarrow x 给出,这里的 \rightarrow 定义同上。

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

在任何 Heyting 代数中,你可以通过设立 \lnot x = (x \rightarrow 0) 定义某个元素 x伪补元 \lnot x,这里的 0 是 Heyting 代数的最小元素。注意 a\wedge \lnot a = 0,而 \lnot a 是有这个性质的最大元素。但是 a\vee\lnot a=1 不通常为真,所以 \lnot 只是伪补运算不是真正的补元

[编辑] 性质

Heyting 代数总是符合分配律。就是说,给定格 A 和二元运算 \rightarrow 它们形成一个 Heyting 代数,当且仅当如下成立:

  1. a\rightarrow a = 1
  2. a\wedge(a\rightarrow b)=a\wedge b
  3. b\wedge(a\rightarrow b)= b
  4. a\rightarrow (b\wedge c)= (a\rightarrow b)\wedge (a\rightarrow c) (分配律)

这有时被陈述为公理,但实际上可以从相对伪补元的存在性得到。道理是作为伽罗瓦连接的下伴随,\wedge 保持所有现存的上确界。所以分配律就是 \wedge 对二元最小上界的保持。

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

x\wedge\bigvee Y = \bigvee \{x\wedge y : y \in Y\}

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

不是所有 Heyting 代数都满足两个德·摩根定律。但是,对于所有 Heyting 代数 H 下列陈述都是等价的:

  1. H 满足两个德·摩根定律。
  2. \lnot(x \wedge y)=\lnot x \vee \lnot y,对于所有 H 中的 x y
  3. \lnot x \vee \lnot\lnot x = 1,对于所有 H 中的 x
  4. \lnot\lnot (x \vee y) = \lnot\lnot x \vee \lnot\lnot y,对于所有 H 中的 x y

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

Heyting 代数 H 的一个元素 x 叫做正规的,如果如下等价条件之一成立:

  1. x=\lnot\lnot x
  2. x=\lnot y,对于 H 的某个元素 y

Heyting 代数 H 是布尔代数,如果下列等价条件之一成立的:

  1. 所有 H 中的 x 都是正规的。
  2. x\vee\lnot x=1,对于所有 H 中的 x

在这种情况下,元素 a \rightarrow b 等价于 \lnot a \vee b

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

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

[编辑] 例子

  • 所有是有界格的全序集合也是 Heyting 代数,在这里对于不是 0 的所有 a\lnot 0 = 1\lnot a = 0
  • 不是布尔代数的最简单的 Heyting 代数是线性有序集合 {0, ½, 1} 带有如下运算:
a \land b
b

a
0 ½ 1
0 0 0 0
½ 0 ½ ½
1 0 ½ 1
 
a \lor b
b

a
0 ½ 1
0 0 ½ 1
½ ½ ½ 1
1 1 1 1
 
a \rightarrow b
b

a
0 ½ 1
0 1 1 1
½ 0 1 1
1 0 ½ 1
注意 ½ \lor\neg ½ = ½ \lor\rightarrow0) = ½ \lor0 = ½ 不满足排中律。
  • 所有的拓扑都以它的开集格的形式提供完全 Heyting 代数。在这种情况下,元素 A \Rightarrow BAcB 的并的内部,这里的 Ac 指示开集 A 的补。不是所有完全 Heyting 代数都有这种形式。这些问题在无点拓扑学中研究,这里完全 Heyting 代数也叫做 framelocale
  • 命题直觉逻辑Lindenbaum 代数是 Heyting 代数。它被定义为所有命题逻辑公式的集合,并通过逻辑蕴涵来排序: 对于任何两个公式 FG 我们有 F \le G ,当且仅当 F \models G。在这个阶段 \le 只是诱发 Heyting 代数所需要的偏序的预序

[编辑] 应用于直觉逻辑的 Heyting 代数

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

如果用 Heyting 代数的术语解释直觉命题逻辑的公理,则对于任何值到公式变量的指派下的任何 Heyting 代数,它们将求值得到最大元素 1。例如,通过伪补元的定义,(P \land Q) \rightarrow P 是最大元素 x 使得 P \land Q \land x \le P。这个不等式对任何 x 都满足,所以最大的这种 x 是 1。

进一步的,肯定前件规则允许从公式 P 和 P → Q 导出公式 Q。在任何 Heyting 代数中,如果 P 有值 1,并且 P → Q 有值 1,因为它意味着 P \land 1 \le Q,所以 1 \land 1 \le Q;因此 Q 只能有值 1。

这意味着如果一个公式可以从直觉逻辑中演绎出来,即从它的公理通过肯定前件推导出来,则在任何值到公式变量的指派下的任何 Heyting 代数中,它总是有值 1。但是你可以一个 Heyting 代数在其中皮尔士定律的值不总是 1。考虑上面给出的三元素代数 {0,½,1}。如果我们指派 ½ 到 P 并指派 0 到 Q,则皮尔士定律 ((P → Q) → P) → P 的值是 ½。这得出了皮尔士定律是不能直觉逻辑推导的。这在类型论中的蕴涵详情请参见Curry-Howard同构

反过来也是可证明的: 如果一个公式总是有值 1,则它是可以从直觉逻辑的公理系统演绎出来的,所以“直觉有效”的公式严格的是永远有值 1 的公式。这类似于“经典有效”公式是在两元素布尔代数中在对公式变量的任何可能真和假指派下永远有值 1 的公式,它们在通常的真值表意义上是重言式。从逻辑的立场,Heyting 代数是普通真值系统的推广,它的最大元素 1 可比拟于真。平常的二值逻辑系统是 Heyting 代数的特殊情况,和最小的非平凡的系统,在其中仅有的代数元素是 1(真)和 0 (假)。

[编辑] 引用

  • Rutherford, Daniel Edwin(1965).Introduction to Lattice Theory.Oliver and Boyd. 
  • F. Borceux, Handbook of Categorical Algebra 3, In Encyclopedia of Mathematics and its Applications, Vol. 53, Cambridge University Press, 1994.
  • G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003.

[编辑] 参见


aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -