Complexity in the Constructive and Intuitionistic Theory of 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.