bits.

FREE HISTORICAL FIGURES OF COMPUTING PROFILE

David Hilbert

1862–1943 · Mathematician

David Hilbert

Mathematician · 1862–1943 · Germany

Hilbert helped turn foundations into mathematical questions: what follows from an axiom system, whether its assumptions conflict, and whether a procedure can decide a whole class of problems. These questions remain practical whenever a programmer distinguishes checking a supplied certificate from finding one.

Life and scope of the work

Hilbert was born on 23 January 1862 near Königsberg, in East Prussia. He received his doctorate at Königsberg in 1885 under Ferdinand von Lindemann, moved to Göttingen in 1895 and retired in 1930. He died in Göttingen on 14 February 1943. His work included invariant theory, algebraic number theory, geometry, integral equations and mathematical physics, as well as logic. University historical biography.

His Foundations of Geometry appeared in 1899. His published 1900 problems ranged across mathematics: the second concerned consistency of arithmetic, and the tenth asked for a method to decide whether a Diophantine equation has an integer solution. The published list contains 23 problems; it should not be confused with a transcript in which all 23 were necessarily delivered orally. Original address in translation.

In the 1920s, Hilbert and collaborators pursued formalization of mathematics and a consistency proof using finitist reasoning. Paul Bernays was a central collaborator; their Grundlagen der Mathematik appeared in 1934 and 1939. This consistency project and the decision problem are related but distinct. Historical and philosophical analysis.

Four questions that must stay separate

A formal derivation is a finite object assembled using specified axioms and inference rules. A model interprets the language and makes the axioms true. These give two notions often blurred in informal writing: derivability inside a calculus and truth in an interpretation.

A theory is consistent if it does not derive both a sentence and its negation. It is syntactically complete if it proves either a sentence or its negation for every sentence in its language. A proof calculus is semantically complete for a class of interpretations when every consequence valid in those interpretations has a derivation. A problem is decidable if a terminating algorithm gives the correct yes/no answer on every permitted input.

Consequently, a semantically complete first-order proof calculus need not give a decision algorithm for validity. It guarantees that a valid sentence has a finite proof. It does not supply a computable deadline after which an unsuccessful proof search can declare the sentence invalid.

The Entscheidungsproblem, in its standard first-order formulation, asks for such a validity-deciding procedure. Church and Turing established a negative answer in 1936 using precise accounts of effective computation. “Truth of any mathematical statement” is too imprecise: specify the language, interpretations and allowed procedures.

Worked mechanism: a proof checker and a searcher

Consider an original, deliberately small system. Its formulas are positive integers. Its axiom is 1. There are two inference rules: from n derive 2n, or from n derive 2n + 1. A proof is a list beginning at 1; each next number must be obtained from an earlier listed number by one of the rules.

The list below proves 13:

1      axiom
3      2 × 1 + 1
6      2 × 3
13     2 × 6 + 1

A checker examines four entries and the claimed parent of each non-axiom step. If a student instead supplies 1, 3, 7, 13, the last step is invalid: neither doubling 7 nor doubling and adding one gives 13, and no earlier entry works either. The desired conclusion may still be provable; this submitted proof is wrong.

For this particular system we can do more than check. Given a positive integer n greater than 1, repeatedly replace it by floor(n/2). Eventually we reach 1 because each step strictly decreases the positive integer. Reverse the chain. An even child uses doubling; an odd child uses doubling plus one. For 13 the reverse chain is 13, 6, 3, 1, yielding the displayed proof. Every positive integer is therefore derivable.

This example has a decision procedure because we established a special property of its rules. We cannot generalize from “proofs are checkable” to “theorems are decidable” for arbitrary systems. For an effectively presented theory, enumerate candidate finite proofs and check them. A target theorem will eventually appear. If the target is not a theorem, this search may run forever.

One tempting repair is to search for both a sentence and its negation. If the theory is consistent and syntactically complete, this parallel search terminates with exactly one answer. Incompleteness removes that guarantee: neither search must succeed for an independent sentence. This is a precise reason the distinction matters, not a slogan about machines being unable to reason.

Consistency is relative to assumptions

Hilbert's geometric approach studies models and dependencies among axioms. If a geometry can be interpreted inside an accepted theory of real numbers, a contradiction in that geometry would produce a contradiction in the background theory. That is a relative consistency result. It does not justify the background assumptions from nowhere. Discussion of the geometry project.

Gödel's first incompleteness theorem, with later refinements, applies to consistent effectively axiomatized theories containing sufficient arithmetic. Such a theory is not syntactically complete. The second theorem, under its required conditions, blocks an internal proof of the theory's standard consistency statement. It does not ban stronger theories from proving weaker theories consistent. Nor does a statement unprovable in one theory become unprovable in every theory. Precise restrictions.

For Hilbert's tenth problem, trying integer tuples can eventually find a solution when one exists. Failure after a million trials proves no general negative result. The Davis-Putnam-Robinson-Matiyasevich theorem led to the negative solution in 1970: no algorithm decides solvability for every integer-coefficient polynomial equation over the integers. Individual equations and restricted families remain solvable.

Mathematical legacy without a collapse story

Hilbert did not invent existence proofs or all mathematical rigor. His basis theorem concerns polynomial rings over suitable coefficient rings, conventionally stated as: if R is a commutative Noetherian ring, then R[x] is Noetherian. Omitting this hypothesis makes the claim false for arbitrary coefficient rings. Modern algebra statement. A Hilbert space is a complete inner-product space; “infinite-dimensional vector space” alone omits both the inner product and completeness.

His research program encountered profound limits while proof theory continued to develop. The useful lesson is methodological: state a claim exactly enough that a proof, countermodel or impossibility theorem can resolve it. Avoid turning incompleteness into a story that nobody can ever know anything with certainty.

Exercises

  1. Construct and check a proof of 22 in the toy integer system. Explain why the backward procedure terminates and why it does not require trying every possible proof.
  2. Suppose a theory has effectively checkable proofs, is consistent and is syntactically complete. Describe an algorithm deciding whether a sentence is a theorem. State exactly where each assumption is used. What breaks if completeness is removed?
  3. Compare these statements: “I searched all pairs with absolute value at most 100 without finding a solution to x² + y² = 3” and “This equation has no integer solution.” Supply a proof of the second statement using residues modulo 4. Explain why this does not solve Hilbert's tenth problem.
Compare your reasoning with the worked solutions
  1. Backward division gives 22, 11, 5, 2, 1. Reversing yields 1, 2, 5, 11, 22. The rules are doubling, doubling-plus-one, doubling-plus-one, then doubling. Every backward step decreases n while retaining a positive integer until it reaches 1. The parity of each child determines the required rule, so the rules themselves expose a terminating search strategy for this restricted system.
  2. Enumerate finite candidate proofs in increasing encoded length, checking each and comparing its conclusion with A and with not-A. Effective checking makes each stage finite. Completeness guarantees that at least one desired proof exists, so enumeration eventually finds it. Consistency prevents both conclusions being theorems and makes the resulting yes/no classification unambiguous. Without completeness, both searches may continue forever for an independent sentence. A failure to find a proof is not a proof of its absence.
  3. An integer square is congruent to 0 or 1 modulo 4. A sum of two squares is therefore congruent to 0, 1 or 2, never 3. Thus equality with 3 is impossible for all integers, including those outside the searched range. The argument works because this equation has a useful modular obstruction. Other unsolvable equations need different arguments, and the existence of many successful special methods does not produce an algorithm guaranteed to settle every polynomial equation.

Sources and further study