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.
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).
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.
on finite sequences of natural numbers such that all of the following conditions hold: then we can conclude that
This principle of bar induction is favoured in the works of, A. S. Troelstra, S. C. Kleene and Albert Dragalin.
on finite sequences of natural numbers such that all of the following conditions hold: then we can conclude that
This principle of bar induction is favoured in the works of Joan Moschovakis and is (intuitionistically) provably equivalent to decidable bar induction.
on finite sequences of natural numbers such that all of the following conditions hold: then we can conclude that
This principle of bar induction is used in the works of A. S. Troelstra, S. C. Kleene, Dragalin and Joan Moschovakis.
The following results about these schemata can be intuitionistically proved: (The symbol "
An additional schema of bar induction was originally given as a theorem by Brouwer (1975) containing no "extra" restriction on
However, the proof for this theorem was erroneous, and unrestricted bar induction is not considered to be intuitionistically valid (see Dummett 1977 pp 94–104 for a summary of why this is so).
The schema of unrestricted bar induction is given below for completeness.
on finite sequences of natural numbers such that all of the following conditions hold: then we can conclude that
In classical reverse mathematics, "bar induction" (