A note on Bar Induction in Constructive Set Theory

Mathematical Logic Quarterly 52 (3):253-258 (2006)
  Copy   BIBTEX


Bar Induction occupies a central place in Brouwerian mathematics. This note is concerned with the strength of Bar Induction on the basis of Constructive Zermelo-Fraenkel Set Theory, CZF. It is shown that CZF augmented by decidable Bar Induction proves the 1-consistency of CZF. This answers a question of P. Aczel who used Bar Induction to give a proof of the Lusin Separation Theorem in the constructive set theory CZF



    Upload a copy of this work     Papers currently archived: 92,075

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

The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
The natural numbers in constructive set theory.Michael Rathjen - 2008 - Mathematical Logic Quarterly 54 (1):83-97.
The role of parameters in bar rule and bar induction.Michael Rathjen - 1991 - Journal of Symbolic Logic 56 (2):715-730.
Variation on a theme of Schutte.D. Probst & G. Jager - 2004 - Mathematical Logic Quarterly 50 (3):258.
On the Strength of some Semi-Constructive Theories.Solomon Feferman - 2012 - In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation. De Gruyter. pp. 201-226.
On the constructive Dedekind reals.Robert S. Lubarsky & Michael Rathjen - 2008 - Logic and Analysis 1 (2):131-152.
Approximate Truth vs. Empirical Adequacy.Seungbae Park - 2014 - Epistemologia 37 (1):106-118.


Added to PP

45 (#353,828)

6 months
11 (#238,613)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Michael Rathjen
University of Leeds

Citations of this work

A Mathematical Model of Quantum Computer by Both Arithmetic and Set Theory.Vasil Penchev - 2020 - Information Theory and Research eJournal 1 (15):1-13.
The Quantum Strategy of Completeness: On the Self-Foundation of Mathematics.Vasil Penchev - 2020 - Cultural Anthropology eJournal (Elsevier: SSRN) 5 (136):1-12.
Representation and Reality by Language: How to make a home quantum computer?Vasil Penchev - 2020 - Philosophy of Science eJournal (Elsevier: SSRN) 13 (34):1-14.

Add more citations

References found in this work

Constructive set theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.
The foundations of intuitionistic mathematics.Stephen Cole Kleene - 1965 - Amsterdam,: North-Holland Pub. Co.. Edited by Richard Eugene Vesley.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Inaccessible set axioms may have little consistency strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.

View all 6 references / Add more references