Mathematical Sciences: Convergence Properties of Hilbert's Substitution Method

点击翻译按钮获取中文摘要

The substitution method was suggested by Hilbert (1930) as a successive approximation method for finding finite function solutions of a system of number-theoretic functional equations, which are derived from proofs in formal systems. Convergence, i.e. termination of this method produces finitistic proofs of combinatorial identities and numerical realizations of provable Sigma-zero-one-formulas. The problem of convergence was treated by von Neumann (1927) for quantifier-free induction and by Ackermann (1940) for the system of first-order arithmetic. The problem for analysis remained open until very recently, when it was settled by Mints (1990). Mints now intends to investigate convergence problems for other systems where the problem is still open, including the following: 1) predicative analysis and predicatively reducible systems, 2) stronger subsystems of analysis whose proof- theoretic ordinal is known, 3) the theory of types, 4) full analysis with the axiom of choice, 5) Zermelo set theory and possibly stronger systems. Proof theory examines questions about proofs that lie to one side of their correctness. Correctness is understood and taken for granted. For example, what axioms are required, all the axioms of a system or only a proper subset? Indeed, certain axioms are particularly critical in such studies, the necessity of employing the so-called Axiom of Choice, involving orders of infinity greater than that of the set of all the positive integers, 1, 2, 3, ..., being considered particularly interesting. Other strong axioms of infinity often play this role too. In another direction, one can ask of a proof that shows that something or other exists whether it provides an explicit recipe for constructing the thing shown to exist. Proofs which do are called "constructive," and others, "non-constructive." A particularly intriguing part of proof theory concerns itself with whether a non-constructive proof can be reworked in some automatic way into a constructive one. It turns out that the answer depends on the theory being studied. The investigator has shown that a method known as the Hilbert substitution method can be used to turn any non-constructive proof in a certain formulation of analysis into a constructive one by essentially turning a crank, and he would like to know if the argument he gave can be adapted to obtain the analogous result for certain other mathematical systems.