Let $f:[0,1] \to \mathbb R$ be a uniformly continuous function such that each value of $f(x)$ is greater than zero. Is its infimum greater than zero in BISH?

I believe that it is indeed the case if one assumes the Fan Theorem. But independent of it, I'm not sure.


Note: It's possible to get around this problem in practice by interpreting $f > 0$ to mean that there exists a constant $c$ such that $f(x) > c > 0$ for all $x$. This is an example of a pseudo-order. The fact that the infimum is greater than zero is then a tautology.

  • $\begingroup$ In response to your edit: yes, the infimum of $f$ now is greater than $0$, but often the new problem becomes to show that $\inf(f)> c$ ... and then we're back at square one. $\endgroup$ Nov 13 '19 at 13:20
  • $\begingroup$ What my paper shows is that there is no simple way to avoid the Fan Theorem if one wishes continuous functions to have certain nice properties. And I am not convinced that the non-simple ways that have been proposed so far to remediate this are really workable in all areas of mathematics. $\endgroup$ Nov 13 '19 at 13:23
  • 1
    $\begingroup$ To the reader wondering what "BISH" could mean: it seems that it means "the Bishop school of constructive mathematics". $\endgroup$
    – Alex M.
    Nov 14 '19 at 9:36

In BISH the follwoing two statements are equivalent:

(i) If $f:[0,1] \to \{y\in\mathbb R\, | \,y>0\}$ is uniformly continuous, then there is $n\in\mathbb N$ such that $\forall x \in [0,1]\ [f(x)>\frac{1}{n}]$

(ii) The Fan Theorem FT

This was already proved in Julian, W.H., and Richman, F., 1984, “A uniformly continuous function on [0, 1] that is everywhere different from its infimum”, Pacific Journal of Mathematics,111: 333–340.

A simpler proof, and a lot more consequences, are given in my paper On the foundations of constructive mathematics --- especially in relation to the theory of continuous functions


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.