| 词条 | Hilbert's second problem |
| 释义 |
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that the arithmetic is consistent – free of any internal contradictions. Hilbert stated that the axioms he considered for arithmetic were the ones given in {{harvtxt|Hilbert|1900}}, which include a second order completeness axiom. In the 1930s, Kurt Gödel and Gerhard Gentzen proved results that cast new light on the problem. Some feel that Gödel's theorems give a negative solution to the problem, while others consider Gentzen's proof as a partial positive solution. Hilbert's problem and its interpretationIn one English translation, Hilbert asks:
Hilbert's statement is sometimes misunderstood, because by the "arithmetical axioms" he did not mean a system equivalent to Peano arithmetic, but a stronger system with a second-order completeness axiom. The system Hilbert asked for a completeness proof of is more like second-order arithmetic than first-order Peano arithmetic. As a nowadays common interpretation, a positive solution to Hilbert's second question would in particular provide a proof that Peano arithmetic is consistent. There are many known proofs that Peano arithmetic is consistent that can be carried out in strong systems such as Zermelo–Fraenkel set theory. These do not provide a resolution to Hilbert's second question, however, because someone who doubts the consistency of Peano arithmetic is unlikely to accept the axioms of set theory (which is much stronger) to prove its consistency. Thus a satisfactory answer to Hilbert's problem must be carried out using principles that would be acceptable to someone who does not already believe PA is consistent. Such principles are often called finitistic because they are completely constructive and do not presuppose a completed infinity of natural numbers. Gödel's incompleteness theorem places a severe limit on how weak a finitistic system can be while still proving the consistency of Peano arithmetic. Gödel's incompleteness theorem{{main|Gödel's incompleteness theorems}}Gödel's second incompleteness theorem shows that it is not possible for any proof that Peano Arithmetic is consistent to be carried out within Peano arithmetic itself. This theorem shows that if the only acceptable proof procedures are those that can be formalized within arithmetic then Hilbert's call for a consistency proof cannot be answered. However, as Nagel and Newman (1958:96–99) explain, there is still room for a proof that cannot be formalized in arithmetic: "This imposing result of Godel's analysis should not be misunderstood: it does not exclude a meta-mathematical proof of the consistency of arithmetic. What it excludes is a proof of consistency that can be mirrored by the formal deductions of arithmetic. Meta-mathematical proofs of the consistency of arithmetic have, in fact, been constructed, notably by Gerhard Gentzen, a member of the Hilbert school, in 1936, and by others since then. ... But these meta-mathematical proofs cannot be represented within the arithmetical calculus; and, since they are not finitistic, they do not achieve the proclaimed objectives of Hilbert's original program. ... The possibility of constructing a finitistic absolute proof of consistency for arithmetic is not excluded by Gödel’s results. Gödel showed that no such proof is possible that can be represented within arithmetic. His argument does not eliminate the possibility of strictly finitistic proofs that cannot be represented within arithmetic. But no one today appears to have a clear idea of what a finitistic proof would be like that is not capable of formulation within arithmetic."[2] Gentzen's consistency proof{{main|Gentzen's consistency proof}}In 1936, Gentzen published a proof that Peano Arithmetic is consistent. Gentzen's result shows that a consistency proof can be obtained in a system that is much weaker than set theory. Gentzen's proof proceeds by assigning to each proof in Peano arithmetic an ordinal number, based on the structure of the proof, with each of these ordinals less than ε0.[3] He then proves by transfinite induction on these ordinals that no proof can conclude in a contradiction. The method used in this proof can also be used to prove a cut elimination result for Peano arithmetic in a stronger logic than first-order logic, but the consistency proof itself can be carried out in ordinary first-order logic using the axioms of primitive recursive arithmetic and a transfinite induction principle. Tait (2005) gives a game-theoretic interpretation of Gentzen's method. Gentzen's consistency proof initiated the program of ordinal analysis in proof theory. In this program, formal theories of arithmetic or set theory are assigned ordinal numbers that measure the consistency strength of the theories. A theory will be unable to prove the consistency of another theory with a higher proof theoretic ordinal. Modern viewpoints on the status of the problemWhile the theorems of Gödel and Gentzen are now well understood by the mathematical logic community, no consensus has formed on whether (or in what way) these theorems answer Hilbert's second problem. Simpson (1988:sec. 3) argues that Gödel's incompleteness theorem shows that it is not possible to produce finitistic consistency proofs of strong theories. Kreisel (1976) states that although Gödel's results imply that no finitistic syntactic consistency proof can be obtained, semantic (in particular, second-order) arguments can be used to give convincing consistency proofs. Detlefsen (1990:p. 65) argues that Gödel's theorem does not prevent a consistency proof because its hypotheses might not apply to all the systems in which a consistency proof could be carried out. Dawson (2006:sec. 2) calls the belief that Gödel's theorem eliminates the possibility of a persuasive consistency proof "erroneous", citing the consistency proof given by Gentzen and a later one given by Gödel in 1958. See also
Notes1. ^From the English translation by M. Newson, 1902 provided by http://aleph0.clarku.edu/~djoyce/hilbert/problems.html . 2. ^A similar quotation with minor variations in wording appears in the 2001 edition p.107-108, as revised by Douglas R. Hofstadter, New York University Press, NY, {{ISBN|0-8147-5816-9}}. 3. ^Actually, the proof assigns a "notation" for an ordinal number to each proof. The notation is a finite string of symbols that intuitively stands for an ordinal number. By representing the ordinal in a finite way, Gentzen's proof does not presuppose strong axioms regarding ordinal numbers. 4. ^:A definition of a "finitary formal system" is given by Goldstein (p. 144, footnote 7)::: "...finitary formal systems... formal systems with a finite or denumerable (or countable) alphabet of symbols, wffs [well-formed-formulas] of finite length, and rules of inference involving only finitely many premises. (Logicians also work with formal systems with uncountable alphabets, with infinitely long wffs, and with proofs having infinitely many premises."(p. 144, footnote 7) References
| title = On an alleged refutation of Hilbert's Program using Gödel's First Incompleteness Theorem | journal = Journal of Philosophical Logic | doi = 10.1007/BF00263316 | volume = 19 | issue = 4 | year = 1990 | pages = 343–377 | author = Michael Detlefsen | publisher= Springer }}
|first=David |last=Hilbert|journal=Jahresbericht der Deutschen Mathematiker-Vereinigung|year=1900|volume=8|pages=180–184|url=http://resolver.sub.uni-goettingen.de/purl?PPN37721857X}}
| author = George Kreisel | title = What have we learnt from Hilbert's second problem? | booktitle = Mathematical developments arising from Hilbert problems (Proc. Sympos. Pure Math., Northern Illinois Univ., De Kalb, Ill.,) | pages = 93–130 | publisher = Amer. Math. Soc. | year = 1976 | location = Providence, R. I. | isbn = 0-8218-1428-1 }}
| title = Partial realizations of Hilbert's Program | jstor = 2274508 | journal = Journal of Symbolic Logic | volume = 53 | issue = 2 | year = 1988 | pages = 349–363 | ISSN = 0022-4812 | citeseerx = 10.1.1.79.5808}} Available online at http://www.math.psu.edu/simpson/papers/hilbert.pdf .
External links
{{Hilbert's problems}} 1 : Hilbert's problems |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。