A Constructive Version of the Lusin Separation Theorem

  • Peter Aczel
Part of the Synthese Library book series (SYLI, volume 341)


I state and prove a constructive version of the Lusin Separation Theorem. The classical statement of the theorem is that disjoint analytic sets are Borel separable. The definitions and results are carried out in the axiom system CZF for constructive set theory.


Tree Representation Countable Union Main Lemma Separation Theorem Baire Space 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. Aczel and M. Rathjen, Notes on Constructive Set Theory, Mittag-Leffler Technical Report No. 40, 2000/2001, (2001).Google Scholar
  2. 2.
    L.E.J. Brouwer, Über Definitionsbereiche von Funktionen, Math. Ann. 95, 453–472, (1927).CrossRefMathSciNetGoogle Scholar
  3. 3.
    J. van Heijenoort, ed. From Frege to Gödel. A Sourcebook in Mathematical Logic 1879–1931, Harvard University Press, Cambridge Mass., Reprinted (1970).Google Scholar
  4. 4.
    N. Lusin, Sur les ensembles analytiques, Fund. Math. 10, 1–95, (1927).zbMATHGoogle Scholar
  5. 5.
    N. Lusin, Leçons sur les ensembles analytiques et leurs applications, Collection de monographies sur la theorie des fonctions, Paris, Gauthiers-Villars (1930).Google Scholar
  6. 6.
    N. Lusin and W. Sierpinski, Sur quelques proprietés des ensembles (A), Bull. Int. Acad. Sci. Cracovie, Série A; Sciences Mathématiques, 35–48, (1918).Google Scholar
  7. 7.
    N. Lusin and W. Sierpinski, Sur un ensemble non mesurable B, Journal de Mathématiques, 9e serie, 2, 53–72, (1923).Google Scholar
  8. 8.
    P. Martin-Löf, Notes on Constructive Mathematics, Almqvist & Wiksell, Stockholm, (1970).Google Scholar
  9. 9.
    Y. Moschovakis, Descriptive Set Theory, North Holland, Amsterdam, (1980).zbMATHGoogle Scholar
  10. 10.
    M. Suslin, Sur une definition des ensembles mesurable B sans nombres transfinis, Comptes Rendus Acad. Sci., Paris 164, 88–91, (1917).Google Scholar
  11. 11.
    W. Veldman, Investigations in Intuitionistic Hierarchy Theory, Ph.D. thesis, Katholieke Universiteit, Nijmegen, (1981).Google Scholar
  12. 12.
    W. Veldman, The Borel Hierarchy and the Projective Hierarchy in Intuitionistic Mathematics, Report No. 0103, Department of Mathematics, University of Nijmegen, (March 2001), (revised version available, June 2006).Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  • Peter Aczel
    • 1
  1. 1.Departments of Mathematics and Computer ScienceManchester UniversityManchesterUK

Personalised recommendations