A decomposition of Brouwer’s fan theorem
Josef Berger · Journal of Logic and Analysis · 2009
We introduce axioms L FAN and C FAN , where the former follows from the law of excluded middle and the latter follows from the axiom of countable choice.Then we show that Brouwer's fan theorem is constructively equivalent to L FAN + C FAN .This decomposition of the fan theorem into a logical axiom and a function existence axiom contributes to the programme of constructive reverse mathematics.