Complexity in the Constructive and Intuitionistic Theory of Reals

拟议的项目包括对现实的建设性和直观理论的主题进行研究。研究的重点是真实的闭域的构造性理论和实域的各种拓扑模型。特别强调将放在调查中的理论的复杂性和这些理论，包括可定义性和公理化的问题的可判定的片段。关于模型的结果有助于找到语言的片段，其真理在真实的数字系统（如毕晓普定义的）可以确定，这一事实是可证明的建设性，或在一个直观的元理论。利用可判定性的结果，下一步是寻找真实的闭序域的构造性和/或直觉理论的可判定片段的一阶公理，并分析这些片段中可定义的元素和集合的结构。然后，工作将转向方向发起的斯考克罗夫特：对模型理论的研究相对强度的公理化建设性的一阶理论的现实。 连接到最近的事态发展有关的决策过程的S2 S和相关的博弈论的方法，并发编程进行调查，以及之间的关系的理论的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.