Abstract

Brouwer introduced a principle called the bar induction to develop his intuitionism including the theory of choice sequences. In order to justify the bar induction, Brouwer supposed a fundamental assumption on the range of canonical proofs. The assumption, however, has been controversial and discussed in papers. Especially, we have to explain the reason why Brouwer introduced the fundamental assumption. In this paper, we point out that Brouwer’s argument is very close to the method of the Ω-rule due to Buchholz, which has been a main tool in infinitary proof theory since 1970’s. Based on this observation, we explain why Brouwer needed the fundamental assumption.