The fundamental theorem of algebra: A constructive development without choice

Abstract

Is it reasonable to do constructive mathematics without the axiom of countable choice? Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are not compelling. The fundamental theorem of algebra will serve as an example of where countable choice comes into play and how to proceed in its absence. Along the way, a notion of a complete metric space, suitable for a choiceless environment, is developed.