Unique existence and computability in constructive reverse mathematics

Abstract

We introduce, and show the equivalences among, relativized versions of Brouwer's fan theorem for detachable bars (FAN), weak König lemma with a uniqueness hypothesis (WKL!), and the longest path lemma with a uniqueness hypothesis (LPL!) in the spirit of constructive reverse mathematics. We prove that a computable version of minimum principle: if f is a real valued computable uniformly continuous function with at most one minimum on {0, 1}N, then there exists a computable α in {0, 1}N such that f(α) = inf f({0, 1}N), is equivalent to some computably relativized version of FAN, WKL! and LPL!. © Springer-Verlag Berlin Heidelberg 2007.