In choiceless constructivism: If $f'=0$ then is $f$ constant?

Question

Prove, without any Choice principles or Excluded Middle, that if a pointwise differentiable function has derivative $0$ everywhere, then it is constant. The function in this case maps $\mathbb R$ to $\mathbb R$, where $\mathbb R$ denotes the Dedekind reals. Unique Choice is allowed.

The usual proof of this proposition is via the Mean Value Theorem or the Law of Bounded Change. However the former is non-constructive, and the truth of the latter (in the absence of Dependent Choice) is an open problem.

Similar questions about elementary analysis in weak foundations have been asked before on this site. For instance, see: Approximate intermediate value theorem in pure constructive mathematics

Answer 1

For a real function $f$ with continuous derivative $f'$ we have the following identity which should not require any choice to prove:

$$ f(x) = f(0) + \int_0^x f'(y)dy \ \ (\mbox{all}\ x\in\mathbb{R}) $$

From this identity the proof of your proposition follows trivially.

---

[Update April 12 to reflect the comments below:]

The idea is to use the derivative $f'$ to reconstruct the original $f$. For this one in principle does not need choice, but rather a compactness-related property (called 'uniformly differentiable') which acts exactly like uniform continuity of continuous functions on the interval $[0,1]$.

Let's call a function $f$ locally uniformly differentiable iff for all $K\in\mathbb{N}, n\in\mathbb{N}$ there is $m\in\mathbb{N}$ such that

$\forall x{\in} [-K,K]\forall h{\in} [-2^{-m}, 2^{-m}][|f(x+h)-(f(x)+h\cdot f'(x))|<2^{-n}\cdot h]$

Notice that Heine-Borel (or the Fan Theorem) implies that all differentiable real functions are locally uniformly differentiable (which is the same as 'uniformly differentiable on each compact interval').

Bishop adapted the definition of 'continuous function' to include 'uniformly continuous on each compact interval', since in the absence of Heine-Borel without this extra condition it becomes impossible to prove basic results in analysis.

In BISH, it is my conviction that we also need differentiable functions to be locally uniformly differentiable, for the same reasons that we need continuous functions to be locally uniformly continuous.

So finally, my answer becomes:

For a locally uniformly differentiable function $f$ with continuous derivative $f'$ we have the following identity which does not require any choice to prove:

$$ f(x) = f(0) + \int_0^x f'(y)dy \ \ (\mbox{all}\ x\in\mathbb{R}) $$

From this identity one trivially proves:

Proposition If $f$ is a locally uniformly differentiable function with pointwise derivative $0$ everywhere, then $f$ is constant.

What is required in my eyes is therefore not choice or LEM, but an incorporation of compactness in the definition of 'differentiable'.

Answer 2

For the record, I provide here a proof of the constancy principle from the principle of open induction. Recall:

Principle of open induction: Let $U \subseteq [0,1]$ be an open set such that $$\forall x \in [0,1] . (\forall y \in [0,1] . y < x \Rightarrow y \in U)) \Rightarrow x \in U.$$ Then $U = [0,1]$.

We also have:

Constancy principle: For a pointwise differentiable map $f : \mathbb{R} \to \mathbb{R}$, if $f'(x) = 0$ for all $x \in \mathbb{R}$, then $f$ is constant.

Theorem: The principle of open induction implies the constancy principle.

Proof. Let $f : \mathbb{R} \to \mathbb{R}$ be pointwise differentiable with $f'(x) = 0$ for all $x \in \mathbb{R}$. Observe that $f$ is pointwise continuous. We show that $f$ is constant on $[0,1]$, and leave the generalization to arbitrary intervals as exercise.

It suffices to show that for all $\epsilon > 0$ and $x \in [0,1]$ we have $|f(x) - f(0)| < \epsilon \cdot x$. The set $$U = \{x \in [0,1] \mid |f(x) - f(0)| < \epsilon \cdot x\}, $$ is open because $f$ is pointwise continuous. We prove that $U = [0,1]$ by open induction. Let $x \in [0,1]$ and assume that $|f(y) - f(0)| < \epsilon \cdot y$ for all $y$ such that $0 \leq y < x$. Because $f'(x) = 0$, there exists $\delta > 0$ such that $|f(x) - f(z)| < \epsilon \cdot (x - z)$ for all $z$ such that $x - \delta < z < x$. We have $x < \delta$ or $x > \delta/2$:

1. If $x < \delta$ then we take $z = 0$ to directly obtain the desired inequality $|f(x) - f(0)| < \epsilon \cdot x$.

2. If $x > \delta/2$ then we take $z = x - \delta/4$, so that $|f(z) - f(0)| < \epsilon \cdot z$ by assumption, and conclude by \begin{align*} |f(x) - f(0) &\leq |f(x) - f(z)| + |f(z) - f(0)| \\ &< \epsilon \cdot (x - z) + \epsilon \cdot z \\ &= \epsilon \cdot x. \end{align*}

Answer 3

This answer is incorrect since the function $f\colon\mathbb R \to\mathbb R$ is not computable. That said, it is possible that a similar idea could provide a counterexample.

---

There is a computable closed set $C \subseteq [0,1]$ with positive measure that contains no computable real number. (This is well-known but I give a construction below.) The function $f\colon\mathbb R \to \mathbb R$ given by $f(x) = \mu(C \cap [0,x])$ has the property that $f'(x) = 0$ for every computable $x$ but it is not a constant function since $f(0) = 0$ and $f(1) = \mu(C) > 0$. If I understand the question correctly, this gives a counterexample in the effective topos.

To construct such a $C$, build a computable sequence $(a_0,b_0), (a_1,b_1),\ldots$ of open intervals with rational endpoints such that $\sum_{k=0}^\infty b_k - a_k \leq 1/2$ as described below and then let $C = [0,1] \setminus \bigcup_{k=0}^\infty (a_k,b_k)$, which is a closed set of measure at least $1/2$.

Let $\varphi_0,\varphi_1,\ldots$ be a computable enumeration of all partial computable functions $\mathbb N \to \{0,1\}$. Write $\varphi_{i,s}$ for the part of $\varphi_i$ which has converged by stage $s$. Also, fix a computable enumeration $q_0,q_1,\ldots$ of $\mathbb Q$.

At stage $s$ of the construction, suppose we have constructed $(a_0,b_0),\ldots,(a_{k-1},b_{k-1})$. Look for the first $i \leq s$ such that:

1. For all $m, n \in \operatorname{dom} \varphi_{i,s}$, if $\varphi_{i,s}(m) = 0$ and $\varphi_{i,s}(n) = 1$ then $q_m < q_n$ (i.e., this looks like part of a Dedekind cut so far).
2. There are no $m, n \in \operatorname{dom} \varphi_{i,s}$ and $j < k$ with $\varphi_{i,s}(m) = 0$ and $\varphi_{i,s}(n) = 1$ such that $a_j < q_m$ and $q_n < b_j$ (i.e., this Dedekind cut has not yet been covered by one of our intervals).
3. There are $m, n \in \operatorname{dom} \varphi_{i,s}$ with $\varphi_{i,s}(m) = 0$ and $\varphi_{i,s}(n) = 1$ such that $q_m - q_n < 1/3^{i+1}$ (i.e., we know enough about this Dedekind cut to cover it with a small interval).

If such an $i \leq s$ is found, then add the interval $(a_k,b_k = a_k + 1/3^{i+1})$ to the list where $a_k < q_m$ and $q_n < b_k$ for $m,n$ as in condition 3. Otherwise, do nothing and move to the next stage.

Note that if $\varphi_i:\mathbb N \to \{0,1\}$ really is a Dedekind cut (i.e., $\varphi_i$ is not constant and if $\varphi_i(m) = 0$, $\varphi_i(n) = 1$ then $q_m < q_n$) then at some stage $\varphi_{i,s}$ will be large enough to meet requirements 1,2,3. Then the real number represented by $\varphi_i$ will be covered by one interval in our list. Also, since our list contains at most one interval of length $1/3^{i+1}$ for each $i$, it follows that $\sum_{k=0}^\infty b_k - a_k \leq \sum_{i=0}^\infty 1/3^{i+1} = 1/2$.

Answer 4

Here's a stab at the question that attempts to make use of the locale of real numbers. (If someone has published something similar, please point me towards it). The reasoning behind this is that if you care about completely choiceless foundations, you are most likely studying topoi including ones that pop up in non-foundational applications, and locales are just inherently more useful than topological spaces in that setting since results about them are easy to translate.

The central idea is to classically (where by classical we mean BISH) rephrase a function satisfying upper + lower Lipschitz conditions using interval arithmetic in the following way: we define $f : \mathbf{R} \to \mathbf{R}$ to have a Lipschitz derivative $f'(U) : I(\mathbf{R})$ on an interval I if

$f(x) - f(y) \in f'(I) (x-y)$

where we remind the reader that $f'(I)$ is an interval and that arithmetic operations with interval are just interval arithmetic as practiced by applied mathematicians. This is just a basic rewriting of the Lifshitz conditions $A(x - y) \leq f(x) - f(y) \leq B(x - y)$ using interval multiplication. However, now that we have had a taste of how the Lipschitz condition really defines a (not necessarily optimal) numerical approximation of a derivative, we may go all the way and rephase everything for intervals $I_1$, $I_2$ instead of points:

$f(I_1) - f(I_2) \subset f'(I) (I_1-I_2)$

where this still uses interval arithmetic. Since the direct image of a map from the locale of reals to itself maps intervals to intervals, we can view this as a definition of Lipschitz derivatives that is more locale-friendly. A key observation here is that if you have an open cover where all $I_i \subset I$ have f-derivatives $f'(I_i) \subset f'(I)$, then $f'(I)$ is a Lipschitz derivative on $I$.

---

To define the derivative at a point $p$ (i.e. completely prime filter $\mathit{N}(p)$ ), we view it as the limit of the prefilter of Lipschitz derivatives at neighbourhoods of $p$ which are subsets of some decidable neighbourhood of $p$ where $f$ is Lipschitz continuous.

We say classically that $f$ is pointwise differentiable at p with derivative $f'(p)$ if $\forall \epsilon > 0$ there is a neighbourhood of p where f has Lipschitz derivative $[f'(p)-\varepsilon, f'(p)+\varepsilon]$. Clearly, if f' is a bounded function defined on a closed interval, then in BISH countable choice + separability gives that f is Lipschitz continuous everywhere, and if it is zero everywhere the Lipschitz derivatives are arbitrarily tight, and the function is constant.

However, if we want to rephrase this for the locale of real numbers, the condition of having a continuous function as the derivative only really makes sense if the derivative is also a map of locales, so you want to flip that definition on its head without changing what it means in constructive math with CC. Here you should require that the function is Lipschitz continuous everywhere in order for the derivative-as-a-function to be well defined, and this means that we can check the inverse image of any open Lipschitz derivative to see where $f$ satisfies the Lipschitz condition on all closed rational subintervals of the inverse image. This doesn't have the same flavour as changing the notion of derivative to be non-local, it basically only requires that an actual computer can actually verify numerically that $f'$ is the derivative of $f$ from approximation of real numbers as rational intervals without any other limits on how quickly things converge.

Now, in choiceless foundations, we can still just use the fact that maps between spatial locales are just continuous functions between sober spaces, so in that case requiring that f' is constant at every point does indeed imply that the map factors through a point. So if you define f' as an optimal Lipschitz derivative on all intervals (i.e. that f is Lipschitz continuous) and you assume that the reals are spatial, being pointwise zero does indeed mean that f is constant. This is an alternative to the "uniformly zero" condition in the other answer, and its assumptions of the locals being real are effectively dual to assuming Heine-Borel.

(Alternatively, you could define that the derivative is zero not as a pointwise function but as a map of locales by making it factor through the one point locale, and this gets rid of the spatiality condition. But then the result is just too trivial since we would be effectively just directly defining the function to be constant)