JUCS - Journal of Universal Computer Science 16(18): 2556-2562, doi: 10.3217/jucs-016-18-2556
On Choice Principles and Fan Theorems
expand article infoHannes Diener, Peter Schuster§
‡ Universität Siegen, Siegen, Germany§ University of Leeds, Leeds, United Kingdom
Open Access
Abstract
Veldman proved that the contrapositive of countable binary choice is a theorem of full-fledged intuitionism, to which end he used a principle of continuous choice and the fan theorem. It has turned out that continuous choice is unnecessary in this context, and that a weak form of the fan theorem suffices which holds in the presence of countable choice. In particular, the contrapositive of countable binary choice is valid in Bishop-style constructive mathematics. We further discuss a generalisation of this result and link it to Ishihara's boundedness principle BD-N.
Keywords
constructive mathematics, fan theorem, countable choice