In mathematics, Hilbert's program, formulated by German mathematician
Contents 1 Statement of Hilbert's program
2 Gödel's incompleteness theorems
3
Statement of Hilbert's program[edit]
The main goal of
A formulation of all mathematics; in other words all mathematical statements should be written in a precise formal language, and manipulated according to well defined rules. Completeness: a proof that all true mathematical statements can be proved in the formalism. Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects. Conservation: a proof that any result about "real objects" obtained using reasoning about "ideal objects" (such as uncountable sets) can be proved without using ideal objects. Decidability: there should be an algorithm for deciding the truth or falsity of any mathematical statement. Gödel's incompleteness theorems[edit]
Main article: Gödel's incompleteness theorems
It is not possible to formalize all of mathematics within a formal
system, as any attempt at such a formalism will omit some true
mathematical statements. There is no complete, consistent extension of
even Peano arithmetic based on a recursively enumerable set of axioms.
A theory such as Peano arithmetic cannot even prove its own
consistency, so a restricted "finitistic" subset of it certainly
cannot prove the consistency of more powerful theories such as set
theory.
There is no algorithm to decide the truth (or provability) of
statements in any consistent extension of Peano arithmetic. Strictly
speaking, this negative solution to the
Although it is not possible to formalize all mathematics, it is
possible to formalize essentially all the mathematics that anyone
uses. In particular Zermelo–Fraenkel set theory, combined with
first-order logic, gives a satisfactory and generally accepted
formalism for almost all current mathematics.
Although it is not possible to prove completeness for systems at least
as powerful as Peano arithmetic (at least if they have a computable
set of axioms), it is possible to prove forms of completeness for many
other interesting systems. The first big success was by Gödel himself
(before he proved the incompleteness theorems) who proved the
completeness theorem for first-order logic, showing that any logical
consequence of a series of axioms is provable. An example of a
non-trivial theory for which completeness has been proved is the
theory of algebraically closed fields of given characteristic.
The question of whether there are finitary consistency proofs of
strong theories is difficult to answer, mainly because there is no
generally accepted definition of a "finitary proof". Most
mathematicians in proof theory seem to regard finitary mathematics as
being contained in Peano arithmetic, and in this case it is not
possible to give finitary proofs of reasonably strong theories. On the
other hand, Gödel himself suggested the possibility of giving
finitary consistency proofs using finitary methods that cannot be
formalized in Peano arithmetic, so he seems to have had a more liberal
view of what finitary methods might be allowed. A few years later,
Gentzen gave a consistency proof for Peano arithmetic. The only part
of this proof that was not clearly finitary was a certain transfinite
induction up to the ordinal ε0. If this transfinite induction is
accepted as a finitary method, then one can assert that there is a
finitary proof of the consistency of Peano arithmetic. More powerful
subsets of second order arithmetic have been given consistency proofs
by
See also[edit] Grundlagen der Mathematik Foundational crisis of mathematics Atomism References[edit] G. Gentzen, 1936/1969. Die Widerspruchfreiheit der reinen Zahlentheorie. Mathematische Annalen 112:493–565. Translated as 'The consistency of arithmetic', in The collected papers of Gerhard Gentzen, M. E. Szabo (ed.), 1969. D. Hilbert. 'Die Grundlagen Der Elementaren Zahlentheorie'. Mathematische Annalen 104:485–94. Translated by W. Ewald as 'The Grounding of Elementary Number Theory', pp. 266–273 in Mancosu (ed., 1998) From Brouwer to Hilbert: The debate on the foundations of mathematics in the 1920s, Oxford University Press. New York. S.G. Simpson, 1988. Partial realizations of Hilbert's program. Journal of Symbolic Logic 53:349–363. R. Zach, 2005. Hilbert's Program Then and Now. Manuscript, arXiv:math/0508572v1. External links[edit] Entry on
v t e Computable knowledge Topics and concepts Alphabet of human thought Authority control Automated reasoning Commonsense knowledge Commonsense reasoning Computability Formal system Inference engine Knowledge base Knowledge-based systems Knowledge engineering Knowledge extraction Knowledge representation Knowledge retrieval Library classification Logic programming Ontology Personal knowledge base Question answering Semantic reasoner Proposals and implementations Zairja
Ars Magna (1300)
An Essay towards a Real Character, and a Philosophical
Language (1688)
In fiction
See also: Logic machines in fiction and List of f |