Normalized naive set theory.
Erik Istre · UC Research Repository (University of Canterbury) · 2017
The broad goal of this thesis is the realization of a mathematically useful formal theory that contains a truth predicate, or as it's called in the literature, a "naive theory". To realize this goal, we explore the prospects for a naive set theory which can define a truth predicate. We first consider some of the promising developments in naive set theories using various non-classical logics that have come before. We look at two classes of non-classical logics: weak relevant logics [58, 59] and light linear logics [52]. Both of these have been used in the development of naive set theories. We review the naive set theories using these logics then discuss the strengths and weaknesses of these approaches. We then turn to the primary contribution of this thesis: the development of a robust naive set theory by accepting only normalized proofs, an idea first proposed by logician Dag Prawitz [25, 39]. It is demonstrated that this theory meets our need of logical strength in a system, while possessing more expressiveness in a foundational system than has come before. All of Heyting Arithmetic is recovered in this theory using a type-theoretic translation of the proof theory and other unique features of the theory are discussed and explored. It is further asserted that this theory is in fact the best case scenario for realizing informal proof in a formal system.