Web Analytics

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

CLASSICISTRANIERI HOME PAGE - YOUTUBE CHANNEL
Privacy Policy Cookie Policy Terms and Conditions
哥德尔数 - Wikipedia

哥德尔数

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

形式数论中,哥德尔编号是对某些形式语言的每个符号和公式指派一个叫做哥德尔数(GN)的唯一的自然数函数。这个概念是哥德尔为证明他的哥德尔不完备定理而引入的。

可计算函数集合的编号有时叫做哥德尔编号或有效编号。哥德尔编号可以被解释为一个编程语言,带有指派哥德尔数到每个可计算函数作为在这种编程语言中计算这个函数的值的程序。Roger 等价定理特征化了是哥德尔编号的可计算函数集合的编号。

目录

[编辑] 定义

给定一个可数集合 S,一个哥德尔编号是函数

f:S \to \mathbb{N}

带有 ff逆函数可计算函数

[编辑] 例子

[编辑] 步骤 1

哥德尔数是参照命题演算形式算术的符号而构造的.每个符号都被指派了一个自然数:

逻辑符号 数 1:12
\lnot 1 ("非")
\forall 2 ("所有")
\supset 3 ("如果-那么")
\vee 4 ("或")
\wedge 5 ("与")
( 6
) 7
S 8 ("后继")
0 9
= 10
. 11
+ 12
命题符号 大于 10 且被 3 整除的数
P 12
Q 15
R 18
S 21
个体变量 大于 10 且被 3 除余 1 的数
v 13
x 16
y 19
谓词符号 大于 10 且被 3 除余 2 的数
E 14
F 17
G 20

以此类推(NB 命题演算的语法确保了在 "P" 和 "+" 之间没有歧义,即使都指派了数 12)。

[编辑] 步骤 2

算术陈述/语句被参照素数系列指派唯一的哥德尔数。这基于一种简单的编码,它在本质上理解为
素数1 字符1 * 素数2 字符2 * 素数3 字符3
以此类推。 例如陈述
\forallx, P(x) 变成了
22 * 316 * 512 * 76 * 1116 * 137,因为
{2, 3, 5, 7, 11, ...} 是素数系列,而 2, 16, 12, 6, 16, 7 是有关的字符代码。这是个巨大但完全确定的数(14259844433335185664666562849653536301757812500)。

注意通过算术基本定理,这个天文数字可以被分解到唯一的素数因数中;所以转换哥德尔数回它的字符序列是可能的。

[编辑] 步骤 3

最后,算术陈述的序列也被进一步指派哥德尔数,比如序列
陈述1 (GN1)
陈述2 (GN2)
陈述3 (GN3)
(这里的 GN 指示一个哥德尔数)
得到哥德尔数 2GN1*3GN2*5GN3,我们称之为 GN4。哥德尔不完备定理的证明依赖于,对在形式算术中,有些陈述的集合在逻辑上蕴涵或证明其他陈述。比如可以证实 GN1, GN2 和 GN3 在一起,也就是 GN4 证明 GN5。因为这是在其自己的符号所授权的数之间的一个可证实的联系,例如 R。接着我们可以写 R(v,x) 来表达 "x 证明 v"。在 xv 是哥德尔数 GN4 和 GN5 的情况下我们可以说 R(GN5,GN4)

[编辑] 哥德尔不完备定理的非正式证明

哥德尔论证的核心是我们可以写陈述

\forallx, \lnotR(v,x)

它意味着

没有类型 v 的命题可以被证明

这个陈述的哥德尔数将是

22 * 316 * 51 * 718 * 116 * 1312 * 1716 * 197

我们将称之为 GN6。现在如果我们考虑陈述

\forallx, \lnotR(GN6,x)

我们将发现它声称了

没有声称“没有类型 v 的命题可以被证明”的命题可以被证明

这瓦解成陈述

这个命题不能被证明

如果这个陈述实际上可以被证明,则它的形式系统是不一致的,因为它证明了声称它自己不能被证明的东西(矛盾)。如果这个陈述在它的形式系统中不能被证明,则陈述所断言的实际上为真,所以这个陈述是一致的,但是因为形式系统包含语义上为真但不能(语法上)证明的陈述,则系统是不完备的。所以,假定形式系统是一致的,它必然是不完备的。

[编辑] 讨论

哥德尔编号不是唯一的。一般性的想法是把公式映射自然数上。一个可供选择的哥德尔编码是是考虑把步骤 1 的每个符号(通过一个映射 h)映射到一个 22 进制的数,所以 n 个符号的字符串组成的一个公式 s1s2s3...sn 可被映射到数

h(s_1) \times 22^{(n-1)} + h(s_2) \times 22^{(n-2)} + ... + h(s_{n-1}) \times 22^1 + h(s_n) \times 22^0

还有,哥德尔编号蕴涵了形式系统的每个推论规则都可以被表达为自然数的函数。如果 f 是哥德尔映射并且如果公式 C 可以推导自公式 AB,通过推论规则 r,就是说

A, B \vdash_r C \

则有某个自然数的算术函数 gr 使得

gr(f(A),f(B)) = f(C)

接着,因为这个形式系统是形式算术的,它能做关于数和它们相互的算术联系的陈述,可以得出这个系统也可以通过哥德尔编号的方式,间接的做关于自身的陈述: 就是说,形式系统的一个命题可以做出断言,在从哥德尔映射的角度查看的时候,能转换成关于同一个形式系统的其他命题,甚至是自身的断言。所以,通过这种方式一个形式算术可以做关于自身的断言,而成为自引用的,就象二阶逻辑。这提供给哥德尔(和其他逻辑学家)一种探索和发现关于形式系统的一致性和完备性性质的一种方法。

[编辑] 参见

[编辑] 引用

  • G?del, Kurt, "über formal unentscheidbare S?tze der Principia Mathematica und verwandter Systeme I", Monatsheft für Math. und Physik 38, 1931, S.173-198.

[编辑] 进一步阅读

  • G?del, Escher, Bach: an Eternal Golden Braid, by Douglas Hofstadter. This book defines and uses an alternative G?del numbering.
  • G?del's Proof by Ernest Nagel and James R. Newman. This book provides a good introduction and summary of the proof, with a large section dedicated to G?del's numbering.

Static Wikipedia (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 (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 2006 (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 - 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 February 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