The relation reflection scheme

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Authors:
  • Peter Aczel

Abstract

We introduce a new axiom scheme for constructive set theory, the Relation Reflection Scheme (RRS). Each instance of this scheme is a theorem of the classical set theory ZF. In the constructive set theory CZF-, when the axiom scheme is combined with the axiom of Dependent Choices (DC), the result is equivalent to the scheme of Relative Dependent Choices (RDC). In contrast to RDC, the scheme RRS is preserved in Heyting-valued models of CZF- using set-generated frames. We give an application of the scheme to coinductive definitions of classes. © 2008 Wiley-VCH Verlag GmbH & Co. KGaA.

Bibliographical metadata

Original languageEnglish
Title of host publicationMathematical Logic Quarterly|Math. Logic Q.
PublisherJohn Wiley & Sons Ltd
Pages5-11
Number of pages6
Volume54
DOIs
Publication statusPublished - Feb 2008
EventWorkshop on Trends in Constructive Mathematics in Honor of the 60th Birthday of Douglas Bridges - Chiemsee Isl, GERMANY
Event duration: 19 Jun 200623 Jun 2006
http://www3.interscience.wiley.com/cgi-bin/fulltext/117902724/PDFSTART

Conference

ConferenceWorkshop on Trends in Constructive Mathematics in Honor of the 60th Birthday of Douglas Bridges
CityChiemsee Isl, GERMANY
Period19/06/0623/06/06
Internet address