Comparison and analysis of constructive set theories

Abstract

Since the discovery of the Curry-Howard-correspondence we know of the deep-lying connections between computability and provability in intuitionistic logic. Hence, constructive mathematics, being based on intuitionistic logic, promises to be a fruitful tool in investigating the computational content of classical mathematics with potential applications in the areas of automated deduction and automated theorem proving. The objective of this thesis is to present and compare different approaches to constructive set theories in a comprehensible and self-contained fashion and thereby demonstrate its potential for applications in automated deduction and automated theorem proving. The particular significance placed here on set theory is due to its historically proven relevance in providing the very foundation of mathematics. The main theories discussed in the thesis are Brouwerian set theory, the axiomatic Zermelo-Fraenkel-style set theories IZF and CZF and Martin-Löfs set theory ML. In a first step, the theories and their axiomatizations are motivated from the constructive standpoint. Some basic results are inferred to get used to reasoning and limitations within the respective system. The broadest investigation, however, is conducted by means of metamathematical analysis. Metamathematical analysis of constructive Zermelo-Fraenkel set theories is executed by two semantical tools: Realizability and topological semantics. The former builds directly on notions from computability theory and thus allows for an investigation of metamathematical properties that are constructively de-sirable. A proof using topological semantics is presented to obtain an independence proof of the principle of decidable bar induction from a variant of Brouwers mathematics formalized within IZF. Finally, a meaning-persevering interpretation of CZF into ML a theory that is considered to give a constructively clear and well-justified notions of sets is discussed. This makes CZF not only especially well-suited for mathematical practice, but also vindicates its constructive nature and makes it a promising starting point for applications.