Complexity in the Constructive and Intuitionistic Theory of Reals

实数建构性直觉理论的复杂性

• 批准号: 9704337
• 负责人: Richard Shore
• 金额: --
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-07-01 至 2001-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9704337&HistoricalAwards=false
• 关键词: Complexity; Constructive; Intuitionistic; Theory; Reals

The proposed project includes research into topics in the constructive and intuitionistic theory of the reals. The research will focus on the constructive theory of real closed fields and on the various topological models of the reals. Particular emphasis will be placed on the complexity of the theories under investigation and on the decidable fragments of these theories including the questions of definability and axiomatizations. Results about the models help to find fragments of the language whose truth in the real number system (as defined by Bishop) can be decided, and this fact is provable constructively, or in an intuitionistic metatheory. Using the decidability results, the next step is to look for first order axioms for the decidable fragments of the constructive and/or intuitionistic theory of real closed ordered fields and to analyze the structure of elements and sets definable in these fragments. The work then would turn to the direction initiated by Scowcroft: towards the model-theoretic study of the relative strength of axiomatizations of a constructive first order theory of the reals. Connections to recent developments about the decision procedure of S2S and to related game-theoretic approach to concurrent programming are to be investigated, as well as the relationship between the theory of a Heyting algebra and the properties of the corresponding model for intuitionistic analysis. In most cases computations involve real numbers. The proposal's aim is to look at the structure of reals - for instance, (maybe infinite) decimal fractions with addition and multiplication - from a constructive point of view. This means, for example, that it is not enough to show that a real number, or a function from reals to reals with particular properties exists, a method is required to find arbitrary approximations of the number or of the values of the function in question. The first step in this practical approach is to find constructive proofs that questions like "is there a number/funct ion with such and such properties?" can be answered. Then from the proof itself, if the answer is yes, one may obtain the method mentioned above. One way to approach this problem is by looking at various models of the constructive/intuitionistic theory of the reals, and this is the starting point of the present proposal. The results then help to find the method when there is such, and also to find the problems where in general there is no such method.

拟议的项目包括对真实的建设性和直觉理论中的主题研究。该研究将重点介绍真实封闭领域的建设性理论以及真实的各种拓扑模型。特别重点将放在所研究理论的复杂性以及这些理论的可决定片段上，包括确定性和公理问题。有关模型的结果有助于找到语言的片段，即可以确定其实际数字系统中的真相（主教定义），并且可以建设性地证明这一事实，或者在直觉中的元情绪中得到证明。使用可决定性结果，下一步是寻找一阶公理，以解决实际封闭有序字段的建设性和/或直觉理论的可定义片段，并分析这些片段中可定义的元素结构和集合。然后，这项工作将转向Scowcroft启动的方向：迈向对实物建设性一阶理论的公理化强度相对强度的模型理论研究。 将研究有关S2S决策程序和与并发编程的相关游戏理论方法的最新发展的联系，以及Heyting代数的理论与直觉分析的相应模型的属性之间的关系。 在大多数情况下，计算涉及实数。该提案的目的是从建设性的角度来研究真实的结构，例如（也许是无限）的小数分数。例如，这意味着不足以证明存在一个真实的数字或具有特定属性的真实功能，需要一种方法来查找数字的任意近似值或函数值的值。这种实用方法的第一步是找到建设性的证据，即“有没有这样的属性的数字/函数吗？”之类的问题？可以回答。然后，从证明本身中，如果答案是肯定的，则可以获得上述方法。解决这个问题的一种方法是查看真实的建设性/直觉理论的各种模型，这是本提案的起点。然后，结果有助于找到该方法，并找到通常没有这种方法的问题。