6
$\begingroup$

In constructive analysis, I'm looking at principles which follow both when there exists at least one discontinuous function from $\mathbb{R}$ to $\mathbb{R}$ (equivalent to WLPO i.e. $x > 0$ or $x \leq 0$, holds for anything similar to classical real analysis) while also being true in real analysis when all functions are continuous (true for the internal logic of many real-world topoi including $\operatorname{Sh}(M)$ where $M$ is a manifold, or for the effective topos, or in the effective topos, and generally in both Brouwerian and Russian-style constructive mathematics).

One of these is this weakening of WLPO: for any function $f\colon \mathbb{R} \to \mathbb{R}$ , if $f(x) > 0$ for $x \geq 0$ and $f(x) > 0$ for $x < 0$, then $f(x) > 0$. Clearly this follows from WLPO, but it also follows from $f$ being continuous so that each case can be extended to an open neighbourhood of the half segments.

This is a very convenient lemma to get rid of epsilons in upper bounds. Does it have a name? Is it provable in Bishop's axiomatization or in arbitrary spatial toposes?

Improve this question
$\endgroup$
2
  • $\begingroup$ Quick observation: the weakened WLPO in the question also follows from Markovs Principle. Since for every f, we have that not f(x) implies not x > 0 and not not x > 0, so we have not not f(x) > 0 and by MP f(x) > 0 $\endgroup$ Commented Nov 21, 2024 at 6:21
  • $\begingroup$ Another note: the version of this theorem with non-strict inequalities is straightforward to prove in BISH. The hard part is getting the version with strict inequalities to work. $\endgroup$ Commented Nov 22, 2024 at 8:10

1 Answer 1

Reset to default
3
$\begingroup$

Assuming that your definition of 'function' includes strong extensionality ($f(x)\#f(y)$ implies $x\#y$), it is provable in BISH, as follows:

Let $f$ be as described in the question. Then we know that $f(0)>0$. Determine $s\in\mathbb{N}$ such that $f(0)>\frac{1}{s}$.

Now let $x\in\mathbb{R}$, we distinguish two cases:

I. $f(x)<\frac{1}{s}$, in which case $f(x)\#f(0)$ and so $x\#0$ by strong extensionality. From $x\#0$ it follows that $f(x)>0$.

II. $f(x)>\frac{1}{2s}$ and we are done straightaway.

Since we can always decide at least one of these cases to hold, we are done.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Very nice, this basically weakens following from MP or Brouwers principle to just following WMP, or restricting the theorem to hold for strongly extensional functions. It also looks like we can just skip finding s in N as well and just use f(0) instead of 1/s in your proof, or am I missing something? In that case it should hold for sheaf topoi over any sequential space since WMP holds for those and that includes every logic I am interested in, though I don't remember if weak extensionality follows from WMP without choice $\endgroup$ Commented Jan 20 at 19:31
  • 1
    $\begingroup$ you are right of course, f(0) works directly and we can skip finding s in N. $\endgroup$ Commented Jan 21 at 2:04
  • $\begingroup$ Ah, Richman has a counterexample to what I hoped to be true for sheaves on the unit interval. Let c be an internal real number externally given by the function f(t) = t - t^2. Then the function from the complete metric space {0,c} to R given by f(0) = 0 and f(c) = 1 is not strongly extensional because 0 and c are not apart. This is despite WMP being true in that topos $\endgroup$ Commented Jan 23 at 9:26
  • $\begingroup$ It does make me wonder if it's still possible to rescue the a weakened version of the claim that every function is strongly extensional, but for complete and convex metric spaces instead of just complete ones, but that's a separate question from this one $\endgroup$ Commented Jan 23 at 9:42
  • $\begingroup$ i'm not sure what you mean, but in BISH, with BISH definitions, the statement 'every real function is strongly extensional' is equivalent to MP. $\endgroup$ Commented Jan 23 at 10:04

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.