Bar induction is a reasoning principle used in intuitionistic mathematics, introduced by L.E.J. Brouwer. In the Philosophy of mathematics, intuitionism, or neointuitionism (opposed to Preintuitionism) is an approach to Mathematics as the constructive Luitzen Egbertus Jan Brouwer ɛxˈbɛʁtəs jɑn ˈbʁʌuəʁ ( February 27 1881, Overschie – December 2 1966, Blaricum It is useful in giving constructive versions of classical results. Classical logic identifies a class of Formal logics that have been most intensively studied and most widely used 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, assume 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 lists by one element satisfy S, then that list also satisfies S.
Then we can conclude that S holds for the empty list.
References
- S.C. Kleene, R. Stephen Cole Kleene ( January 5, 1909, Hartford Connecticut, USA &ndash January 25, 1994, Madison Wisconsin 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)
- Bar induction, article on Encyclopaedia of Mathematics, Edited by Michiel Hazewinkel, Springer-Verlag (2002)
Dapyx Software network: MP3 Explorer | Ebook Manager | Zenithic