Privacy Policy Cookie Policy Terms and Conditions 替代公理 - Wikipedia

替代公理

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

公理化集合论和使用它的逻辑数学计算机科学分支中,替代公理模式Zermelo-Fraenkel 集合论的一个公理模式,它本质上断言一个集合在一个映射(泛函谓词)下的也是一个集合。它对于构造特定的大集合是必需的。

[编辑] 陈述

假定 P 是任何两个变量谓词,使得对于所有集合 x 有一个唯一的集合 y 使 P(x,y) 成立。接着我们可以形成一个变量的泛函谓词 F 使得 F(x) = y 当且仅当 P(x,y)。

替代公理声称,给定一个集合 A,我们可以找到一个集合 B,它的成员完全是 FA 的成员上的值。注意对于每个这种谓词 P 都有一个这个公理;所以,这是一个公理模式

在 Zermelo-Fraenkel 公理的形式语言中,这个公理模式读做:

(\forall x, \exist!\, y: P(x, y)) \rightarrow \forall A, \exist B, \forall y: y \in B \iff \exist x \in A : P(x, y)

换句话说,

如果给定任何集合 x有一个唯一的集合 y 使得 Pxy 成立,那么给定任何集合 A有着一个集合 B 使得,给定任何集合 yyB 的一个成员,当且仅当有是 A 的成员的一个集合 x 使得 P 对于 xy 成立。

如果你形式化谓词逻辑的语言为允许在公理模式中使用导出的泛函谓词,则这个公理模式可以写为:

\forall A, \exist B, \forall y: y \in B \iff \exist x \in A : y = F(x)

对于每个导出的一个变量的泛函谓词 F; 换句话说:

给定任何集合 A,有一个集合 B 使得,给定任何集合 yyB 的成员,当且仅当有是 A 的成员的一个集合 x 使得 y 等于 Fx 上的值。

我们可以使用外延公理来证实这个集合 B 是唯一的。我们称这个集合 BAF 下的,并指示它为 F(A) 或(使用集合建造符号形式) \{F(x) : x \in A\}

有时引用这个公理不带唯一性要求:

\forall A (\forall x \in A, \exist y: P(x, y)) \rightarrow \exist B, \forall x \in A, \exist y \in B: P(x, y)

就是说,谓词 P 不被限制为泛函的: 要应用它于一个集合 A,对应于 A 的每个元素 x 存在至少一个元素 y 就足够的;y 对每个 x 是唯一的不是必需的。在这种情况下。被断言存在的像集合 B 将为原集合的每个 x 包含至少一个这样的 y,不保证只包含唯一的一个。

有时陈述这个公理不对谓词加任何限制:

\forall A, \exist B, \forall x \in A : ((\exist y : P(x, y)) \rightarrow \exist y \in B : P(x, y))

就是说,根本不要求 P 把集合 A 的一个元素映射到任何东西。但是如果对于 A 的一个元素 x 有至少一个 y 对应于它,则像集合 B 将包含至少一个这样的 y

结果的公理也叫做有界公理搜集公理,表现得更强壮,但是这两个版本都可以从替代公理推导出来。任何泛函谓词都是谓词,所以有界公理也蕴涵替代公理,因此两个公理是等价的(在与其他 Zermelo-Fraenkel 公理一起出现的时候)。

[编辑] 例子应用

序数 ω2 = ω + ω (使用冯·诺伊曼的现代定义)是第一个不使用替代公理就不能构造的序数。无穷公理断言无限序列 ω = {0, 1 ,2 ,...} 的存在,并只断言了这个序列。你可能想定义 ω2 为序列 {ω, ω + 1, ω + 2,...},但是一般的序数的不需要是集合(例如,所有序数的类不是集合)。替代公理允许你把在 ω 中每个有限数 n 替代为对应的 ω + n,并保证它们的类是集合。注意你可以轻易的构造同构于 ω2 的良序集合而不用依靠替代公理: 简单的采用 ω 的两个复件的不交并,带有第二个复件大于第一个,但是这不是一个序数因为它不是通过包含而全序的。

明显的,序数到所有良序集合的指派的存在也要求替代公理。类似的指派基数到每个集合的冯·诺伊曼基数指派也要求替代公理,同选择公理一样。

所有的可数极限序数对它的类似于 ω2 的构造要求替代公理。更大的序数更不直接的依赖于替代公理。例如 ω1 是第一个不可数序数,可以构造如下: 可数良序的集合存在为 ℘(N×N) 的子集,通过分离公理幂集公理(在 A 上的关系A×A 的一个子集,因此是幂集 ℘(A×A) 的一个元素。关系的集合因此是 ℘(A×A) 的子集)。替代每个良序集合为它的序数。这是可数序数 ω1 的集合,它自身可以被证明是不可数的。这个构造使用替代公理两次;第一次确保对每个良序集合的一个序数指派,第二次替代良序集合为它们的序数。这是 Hartogs 数的结果的特殊情况,而一般情况可以类似的证明。

不带替代公理的选择公理(ZC 集合论)没有强到证实 Borel 集合是确定的;为此你需要替代公理。

[编辑] 历史和哲学

多数可以应用替代公理的应用实际上不需要它。例如,假设 f 是从集合 S 到集合 T函数。接着我们可以构造一个泛函谓词 F 使得在 xS 的成员的时候 F(x) = f(x),在其他时候设 F(x) 是我们希望的(与这个应用无关)任何东西。那么,给定 S 的一个子集 A,应用替代公理模式于 F,构造子集 A 在函数 f 下的 f(A) 为 \{ F(x) : x \in A \}(或表示为 F(A))。但是这里实际上不需要替代公理,因为 f(A) 是 T 的子集,所以我们可以使用分类公理模式来构造这个像为集合 \{ y \in T : \exists x \in A, y = f(x) \}。一般的说,分类公理在 FA 的成员上的值都属于某个预先构造的集合 T 的时候是足够的;替代公理只在不能获得这样的 T 的时候才需要,比如定义在真类的子集上的操作。

依据某些哲学家,在上述例子中最好应用分类公理于集合 T,因为分类公理在逻辑上弱于替代公理。实际上,替代公理在普通数学中是不需要,只对特定公理化集合论特征才需要。例如,你需要替代公理来从 ω2 向上构造冯·诺伊曼序数,而冯·诺伊曼序数对特定集合论结论是必需的。在良序集合的理论足够应用的其他方面,你不需要用替代公理构造这些序数。某些工作于数学基础的数学家,特别是那些集中于反对集合论的类型论的人,发现在他们的基础中对于任何目的这个公理(或它的类型论类似者)都是不需要的。替代公理在基于 topos 理论建造的基础上根本的难以表达,所以通常不包括它。然而,替代公理的争论不在于有人发现它的推论必然是假的(如选择公理的争论)而是发现它是没有必要的。

替代公理模式不是 Ernst Zermelo1908年所公理化的集合论(Z)的一部分;它由 Adolf Fraenkel 在 1922 年介入,得到了现代的 Zermelo-Fraenkel 集合论 (ZF)。Thoralf Skolem 在同一年晚些时候独立的发现了这个公理,实际上我们今天使用的公理列表是 Skolem 的最终版本 -- 通常不提及他的贡献是因为每个单独的公理都是 Zermelo 或 Fraenkel 早先发现的。从证明论的观点看增加替代公理形成了极大的差异;向 Zermelo 公理增加这个公理模式使系统在逻辑上更强,允许你证明更多的陈述。特别是,在ZF 中你可以通过构造冯·诺伊曼全集 Vω2模型证明 Z 的兼容性。(当然,哥德尔第二不完备定理证实了这两个理论都不能证明自身的相容性,如果它们是相容性的。)

THIS WEB:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - 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 - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - 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 - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - 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

Static Wikipedia 2008 (no images)

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 -

Static Wikipedia 2007:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - 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 - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - 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 - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - 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

Static Wikipedia 2006:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - 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 - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - 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 - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - 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