The relation reflection scheme

Research output: Contribution to journalArticle

  • 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
Pages (from-to)5-11
Number of pages6
JournalMathematical Logic Quarterly
Volume54
Issue number1
DOIs
Publication statusPublished - Feb 2008