Return to Answer

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}]$

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'.

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'.

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}]$

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, be it only already to prove the Fundamental theorem of Calculus (!).

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'.

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}]$

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'.

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}]$

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, be it only already to prove the Fundamental theorem of Calculus (!).

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'.

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}]$

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, be it only already to prove the Fundamental theorem of Calculus (!).

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'.