Bar induction

Bar induction is a reasoning principle used in intuitionistic mathematics, introduced by L.E.J. Brouwer. It is useful in giving constructive versions of classical results. It is based on an inductive argument.

The goal of the principle is to prove properties of infinite streams of natural numbers, called choice sequences in intuitionistic terminology, by inductively reducing them to decidable properties of finite lists.

Given two predicates R and S on finite lists of natural numbers such that the following conditions hold:

• R is decidable;
• every choice sequence has a finite prefix satisfying R (this is expressed by saying that R is a bar);
• every list satisfying R also satisfies S;
• if all extensions of a list by one element satisfy S, then that list also satisfies S;

then we can conclude that S holds for the empty list.

In classical reverse mathematics, "bar induction" (BI) denotes the related principle stating that if a relation R is a well-order, then we have the schema of transfinite induction over R for arbitrary formulas.

References

• S.C. Kleene, R.E. Vesley, The foundations of intuitionistic mathematics: especially in relation to recursive functions, North-Holland (1965)
• Michael Dummett, Elements of intuitionism, Clarendon Press (1977)
• A. S. Troelstra, Choice sequences, Clarendon Press (1977)
• Dragalin, A.G. (2001), "Bar induction", in Hazewinkel, Michiel, Encyclopedia of Mathematics, Springer, ISBN 978-1-55608-010-4
• Michael Rathjen, The role of parameters in bar rule and bar induction, Journal of Symbolic Logic 56 (1991), no. 2, pp. 715–730.