Title: Comparison and analysis of constructive set theories
Other Titles: Vergleich und Analyse konstruktiver Mengenlehren
Language: English
Authors: Freiman, Robert 
Qualification level: Diploma
Advisor: Fermüller, Christian 
Issue Date: 2020
Number of Pages: 131
Qualification level: Diploma
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.
Keywords: constructivism; set theory; intuitionistic logic
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-133343
Library ID: AC15546935
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Page view(s)

checked on Jul 11, 2021


checked on Jul 11, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.