|
|||||
|
|
A note on Bar Induction in Constructive Set Theory |
|
| Authors: | Michael Rathjen |
| 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. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim) |
| Keywords: | Constructive set theory Brouwerian principles Bar Induction proof‐theoretic strength |