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.