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. 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 , any finite sequence of elements of this sequence is called an initial segment of this choice sequence. There are three forms of bar induction currently in the literature, each one places certain restrictions on a pair of predicates and the key differences are highlighted using bold font. Given two predicates and on finite sequences of natural numbers such that all of the following conditions hold: every choice sequence contains at least one initial segment satisfying at some point (this is expressed by saying that is a bar); is decidable (i.e. our bar is decidable); every finite sequence satisfying also satisfies (so holds for every choice sequence beginning with the aforementioned finite sequence); if all extensions of a finite sequence by one element satisfy , then that finite sequence also satisfies (this is sometimes referred to as being upward hereditary); then we can conclude that holds for the empty sequence (i.e. A holds for all choice sequences starting with the empty sequence). This principle of bar induction is favoured in the works of, A. S. Troelstra, S. C. Kleene and Albert Dragalin. Given two predicates and on finite sequences of natural numbers such that all of the following conditions hold: every choice sequence contains a unique initial segment satisfying at some point (i.e.