A Formalization of Brouwer's Argument for Bar Induction

摘要

Brouwer was a founder of intuitionism and he developed intuitionistic mathematics in 1920's. In particular, he proved the uniform continuity theorem using the fan theorem in 1927, which was derived from a stronger theorem called bar induction. For this principle Brouwer gave a justification which was an important source of BHK-interpretation, but it depends on an assumption which we call "the fundamental assumption" (FA). Since FA was neither explained or justified, many people have thought that Brouwer's argument is highly controversial. In this paper, we propose a way of formalizing Brouwer's argument using a method in infinitary proof theory. Also, based on our formalization, we give an explanation and justification of FA from the viewpoint of the practice of intuitionistic mathematics.