An inductive way of reasoning, used in intuitionistic mathematics (cf.
Intuitionism),
which may be described as follows. Let certain properties
and
be defined on finite tuples (cf.
Tuple)
of natural integers, such that 1) the property
is decidable, i.e. it is possible to effectively find
out whether it is fulfilled on any tuple
or not; 2) for any choice sequence
it is possible to find a tuple of the form
for which
is fulfilled. Moreover, if 2) is fulfilled, one says that
"bars"
the empty tuple
(hence the name); 3) for any tuple
of natural integers, if
,
then
(the so-called
basis of the bar induction);
and 4) if
is a tuple such that for any natural number
one has
,
then
;
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
.
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).
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: