View source for Bar induction

An inductive way of reasoning, used in intuitionistic mathematics (cf. [[Intuitionism|Intuitionism]]), which may be described as follows. Let certain properties <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152201.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152202.png" /> be defined on finite tuples (cf. [[Tuple|Tuple]]) of natural integers, such that 1) the property <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152203.png" /> is decidable, i.e. it is possible to effectively find out whether it is fulfilled on any tuple <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152204.png" /> or not; 2) for any choice sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152205.png" /> it is possible to find a tuple of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152206.png" /> for which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152207.png" /> is fulfilled. Moreover, if 2) is fulfilled, one says that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152208.png" />  "bars"  the empty tuple <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b0152209.png" /> (hence the name); 3) for any tuple <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522010.png" /> of natural integers, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522011.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522012.png" /> (the so-called basis of the bar induction); and 4) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522013.png" /> is a tuple such that for any natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522014.png" /> one has <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522015.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522016.png" />; this property is known as the step of the bar induction.

If the conditions 1) through 4) above are met, one can deduce from the principle of bar induction that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522017.png" />.

The use of bar induction was proposed by L.E.J. Brouwer as an intuitionistic method of reasoning which indicates that the collection of free choice sequences is incomplete and to some extent uncountable. It was demonstrated, in particular, by S.C. Kleene and, independently, by A.A. Markov that it follows from the principle of bar induction (in fact, even from a corollary of bar induction, the fan theorem) that not all choice sequences are recursive (cf. [[Fan|Fan]]).

The forms of bar induction which one started to utilize in the foundations of mathematics in the 1960's do not deal with tuples of natural numbers, but rather with tuples of more complex objects, such as tuples of choice sequences.

Bar induction can be written down in the language of formal intuitionistic mathematical analysis as follows:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522018.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522019.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b015/b015220/b01522020.png" /></td> </tr></table>

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,   R.E. Vesley,   "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland  (1965)</TD></TR></table>



====Comments====


====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  M.A.E. Dummett,   "Elements of intuitionism" , Clarendon Press  (1977)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  A.S. Troelstra,   "Choice sequences" , Clarendon Press  (1977)</TD></TR></table>