Mathematical Sciences: Convergence Properties of Hilbert's Substitution Method

代换方法是由Hilbert(1930)提出的一种求数论函数方程组有限函数解的逐次逼近方法，这种方法是由形式系统中的证明导出的。收敛，即此方法的终止，产生组合恒等式的有限证明和可证明的Sigma-0-1公式的数值实现。Von Neumann(1927)和Ackermann(1940)分别针对无限量词归纳和一阶算术系统讨论了收敛问题。这个待分析的问题一直悬而未决，直到最近，Mints(1990)才解决了这个问题。Mints现在打算研究问题仍然悬而未决的其他系统的收敛问题，包括：1)谓词分析和预测可约系统，2)证明论序数已知的更强分析子系统，3)类型理论，4)具有选择公理的完全分析，5)Zermelo集合论和可能的更强系统。证明论考察的是有关证据的问题，这些问题偏向于证据的正确性。人们理解并认为正确是理所当然的。例如，需要什么公理，是一个系统的所有公理，还是只需要一个适当的子集？事实上，某些公理在这样的研究中尤其关键，使用所谓的选择公理的必要性被认为是特别有趣的，它涉及比所有正整数集1，2，3，……的无穷大阶。其他强大的无穷大公理也常常扮演这一角色。在另一个方向上，人们可以要求一个证明某物或另一物存在的证据，无论它是否提供了构建所显示的存在的事物的明确配方。这样做的证据被称为“建设性的”，而其他的则被称为“非建设性的”。证据理论中一个特别耐人寻味的部分涉及到非建构性证明是否可以以某种自动的方式重新编写为建构性证明。事实证明，答案取决于正在研究的理论。这位研究人员已经证明，一种被称为希尔伯特替换法的方法可以用来将某种分析公式中的任何非建构性证明转化为建构性证明，本质上是通过转动曲柄来实现的，他想知道他给出的论点是否可以适用于其他某些数学系统，以获得类似的结果。

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.