Bar induction

Bar induction is a reasoning principle used in intuitionistic mathematics, introduced by L. E. J. Brouwer. Bar induction's main use is the intuitionistic derivation of the fan theorem, a key result used in the derivation of the uniform continuity theorem. Bar induction is a reasoning principle used in intuitionistic mathematics, introduced by L. E. J. Brouwer. Bar induction's main use is the intuitionistic derivation of the fan theorem, a key result used in the derivation of the uniform continuity theorem. It is also useful in giving constructive alternatives to other classical results. The goal of the principle is to prove properties for all infinite sequences of natural numbers (called choice sequences in intuitionistic terminology), by inductively reducing them to properties of finite lists. Bar induction can also be used to prove properties about all choice sequences in a spread (a special kind of set). Given a choice sequence x 0 , x 1 , x 2 , x 3 , … {displaystyle x_{0},x_{1},x_{2},x_{3},ldots } , any finite sequence of elements x 0 , x 1 , x 2 , x 3 , … , x i {displaystyle x_{0},x_{1},x_{2},x_{3},ldots ,x_{i}} of this sequence is called an initial segment of this choice sequence.