译者注：本人所译文章(以及其中本人的所注、所编和所评，用绿色示出)，首先是出于自身研究工作的需要；同时也兼顾作为同行们和学友们的非正式参考。文中诸多错误和谬误，恳望读者审查、指正。
不难发现,数学术语的译名,常常比较艰涩难读(但不应是晦涩难懂)，想来是为了避免与容易产生常义二义性的习常词汇相混淆，以保证数学术语涵义的唯一性和确切性。译者把这一条作为自己译作的信条之一；出于类似的考虑，在本人译作的译文中，亦常尝试着,采用插入空格、短逗号(正常逗号只用于独立句，但不是完整句的场合)、增加虚词等‘不规范’的辅助方式，来尽量避免译意的模糊性和二义性，提高译文的可读性。还应指出，译者将译作中第一次明确出现的、译者‘杜撰’的数学术语的译名(后加原文名),以及原文中相应部分,用阴影加以强调。愿读者不吝赐教。（在本段落中即有部分体现。请见带阴影的部分。）
为了避免术语译义上的混乱，本人译作中认为需要杜撰的重要术语,後附术语原文，必要时更附上已经存在的汉译术语，并一直保持。
http://en.wikipedia.org/wiki/Hilbert%27s_program
Thispagewaslastmodifiedon26February2013at01:27
Hilbert''sprogram希尔伯特规划
FromWikipedia,thefreeencyclopedia
Inmathematics,Hilbert''sprogram,formulatedbyGermanmathematicianDavidHilbert,wasaproposedsolutiontothefoundationalcrisisofmathematics,whenearlyattemptstoclarifythefoundationsofmathematicswerefoundtosufferfromparadoxesandinconsistencies.Asasolution,Hilbertproposedtogroundallexistingtheoriestoafinite,completesetofaxioms,andprovideaproofthattheseaxiomswereconsistent.Hilbertproposedthattheconsistencyofmorecomplicatedsystems,suchasrealanalysis,couldbeprovenintermsofsimplersystems.Ultimately,theconsistencyofallofmathematicscouldbereducedtobasicarithmetic.
在数学中,由德国数学家大卫·希尔伯特表述的希尔伯特的规划，是一种为了解决根本的数学危机的建议方案，早期是打算澄清数学基础中发现的悖论和不一致之处。作为一种解决方案,希尔伯特建议,将所有现有的的理论,建立到一个有限的完备公理集,并提供一种这些公理是一致的证明。希尔伯特提出,更复杂系统的一致性,如实数分析，可以依据简单系统来证明。最终,全部数学的一致性,可以简化到基本算术。
However,somearguethatG?del''sincompletenesstheoremsshowedin1931thatHilbert''sprogramwasunattainable.Inhisfirsttheorem,G?delshowedthatanyconsistentsystemwithacomputablesetofaxiomswhichiscapableofexpressingarithmeticcanneverbecomplete:itispossibletoconstructastatementthatcanbeshowntobetrue,butthatcannotbederivedfromtheformalrulesofthesystem.Inhissecondtheorem,heshowedthatsuchasystemcouldnotproveitsownconsistency,soitcertainlycannotbeusedtoprovetheconsistencyofanythingstronger.ThisrefutedHilbert''sassumptionthatafinitisticsystemcouldbeusedtoprovetheconsistencyofastrongertheory.
然而,有些人争辩,1931年证明的哥德尔不完备定理,表明希尔伯特规划是无法实现的。在哥德尔的第一个定理中证明,具有可计算的、能表达算法的公理集的任何一致性系统,永远不可能是完备的：你有可能构建出一个数学陈述，表明它确实存在,然而却不能从该系统的形式规则推导出来。在他的第二个定理中证明,这种系统无法证明自己的一致性，所以它当然不能用来证明任何更强事物的一致性。这就驳斥了希尔伯特的的假定，也就是,一个有穷系统不可能用于证明一个更强理论的一致性。
Contents
[hide]
1StatementofHilbert''sprogram希尔伯特规划的说明
2G?del''sincompletenesstheorems哥德尔完备性定理
3Hilbert''sprogramafterG?del后哥德尔的希尔伯特规划
4Seealso参见
5References参考文献
6Externallinks外部链接
·1.[edit]StatementofHilbert''sprogram希尔伯特规划的陈述
ThemaingoalofHilbert''sprogramwastoprovidesecurefoundationsforallmathematics.Inparticularthisshouldinclude:
希尔伯特规划的主要目标是为全部数学提供安全的基础。尤其应包括：
Aformalizationofallmathematics;inotherwordsallmathematicalstatementsshouldbewritteninapreciseformallanguage,andmanipulatedaccordingtowelldefinedrules.
一种包括全部数学的形式化：换句话说，所有的数学陈述,都应该用一种精确的形式化语言来编写，并按照定义确切的规则来操作。
Completeness:aproofthatalltruemathematicalstatementscanbeprovedintheformalism.
完备性：指一种证明，即所有真数学陈述都可以在形式体系中证明。
Consistency:aproofthatnocontradictioncanbeobtainedintheformalismofmathematics.Thisconsistencyproofshouldpreferablyuseonly"finitistic"reasoningaboutfinitemathematicalobjects
一致性：指一种证明，即在数学的形式体系中可以证明无矛盾性。这种一致性证明,对于有限数学对象,应当尽可能只使用‘有穷’推理。
Conservation:aproofthatanyresultabout"realobjects"obtainedusingreasoningabout"idealobjects"(suchasuncountablesets)canbeprovedwithoutusingidealobjects.
保守性：指一种证明，即使用与“理想对象”(如不可数集)有关的推理来获得的与“实际对象”有关的任何结果,都可以不使用理想对象而被证明。
Decidability:thereshouldbeanalgorithmfordecidingthetruthorfalsityofanymathematicalstatement.
可判定性：应该存在一种算法,用于判定任何数学陈述句的真实或虚假。
·2.[edit]G?del''sincompletenesstheorems哥德尔不完备性定理
Mainarticle:G?del''sincompletenesstheorems主条目：哥德尔不完备性定理
KurtG?delshowedthatmostofthegoalsofHilbert''sprogramwereimpossibletoachieve,atleastifinterpretedinthemostobviousway.Hissecondincompletenesstheoremstatedthatanyconsistenttheorypowerfulenoughtoencodeadditionandmultiplicationofintegerscannotproveitsownconsistency.ThiswipesoutmostofHilbert''sprogramasfollows:
哥德尔表明,大部分希尔伯特规划的目标是不可能达到的，这是对哥德尔不完备性定理若以最浅显的方式所作的解释。他的第二不完备性定理指出,任何强大到足以实现整数加法和乘法的一致性理论,都无法证明自身的一致性。这就排除了下面这些希尔伯特规划：
Itisnotpossibletoformalizeallofmathematics,asanyattemptatsuchaformalismwillomitsometruemathematicalstatements.
不可能形式化全部数学，因为任何打算使用这样的形式体系,会忽略掉某些真数学陈述。
AneasyconsequenceofG?del''sincompletenesstheoremisthatthereisnocompleteconsistentextensionofevenPeanoarithmeticwitharecursivelyenumerablesetofaxioms,soinparticularmostinterestingmathematicaltheoriesarenotcomplete.
哥德尔不完备性定理的一个简单结论是，即使是具有一个递归可枚举公理集的皮亚诺算术,也不存在完备的一致性扩展；所以，尤其是大多数令人感兴趣的数学理论,也是不完备的。
AtheorysuchasPeanoarithmeticcannotevenproveitsownconsistency,soarestricted"finitistic"subsetofitcertainlycannotprovetheconsistencyofmorepowerfultheoriessuchassettheory.
一种像皮亚诺算术这样的理论，甚至无法证明自身的一致性，所以它的受限的“有穷”子集,当然不能证明像集论那样的更强理论的一致性。
Thereisnoalgorithmtodecidethetruth(orprovability)ofstatementsinanyconsistentextensionofPeanoarithmetic.(StrictlyspeakingthisresultonlyappearedafewyearsafterG?del''stheorem,becauseatthetimethenotionofanalgorithmhadnotbeenpreciselydefined.)
这样的算法是不存在的，即判定任何皮亚诺算术一致性扩展的数学陈述的真值(或可能性)。（严格地说,这个结果只是在哥德尔定理之后几年才出现；因为算法的概念当时还没有被精确地定义。）
·3.[edit]Hilbert''sprogramafterG?del哥德尔定理之后的希尔伯特规划
Manycurrentlinesofresearchinmathematicallogic,prooftheoryandreversemathematicscanbeviewedasnaturalcontinuationsofHilbert''soriginalprogram.Muchofitcanbesalvagedbychangingitsgoalsslightly(Zach2005),andwiththefollowingmodificationssomeofitwassuccessfullycompleted:
当前,在数理逻辑，证明理论和逆数学(它试图通过找出证明所需的充分和必要的公理来评价一批常用数学结果的逻辑有效性
Althoughitisnotpossibletoformalizeallmathematics,itispossibletoformalizeessentiallyallthemathematicsthatanyoneuses.InparticularZermelo–Fraenkelsettheory,combinedwithfirst-orderlogic,givesasatisfactoryandgenerallyacceptedformalismforessentiallyallcurrentmathematics.
虽然形式化全部数学是不可能的，却可能形式化基本上人们常用的所有数学。尤其是与一阶逻辑相结合的策梅罗-Fraenkel集合论,基本上对于所有的当代数学，给出了一种满意的和一般可接受的形式体系。
AlthoughitisnotpossibletoprovecompletenessforsystemsatleastaspowerfulasPeanoarithmetic(atleastiftheyhaveacomputablesetofaxioms),itispossibletoproveformsofcompletenessformanyinterestingsystems.ThefirstbigsuccesswasbyG?delhimself(beforeheprovedtheincompletenesstheorems)whoprovedthecompletenesstheoremforfirst-orderlogic,showingthatanylogicalconsequenceofaseriesofaxiomsisprovable.Anexampleofanon-trivialtheoryforwhichcompletenesshasbeenprovedisthetheoryofalgebraicallyclosedfieldsofgivencharacteristic.
虽然至少对于像皮亚诺算术那样强大的系统（如果至少他们具有一个可计算公理集）还不可能证明其完备性，却对于许多令人关注的系统,能证明其完备性的形式。第一个伟大的成功是由哥德尔自己（之前，他证明了不完备性定理）完成的，他对一阶逻辑证明了完备性定理，表明其一系列公理的任何合乎逻辑的结果都是可证明的。其完备性已被证明的一个非平凡理论的一个例子,是代数上所给特征的闭域的理论。
Thequestionofwhethertherearefinitaryconsistencyproofsofstrongtheoriesisdifficulttoanswer,mainlybecausethereisnogenerallyaccepteddefinitionofa"finitaryproof".MostmathematiciansinprooftheoryseemtoregardfinitarymathematicsasbeingcontainedinPeanoarithmetic,andinthiscaseitisnotpossibletogivefinitaryproofsofreasonablystrongtheories.OntheotherhandG?delhimselfsuggestedthepossibilityofgivingfinitaryconsistencyproofsusingfinitarymethodsthatcannotbeformalizedinPeanoarithmetic,soheseemstohavehadamoreliberalviewofwhatfinitarymethodsmightbeallowed.Afewyearslater,GentzengaveaconsistencyproofforPeanoarithmetic.Theonlypartofthisproofthatwasnotclearlyfinitarywasacertaintransfiniteinductionuptotheordinalε0.Ifthistransfiniteinductionisacceptedasafinitarymethod,thenonecanassertthatthereisafinitaryproofoftheconsistencyofPeanoarithmetic.MorepowerfulsubsetsofsecondorderarithmetichavebeengivenconsistencyproofsbyGaisiTakeutiandothers,andonecanagaindebateaboutexactlyhowfinitaryorconstructivetheseproofsare.(Thetheoriesthathavebeenprovedconsistentbythesemethodsarequitestrong,andincludemost"ordinary"mathematics.)
强理论是否存在有穷一致性的提问,是难以回答的，这主要是因为所谓“有穷证明”并没有普遍接受的定义。大多数证明论数学家似乎认为在皮亚诺算术中包含了有穷数学；在这种情况下,要合理地给出强理论有穷证明是不可能的。另一方面,哥德尔自己建议使用有穷方法来给出有穷一致性证明的可能性；而这在皮亚诺算术中是不能被形式化的。这样看来,他似乎持有一种更宽松的观点,认为有穷方法可以被允许。几年后,根岑为皮亚诺算术给出了一个一致性证明。该证明有一点并不清楚：有穷是一个取决于序ε0的某种超限归纳法。如果这一超限归纳法被接受为有穷方法,则可以断言,皮亚诺算术的一致性存在着一个有穷的证明。更强的二阶算术子集已经由GaisiTakeuti和其他人给出了一致性证明；可以再次辩论的是,这些证明究竟是如何有穷或构建的。（通过这些方法证明是一致性的理论是相当强的,且已包括了大多数“普通”数学。）
AlthoughthereisnoalgorithmfordecidingthetruthofstatementsinPeanoarithmetic,therearemanyinterestingandnon-trivialtheoriesforwhichsuchalgorithmshavebeenfound.Forexample,Tarskifoundanalgorithmthatcandecidethetruthofanystatementinanalyticgeometry(moreprecisely,heprovedthatthetheoryofrealclosedfieldsisdecidable).GiventheCantor–Dedekindaxiom,thisalgorithmcanberegardedasanalgorithmtodecidethetruthofanystatementinEuclideangeometry.ThisissubstantialasfewpeoplewouldconsiderEuclideangeometryatrivialtheory.
虽然在皮亚诺算术中还没有用于判定陈述句真性值的算法，然而对于许多有趣和非平凡的理论，这样的算法已经发现了。例如,塔斯基发现了一种算法，可以判定在解析几何中任何语句的真性值（更确切地说,他证明了实数闭域理论是可判定的）。考虑到康托-戴德金公理，该算法可以被看作为判定欧几里德几何中任何语句真性值的一种算法。这很重要，因为很少有人会认为欧几里德几何是一种平凡理论。
·4.[edit]Seealso参见
GrundlagenderMathematik
Foundationalcrisisofmathematics
Atomism
·5.[edit]References参考文献
G.Gentzen,1936/1969.DieWiderspruchfreiheitderreinenZahlentheorie.MathematischeAnnalen112:493–565.Translatedas''Theconsistencyofarithmetic'',inThecollectedpapersofGerhardGentzen,M.E.Szabo(ed.),1969.
D.Hilbert.''DieGrundlagenDerElementarenZahlentheorie''.MathematischeAnnalen104:485–94.TranslatedbyW.Ewaldas''TheGroundingofElementaryNumberTheory'',pp.266–273inMancosu(ed.,1998)FromBrouwertoHilbert:Thedebateonthefoundationsofmathematicsinthe1920s,OxfordUniversityPress.NewYork.
S.G.Simpson,1988.PartialrealizationsofHilbert''sprogram.JournalofSymbolicLogic53:349–363.
R.Zach,2005.Hilbert''sProgramThenandNow.Manuscript,arXiv:math/0508572v1.
·6.[edit]Externallinks外部链接
EntryonHilbert''sprogramattheStanfordEncyclopediaofPhilosophy.
[hide]v
t
e
Computableknowledge
Topicsandconcepts
Alphabetofhumanthought
Authoritycontrol
Automatedreasoning
Commonsenseknowledgebase
Commonsensereasoning
Computability
Formalsystem
Inferenceengine
Knowledgebase
Knowledge-basedsystems
Knowledgediscovery
Knowledgeengineering
Knowledgerepresentation
Knowledgeretrieval
Knowledgeextraction
Libraryclassification
Logicprogramming
Ontology
Questionanswering
Semanticreasoner
Proposalsandimplementations
Zairja
ArsMagna(RamonLlull,1300)
AnEssaytowardsaRealCharacterandaPhilosophicalLanguage(JohnWilkins,1688)
Calculusratiocinator&Characteristicauniversalis(GottfriedLeibniz,1700)
DeweyDecimalClassification(MelvilDewey,1876)
Begriffsschrift(GottlobFrege,1879)
Mundaneum(PaulOtlet&HenriLaFontaine,1910)
Logicalatomism(BertrandRussell,1918)
TractatusLogico-Philosophicus(LudwigWittgenstein,1921)
Hilbert''sprogram(DavidHilbert,1920s)
Incompletenesstheorem(KurtG?del,1931)
Memex(VannevarBush,1945)
Prolog(1972)
Cyc(1984)
TrueKnowledge(TrueKnowledgeLtd.,2007)
WolframAlpha(WolframResearch,2009)
Watson(IBM,2011)
Siri(Apple,2011)
KnowledgeGraph(Google,2012)
Infiction
TheEngine(Gulliver''sTravels,1726)
Joe("ALogicNamedJoe,"1946)
TheLibrarian(SnowCrash,1992)
Dr.Know(A.I.ArtificialIntelligence,2001)
Waterhouse(TheBaroqueCycle,2003)
Seealso:LogicmachinesinfictionandListoffictionalcomputers
Categories:
Mathematicallogic
Prooftheory
Hilbert''sproblems
2
1
|
|
