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.
if all extensions of a finite sequence by one element satisfy, then that finite sequence also satisfies ;
then we can conclude that holds for the empty sequence. This principle of bar induction is favoured in the works of, A. S. Troelstra, S. C. Kleene and Dragalin.
Thin bar induction (BI''T'')
Given two predicates and on finite sequences of natural numbers such that all of the following conditions hold:
every choice sequence contains at least a unique initial segment satisfying at some point ;
every finite sequence satisfying also satisfies ;
if all extensions of a finite sequence by one element satisfy, then that finite sequence also satisfies ;
then we can conclude that holds for the empty sequence. This principle of bar induction is favoured in the works of Joan Moschovakis and is provably equivalent to decidable bar induction.
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;
once a finite sequence satisfies, then every possible extension of that finite sequence also satisfies ;
every finite sequence satisfying also satisfies ;
if all extensions of a finite sequence by one element satisfy, then that finite sequence also satisfies ;
then we can conclude that holds for the empty sequence. This principle of bar induction is used in the works of A. S. Troelstra, S. C. Kleene, Dragalin and Joan Moschovakis. It is usually derived from either thin bar induction or monotonic bar induction.
Relationships between these schemata and other information
The following results about these schemata can be intuitionistically proved: (The symbol "" is a "turnstile".
Unrestricted bar induction
An additional schemata of bar induction was originally given as a theorem by Brouwer containing no "extra" restriction on R under the name The BarTheorem. However, the proof for this theorem was erroneous, and unrestricted bar induction is not considered to be intuitionistically valid. The schema of unrestricted bar induction is given below for completeness. 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;
every finite sequence satisfying also satisfies ;
if all extensions of a finite sequence by one element satisfy, then that finite sequence also satisfies ;
then we can conclude that holds for the empty sequence.
