On Choice Principles and Fan Theorems

: 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. Key Words: constructive mathematics, fan theorem, countable choice Category: G.0 In this paper, we work in Bishop-style constructive mathematics [Bishop and Bridges 1985], that is informal mathematics using only intuitionistic logic. However, we will state explicitly when choice principles are used. This way our results not only hold in the usual varieties of constructive mathematics such as Brouwer's intuitionis...

• Type: Journal
• Year: 2010
• Where: JUCS
• Authors: Hannes Diener, Peter Schuster
• Keywords: Constructive Mathematics, Countable Binary Choice, Fan Theorem, JUCS 2010