Independence and conservativity results for intuitionistic set theory

There are two main parts to this thesis. The first part will deal with some independence results. In 1979, Lifschitz in [13] introduced a realizability interpretation for Heyting's arithmetic, HA, that could differentiate between Church's thesis with uniqueness condition, CT0!, and the gen...

Full description

Bibliographic Details
Main Author: Chen, Ray-Ming
Other Authors: Rathjen, M. ; Wainer, S.
Published: University of Leeds 2010
Subjects:
510
Online Access:http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.530616
id ndltd-bl.uk-oai-ethos.bl.uk-530616
record_format oai_dc
spelling ndltd-bl.uk-oai-ethos.bl.uk-5306162017-10-04T03:32:47ZIndependence and conservativity results for intuitionistic set theoryChen, Ray-MingRathjen, M. ; Wainer, S.2010There are two main parts to this thesis. The first part will deal with some independence results. In 1979, Lifschitz in [13] introduced a realizability interpretation for Heyting's arithmetic, HA, that could differentiate between Church's thesis with uniqueness condition, CT0!, and the general form of Church's thesis, CT0. The objective here is to extend Lifschitz' realizability to intuitionistic Zermelo-Fraenkel set theory with two sorts, IZFN. In addition to separating Church's thesis with uniqueness condition from its general form in intuitionistic set theory, I also obtain several interesting corollaries. The interpretation repudiates a weak form of countable choice, ACN2, asserting that every countable family of inhabited subsets of {0,1} has a choice function. The second part will be concerned with Constructive Zermelo-Fraenkel Set Theory and other intuitionistic set theories augmented by various principles, notably choice principles. It will be shown that the addition of these (choice) principles does not change the stock of provable arithmetical theorems. This type of conservativity result has its roots in a theorem of Goodman[9] who showed that Heyting arithmetic in all nite types augmented by the axiom of choice for all levels is conservative over HA. The technique I employ here to obtain such results for intuitionistic set theories, however, owes a lot to a paper by Beeson published in 1979. In [2] he showed how to construe Goodman's Theorem as the composition of two interpretations, namely relativized realizability and forcing. In this thesis, I adopt the same approach and employ it to a plethora of intuitionistic set theories.510University of Leedshttp://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.530616http://etheses.whiterose.ac.uk/1439/Electronic Thesis or Dissertation
collection NDLTD
sources NDLTD
topic 510
spellingShingle 510
Chen, Ray-Ming
Independence and conservativity results for intuitionistic set theory
description There are two main parts to this thesis. The first part will deal with some independence results. In 1979, Lifschitz in [13] introduced a realizability interpretation for Heyting's arithmetic, HA, that could differentiate between Church's thesis with uniqueness condition, CT0!, and the general form of Church's thesis, CT0. The objective here is to extend Lifschitz' realizability to intuitionistic Zermelo-Fraenkel set theory with two sorts, IZFN. In addition to separating Church's thesis with uniqueness condition from its general form in intuitionistic set theory, I also obtain several interesting corollaries. The interpretation repudiates a weak form of countable choice, ACN2, asserting that every countable family of inhabited subsets of {0,1} has a choice function. The second part will be concerned with Constructive Zermelo-Fraenkel Set Theory and other intuitionistic set theories augmented by various principles, notably choice principles. It will be shown that the addition of these (choice) principles does not change the stock of provable arithmetical theorems. This type of conservativity result has its roots in a theorem of Goodman[9] who showed that Heyting arithmetic in all nite types augmented by the axiom of choice for all levels is conservative over HA. The technique I employ here to obtain such results for intuitionistic set theories, however, owes a lot to a paper by Beeson published in 1979. In [2] he showed how to construe Goodman's Theorem as the composition of two interpretations, namely relativized realizability and forcing. In this thesis, I adopt the same approach and employ it to a plethora of intuitionistic set theories.
author2 Rathjen, M. ; Wainer, S.
author_facet Rathjen, M. ; Wainer, S.
Chen, Ray-Ming
author Chen, Ray-Ming
author_sort Chen, Ray-Ming
title Independence and conservativity results for intuitionistic set theory
title_short Independence and conservativity results for intuitionistic set theory
title_full Independence and conservativity results for intuitionistic set theory
title_fullStr Independence and conservativity results for intuitionistic set theory
title_full_unstemmed Independence and conservativity results for intuitionistic set theory
title_sort independence and conservativity results for intuitionistic set theory
publisher University of Leeds
publishDate 2010
url http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.530616
work_keys_str_mv AT chenrayming independenceandconservativityresultsforintuitionisticsettheory
_version_ 1718544667198357504