Proof theory
The formalization of mathematical proof by means of a logistic system (q. v.) makes possible an objective theory of proofs and provability, in which proofs are treated as concrete manipulations of formulas (and no use is made of meanings of formulas). This is Hilbert’s proof theory, or metamathematics. p A central problem of proof theory, according to Hilbert, is the proof of consistency of logistic systems adequate to mathematics or substantial parts of mathematics. — A logistic system is said to be consistent, relatively to a particular notation in the system called negation, if there is no formula A such that both A and the negation of A are provable (i.e., are theorems). The systems with which Hilbert deals, and the notations in them which he wishes to call negation, are such that, if a formula A and its negation were once proved, every propositional formula could be proved; hence he is able to formulate the consistency by snying that a particular formula (e.g., ~[0 = 0]) is not provable.
A consistency proof evidently loses much of its significance unless the methods employed in the proof are in some sense less than, or less dubitable than, the methods of proof which the logistic system is intended to formalize. Hilbert required that the methods employed in a consistency proof should be finitary — a condition more stringent than that of intuitionistic acceptability. See Intuitionism (mathematical).
Gdel’s theorems (see Logic, formal, 6) are a difficulty for the Hilbert program because they show that the methods employed in a consistency proof must also be in some sense more than those which the logistic system formalizes. Godel himself remarks that the difficulty may not be insuperable.
Other problems of proof theory are the decision problem, and the problem of proving completeness (in one of various senses) for a logistic system. Cf. Logic, formal, 1, 3. — A.C.
Hilbert and Bernays,
Grundlagen der Mathematik, vol. 1, Berlin, 1934, and vol. 2, Berlin. 1939.
P. Bernays,
Sur le platonisme dans les mathematiques, and
Quelques points essentiels de la metamathematique, l’Enseignement Mathematique, vol. 34 (1935), pp. 52-95.
W. Ackermann,
Zur Widerspruchsfreiheitt der Zahlentheorie, Mathematische Annalen, vol. 117 (1940), pp 162-194.