Binary Refinement Implies Discrete Exponentiation

Studia Logica 84 (3):361-368 (2006)
  Copy   BIBTEX


Working in the weakening of constructive Zermelo-Fraenkel set theory in which the subset collection scheme is omitted, we show that the binary refinement principle implies all the instances of the exponentiation axiom in which the basis is a discrete set. In particular binary refinement implies that the class of detachable subsets of a set form a set. Binary refinement was originally extracted from the fullness axiom, an equivalent of subset collection, as a principle that was sufficient to prove that the Dedekind reals form a set. Here we show that the Cauchy reals also form a set. More generally, binary refinement ensures that one remains in the realm of sets when one starts from discrete sets and one applies the operations of exponentiation and binary product a finite number of times.



    Upload a copy of this work     Papers currently archived: 93,098

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

149 (#130,397)

6 months
14 (#200,872)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Laura Crosilla
Università degli Studi di Firenze
Peter Schuster
University of Leeds

Citations of this work

Refinement is equivalent to Fullness.Albert Ziegler - 2010 - Mathematical Logic Quarterly 56 (6):666-669.

Add more citations