Complexity in the Constructive and Intuitionistic Theory of Reals

拟议的项目包括对真实的建构性和直觉性理论的主题的研究。研究将集中在实闭域的构造理论和实的各种拓扑模型上。将特别强调正在调查的理论的复杂性和这些理论的可判定的片断，包括可定义性和公理化问题。关于模型的结果有助于找到语言的片段，其在实数系统(如毕晓普所定义的)中的真实性可以被确定，并且这一事实是可以建设性地证明的，或者在直观的元理论中。利用可判断性结果，下一步是寻找实闭序域的构造性和/或直觉性理论的可判定片段的一阶公理，并分析在这些片段中可定义的元素和集合的结构。然后，这项工作将转向斯考克罗夫特开创的方向：对实数的建设性的一阶理论的公理化的相对强度的模型论研究。将研究S2S决策过程的最新发展与并发编程的相关博弈论方法的联系，以及Heyting代数理论与用于直观分析的相应模型的性质之间的关系。在大多数情况下，计算涉及实数。该提案的目的是从建设性的角度来研究实数的结构--例如，带有加法和乘法的(可能是无限的)小数。这意味着，例如，仅证明实数或具有特定性质的从实数到实数的函数的存在是不够的，需要一种方法来找到所述函数的数目或值的任意近似。这种实用方法的第一步是找到建设性的证据，证明“这样或那样的性质是否有一个数字/函数？”可以回答。然后从证明本身来看，如果答案是肯定的，就可以得到上述方法。解决这一问题的一种方法是通过观察各种真实的建设性/直觉主义理论模型，这是本提案的起点。然后，结果有助于在有这样的方法的情况下找到方法，并且还可以找到通常没有这样的方法的问题。

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.