Metamathematical interpretation of the fan theorem
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part V, Tome 32 (1972), pp. 45-52

Voir la notice de l'article provenant de la source Math-Net.Ru

Brouwer's fan theorem states that if (a) a function $f$ assigns a natural number to every element of a given fan then (b) its values depend on $N$ initial members of an argument only, where $N$ is sufficiently large. Elements are treated there as choise sequences. If one treats them as recursive functions then the statement “(a) implies (b)” is known to be false. However we prove that if (a) is provable in a certain formal system of constructive analysis which is correct with respect to the interpretation of sequences as recursive functions then (b) holds under the same interpretation. The system is obtained from Kleene–Vesley system of intuitionistic analysis by deleting bar theorem and Brouwer principle and adding Markov's scheme.
@article{ZNSL_1972_32_a6,
     author = {V. A. Lifshits},
     title = {Metamathematical interpretation of the fan theorem},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {45--52},
     publisher = {mathdoc},
     volume = {32},
     year = {1972},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1972_32_a6/}
}
TY  - JOUR
AU  - V. A. Lifshits
TI  - Metamathematical interpretation of the fan theorem
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1972
SP  - 45
EP  - 52
VL  - 32
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1972_32_a6/
LA  - ru
ID  - ZNSL_1972_32_a6
ER  - 
%0 Journal Article
%A V. A. Lifshits
%T Metamathematical interpretation of the fan theorem
%J Zapiski Nauchnykh Seminarov POMI
%D 1972
%P 45-52
%V 32
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZNSL_1972_32_a6/
%G ru
%F ZNSL_1972_32_a6
V. A. Lifshits. Metamathematical interpretation of the fan theorem. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part V, Tome 32 (1972), pp. 45-52. http://geodesic.mathdoc.fr/item/ZNSL_1972_32_a6/