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 (i.e. our bar is monotonic); 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. 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 schema of bar induction was originally given as a theorem by Brouwer (1975) containing no "extra" restriction on under the name The Bar Theorem. 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. 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. Relations to other fields In classical reverse mathematics, "bar induction" () denotes the related principle stating that if a relation is a well-order, then we have the schema of transfinite induction over for arbitrary formulas. References L. E. J. Brouwer Brouwer, L. E. J. Collected Works, Vol. I, Amsterdam: North-Holland (1975). Michael Dummett, Elements of intuitionism, Clarendon Press (1977) S. C. Kleene, R. E. Vesley, The foundations of intuitionistic mathematics: especially in relation to recursive functions, North-Holland (1965) Michael Rathjen, The role of parameters in bar rule and bar induction, Journal of Symbolic Logic 56 (1991), no. 2, pp. 715–730. A. S. Troelstra, Choice sequences, Clarendon Press (1977) A. S. Troelstra and Dirk van Dalen, Constructivism in Mathematics, Studies in Logic and the Foundations of Mathematics'', Elsevier (1988) Constructivism (mathematics) Mathematical induction