Many existence propositions in constructive analysis are implied by the lesser limited principle of omniscience LLPO; sometimes one can even show equivalence. It was discovered recently that some existence propositions are equivalent to Bouwer's fan theorem FAN if one additionally assumes that there exists at most one object with the desired property. We are providing a list of conditions being equivalent to FAN, such as a unique version of weak König's lemma. This illuminates the relation between FAN and LLPO. Furthermore, (...) we give a short and elementary proof of the fact that FAN is equivalent to each positive valued function with compact domain having positive infimum. (shrink)

We introduce the notion of a convex tree. We show that the binary expansion for real numbers in the unit interval ) is equivalent to weak König lemma ) for trees having at most two nodes at each level, and we prove that the intermediate value theorem is equivalent to \ for convex trees, in the framework of constructive reverse mathematics.

Working within Bishop’s constructive framework, we examine the connection between a weak version of the Heine–Borel property, a property antithetical to that in Specker’s theorem in recursive analysis, and the uniform continuity theorem for integer-valued functions. The paper is a contribution to the ongoing programme of constructive reverse mathematics.

The existence and uniqueness of a maximum point for a continuous real—valued function on a metric space are investigated constructively. In particular, it is shown, in the spirit of reverse mathematics, that a natural unique existence theorem is equivalent to the fan theorem.

We show constructively that every quasi-convex, uniformly continuous function \ with at most one minimum point has a minimum point, where C is a convex compact subset of a finite dimensional normed space. Applications include a result on strictly quasi-convex functions, a supporting hyperplane theorem, and a short proof of the constructive fundamental theorem of approximation theory.

It is shown, with intuitionistic logic, that if every locally constant function from to has a property akin to constancy, then the fan theorem for -bars holds, and conversely.

Dini's theorem says that compactness of the domain, a metric space, ensures the uniform convergence of every simply convergent monotone sequence of real-valued continuous functions whose limit is continuous. By showing that Dini's theorem is equivalent to Brouwer's fan theorem for detachable bars, we provide Dini's theorem with a classification in the recently established constructive reverse mathematics propagated by Ishihara. As a complement, Dini's theorem is proved to be equivalent to the analogue of the fan theorem, weak König's lemma, in (...) the original classical setting of reverse mathematics started by Friedman and Simpson. (shrink)

We prove constructively that the weak König lemma and quantifier-free number-number choice imply that every pointwise continuous function from Cantor space into Baire space has a modulus of uniform continuity.

It is shown that, relative to Bishop-style constructive mathematics, the boundedness principle BD-N is equivalent both to a general result about the convergence of double sequences and to a particular one about Cauchyness in a semi-metric space.

We represent continuous functions on compact intervals by sequences of functions defined on finite sets of rational numbers. We call this an exact representation. This enables us to calculate the values of the function arbitrarily exactly, without roundoff errors. As an application we develop a procedure to transfer an exact representation of an increasing function into an exact representation of the corresponding inverse function.

In this paper we analyse in the framework of constructive mathematics (BISH) the validity of Farkas' lemma and related propositions, namely the Fredholm alternative for solvability of systems of linear equations, optimality criteria in linear programming, Stiemke's lemma and the Superhedging Duality from mathematical finance, and von Neumann's minimax theorem with application to constructive game theory.

The problem of the origin of life understandably counts as one of the most exciting questions in the natural sciences, but in spite of almost endless speculation on this subject, it is still far from its final solution. The complexity of the functional correlation between recent nucleic acids and proteins can e.g. give rise to the assumption that the genetic code (and life) could not originate on the Earth. It was Portelli (1975) who published the hypothesis that the genetic code (...) could not originate during the history of the Earth. In his opinion the recent genetic code represents the informational message transmitted by living systems of the previous cycle of the Universe. Here however, we defend the existence of a certain strategy in the syntheses of the genetic code during the history of the Earth. The strategy of correlation between amino acid and nucleotide polymers made an increasing velocity of the chemical evolution possible, that is, it increased the velocity of formation of the genetic code. Thus, life with the recent genetic code could originate on the Earth within the present cycle of the Universe. (shrink)