Mathematical Sciences: Convergence Properties of Hilbert's Substitution Method

数学科学：希尔伯特代换法的收敛性

• 批准号: 9206976
• 负责人: Solomon Feferman
• 金额: $ 6万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1992
• 资助国家: 美国
• 起止时间: 1992-09-01 至 1996-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9206976&HistoricalAwards=false
• 关键词: Mathematical; Sciences; Convergence; Properties; Hilbert

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.

希尔伯特（1930）提出了替代方法， 求有限函数逐次逼近法 数论函数方程组的解， 这是从形式系统中的证明中推导出来的。 收敛，即 这种方法的终止产生的有限性证明 组合恒等式和可证的数值实现 Sigma-zero-one-formulas. 收敛性问题的处理是： 冯·诺依曼（1927年）的无量词归纳法和阿克曼的 （1940）一阶算术系统。 的问题 分析一直保持开放，直到最近，当它被解决， Mints（1990年）。 明茨现在打算研究融合 对于问题仍然存在的其他系统， 包括以下几个方面：1）谓词性分析和谓词性 可约系统，2）更强的子系统的分析，其证明- 理论序数是已知的，3）类型的理论，4）充分 选择公理分析，5）策梅罗集理论和 更强大的系统。 证明理论研究的问题证明谎言一个 正确性的一面。 正确性被理解并被视为 理所当然 例如，需要什么公理， 是一个系统还是一个真子集 事实上，某些公理 在这些研究中，特别重要的是， 所谓的选择公理，涉及无穷大的顺序， 比所有正整数的集合1，2，3，...， 被认为特别有趣。 其他强公理 无限也常常扮演这个角色。 在另一个方向，人们可以 要求证明某事或其他事物存在， 提供了一个明确的配方， 存在. 这样做的证明被称为“建设性的”，其他的， “非建设性的。“证明理论中一个特别有趣的部分 关注的是一个非建设性的证据是否可以 自动地重新加工成一个有建设性的。 原来 答案取决于所研究的理论。 的 研究人员已经表明，一种称为希尔伯特的方法 替代方法可以用来把任何非构造性证明 在某种分析公式中， 基本上是转动曲柄，他想知道 他给出的论证可以适用于获得类似的结果， 其他数学系统。