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).

Definition

edit

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.

Decidable bar induction (BID)

edit

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.

Thin bar induction (BIT)

edit

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. our bar is thin);
  • 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 (intuitionistically) provably equivalent to decidable bar induction.

Monotonic bar induction (BIM)

edit

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   (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

edit

The following results about these schemata can be intuitionistically proved:

 

(The symbol " " is a "turnstile".)

Unrestricted bar induction

edit

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

edit

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

edit
  • L. E. J. Brouwer Brouwer, L. E. J. Collected Works, Vol. I, Amsterdam: North-Holland (1975).
  • Dragalin, Albert G. (2001) [1994], "Bar induction", Encyclopedia of Mathematics, EMS Press
  • 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)