Skip to main content
Notice removed Draw attention by Mike Shulman
Bounty Ended with user44143's answer chosen by Mike Shulman
clarify "the real numbers"
Source Link
Mike Shulman
  • 66.8k
  • 7
  • 162
  • 368

The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise countermodel: the basic idea is that the root may not depend continuously or computably on the function, since a small perturbation in a function's value may cause a root to appear or disappear.

There are, however, many variants of the IVT that are constructively provable. This question is about the approximate IVT, which says that if $f(a)<0<f(b)$ then for any $\epsilon>0$ there is a point $x$ with $|f(x)|<\epsilon$. It seems to be well-known that the approximate IVT can be proven assuming either (1) countable (or maybe dependent) choice, or (2) that $f$ is uniformly continuous. This paper contains many versions of approximate IVT using somewhat weaker hypotheses such as "strong continuity" of $f$. But I would like to know:

Can the approximate IVT be proven constructively about an arbitrary (pointwise) continuous function $f$, without using any form of choice or excluded middle (e.g. in the mathematics valid in any elementary topos with NNO)?

If the answer is no, I would like to see at least a weak counterexample, or even better a specific countermodel (e.g. a topos in which it fails).

Edit: To clarify, the functions in question are from the real numbers (or some interval therein) to the real numbers. I'll accept an answer that defines "the real numbers" either as equivalence classes of Cauchy sequences or as Dedekind cuts (but not as a "setoid" of Cauchy sequences).

The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise countermodel: the basic idea is that the root may not depend continuously or computably on the function, since a small perturbation in a function's value may cause a root to appear or disappear.

There are, however, many variants of the IVT that are constructively provable. This question is about the approximate IVT, which says that if $f(a)<0<f(b)$ then for any $\epsilon>0$ there is a point $x$ with $|f(x)|<\epsilon$. It seems to be well-known that the approximate IVT can be proven assuming either (1) countable (or maybe dependent) choice, or (2) that $f$ is uniformly continuous. This paper contains many versions of approximate IVT using somewhat weaker hypotheses such as "strong continuity" of $f$. But I would like to know:

Can the approximate IVT be proven constructively about an arbitrary (pointwise) continuous function $f$, without using any form of choice or excluded middle (e.g. in the mathematics valid in any elementary topos with NNO)?

If the answer is no, I would like to see at least a weak counterexample, or even better a specific countermodel (e.g. a topos in which it fails).

The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise countermodel: the basic idea is that the root may not depend continuously or computably on the function, since a small perturbation in a function's value may cause a root to appear or disappear.

There are, however, many variants of the IVT that are constructively provable. This question is about the approximate IVT, which says that if $f(a)<0<f(b)$ then for any $\epsilon>0$ there is a point $x$ with $|f(x)|<\epsilon$. It seems to be well-known that the approximate IVT can be proven assuming either (1) countable (or maybe dependent) choice, or (2) that $f$ is uniformly continuous. This paper contains many versions of approximate IVT using somewhat weaker hypotheses such as "strong continuity" of $f$. But I would like to know:

Can the approximate IVT be proven constructively about an arbitrary (pointwise) continuous function $f$, without using any form of choice or excluded middle (e.g. in the mathematics valid in any elementary topos with NNO)?

If the answer is no, I would like to see at least a weak counterexample, or even better a specific countermodel (e.g. a topos in which it fails).

Edit: To clarify, the functions in question are from the real numbers (or some interval therein) to the real numbers. I'll accept an answer that defines "the real numbers" either as equivalence classes of Cauchy sequences or as Dedekind cuts (but not as a "setoid" of Cauchy sequences).

Notice added Draw attention by Mike Shulman
Bounty Started worth 200 reputation by Mike Shulman
Source Link
Mike Shulman
  • 66.8k
  • 7
  • 162
  • 368

Approximate intermediate value theorem in pure constructive mathematics

The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise countermodel: the basic idea is that the root may not depend continuously or computably on the function, since a small perturbation in a function's value may cause a root to appear or disappear.

There are, however, many variants of the IVT that are constructively provable. This question is about the approximate IVT, which says that if $f(a)<0<f(b)$ then for any $\epsilon>0$ there is a point $x$ with $|f(x)|<\epsilon$. It seems to be well-known that the approximate IVT can be proven assuming either (1) countable (or maybe dependent) choice, or (2) that $f$ is uniformly continuous. This paper contains many versions of approximate IVT using somewhat weaker hypotheses such as "strong continuity" of $f$. But I would like to know:

Can the approximate IVT be proven constructively about an arbitrary (pointwise) continuous function $f$, without using any form of choice or excluded middle (e.g. in the mathematics valid in any elementary topos with NNO)?

If the answer is no, I would like to see at least a weak counterexample, or even better a specific countermodel (e.g. a topos in which it fails).