From constructive mathematics to computable analysis via the realizability interpretation
Peter Lietz · Technischen Universität Darmstadt · 2008
Constructive mathematics is mathematics without the use of the principle of the excluded middle. There exists a wide array of models of constructive logic. One particular interpretation of constructive mathematics is the realizability interpretation. It is utilized as a metamathematical tool in order to derive admissible rules of deduction for systems of constructive logic or to demonstrate the equiconsistency of extensions of constructive logic. In this thesis, we employ various realizability models in order to logically separate several statements about continuity in constructive mathematics. A trademark of some constructive formalisms is predicativity. Predicative logic does not allow the definition of a set by quantifying over a collection of sets that the set to be defined is a member of. Starting from realizability models over a typed version of partial combinatory algebras we are able to show that the ensuing models provide the features necessary in order to interpret impredicative logics and type theories if and only if the underlying typed partial combinatory algebra is equivalent to an untyped pca. It is an ongoing theme in this thesis to switch between the worlds of classical and constructive mathematics and to try and use constructive logic as a method in order to obtain results of interest also for the classically minded mathematician. A classical mathematician can see the value of a solution algorithm as opposed to an abstract proof of the existence of a solution, but he or she would not insist on a constructive correctness proof for that algorithm. We introduce a class of formulae which is supposed to capture this pragmatic point of view. The class is defined in such a way that existence statements have a strong status, yet the correctness of an operation need only be proved classically. Moreover, this theory contains only classically true formulae. We pose the axiomatization of this class of formulae as an open problem and provide partial results. Like ordinary recursion theory, computable analysis is a branch of classical mathematics. It applies the concept of computability to entities of analysis by equipping them with a generalization of Gödelizations called representations. Representations can be organized into a realizability category with rich logical properties. In this way, natural representations of spaces can be found by categorically interpreting the description of the underlying set of a space. Computability and non-computability results can be and are shown on an abstract, logical level. Finally, we turn to another application of realizability models, the field of strong normalization proofs for type theoretic frameworks. We will argue why we think that the modified realizability topos is not suited for this purpose and propose an alternative.