A note on Bar Induction in Constructive Set Theory

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

Abstract

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

Categories

Keywords

Reprint years

DOI

10.1002/malq.200510030

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

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

Through your library

My notes

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.
A note on the theory of positive induction, $${{\rm ID}^*_1}$$.Bahareh Afshari & Michael Rathjen - 2010 - Archive for Mathematical Logic 49 (2):275-281.
The natural numbers in constructive set theory.Michael Rathjen - 2008 - Mathematical Logic Quarterly 54 (1):83-97.
Some theories with positive induction of ordinal strength ϕω.Gerhard Jäger & Thomas Strahm - 1996 - Journal of Symbolic Logic 61 (3):818-842.
The role of parameters in bar rule and bar induction.Michael Rathjen - 1991 - Journal of Symbolic Logic 56 (2):715-730.
Some Theories with Positive Induction of Ordinal Strength $varphiomega 0$.Gerhard Jager & Thomas Strahm - 1996 - Journal of Symbolic Logic 61 (3):818-842.
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 proof-theoretic strength of monotone induction in explicit mathematics.Thomas Glaß, Michael Rathjen & Andreas Schlüter - 1997 - Annals of Pure and Applied Logic 85 (1):1-46.
On the constructive Dedekind reals.Robert S. Lubarsky & Michael Rathjen - 2008 - Logic and Analysis 1 (2):131-152.
A material dissolution of the problem of induction.John D. Norton - 2014 - Synthese 191 (4):1-20.
The proof theory of classical and constructive inductive definitions. A 40 year saga, 1968-2008.Solomon Feferman - unknown
The strength of Martin-Löf type theory with a superuniverse. Part II.Michael Rathjen - 2001 - Archive for Mathematical Logic 40 (3):207-233.
Approximate Truth vs. Empirical Adequacy.Seungbae Park - 2014 - Epistemologia 37 (1):106-118.
The strength of Martin-Löf type theory with a superuniverse. Part I.Michael Rathjen - 2000 - Archive for Mathematical Logic 39 (1):1-39.

Analytics

Added to PP
2013-12-01

Downloads
42 (#370,011)

6 months
8 (#342,364)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Michael Rathjen
University of Leeds

Citations of this work

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