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.
| Original language | English |
|---|---|
| Pages (from-to) | 5-11 |
| Number of pages | 6 |
| Journal | Mathematical Logic Quarterly |
| Volume | 54 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - Feb 2008 |
Keywords
- Coinductive definitions
- Constructive set theory
- Dependent choices
Fingerprint
Dive into the research topics of 'The relation reflection scheme'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver