Timeline for Approximate intermediate value theorem in pure constructive mathematics
Current License: CC BY-SA 3.0
41 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Apr 10 at 23:31 | comment | added | Mike Shulman | @ErelSegal-Halevi Because constructively you don't have trichotomy, so you can't decide whether f is positive, negative, or zero at the midpoint to determine which half-interval to proceed with. | |
Apr 10 at 19:30 | comment | added | Erel Segal-Halevi | Can you explain to a layman, why does the simple bisection method not work? | |
Dec 1, 2016 at 18:27 | comment | added | Mike Shulman | @MikhailKatz as mentioned in the original question, there are many versions of the IVT and many ways to prove it. For the approximate IVT I asked about here, as I mentioned, one standard way to prove it uses nothing but countable choice, which does not imply LPO. In the answer below, Matt F. gives a way to prove it without using even countable choice. | |
Dec 1, 2016 at 18:05 | comment | added | Mikhail Katz | Mike, my point was merely that one can't prove the extreme value theorem or the intermediate value theorem without using LPO. Is this not correct? | |
Dec 1, 2016 at 17:36 | comment | added | Mike Shulman | Similarly LLPO is equivalent to $\forall x, (x\le 0) \vee (x\ge 0)$, and in that case it is possible for there to exist a real number that is neither $\le 0$ nor $\ge 0$, as discussed in that section. But I really think it is not possible to violate trichotomy. To say $x>0$ means there exists a positive rational bounding $x$ away from 0. If this is false, then $x<q$ for all positive rationals $q$. Similarly, if $\neg(x<0)$ then $x>q$ for all negative rationals $q$, hence $|x|<q$ for all positive rationals $q$. No matter whether $x$ is a Cauchy or Dedekind real, this entails $x=0$. | |
Dec 1, 2016 at 17:33 | comment | added | Mike Shulman | @MikhailKatz Constructive mathematicians talk about existence all the time; in fact one might say they talk about it more than classical mathematicians do (who care more about failure to nonexist). I looked at the arXiv link, and the only thing I could find relevant was section 5 saying that trichotomy for reals is equivalent to LPO. But the negation of LPO doesn't entail the existence of a real number violating trichotomy, only that not all real numbers satisfy trichotomy: $\neg\forall \neq \exists \neg$ is a hallmark of constructive logic. | |
Dec 1, 2016 at 16:54 | comment | added | Mikhail Katz | Mike, this is a completely routine thing out of Troelstra--van Dalen. The only advantage of the article I mentioned is that it is shorter and focuses on the issue more than Troelstra-van Dalen. Once you start talking about "existence" you leave the company of constructive mathematicians, I think :-) Try the links given here. | |
Dec 1, 2016 at 16:50 | comment | added | Mike Shulman | @MikhailKatz - That article is behind a paywall. Can you explain (perhaps in a chat room) how such a real number can exist -- not just an element of some real-number-like ring such as the line object in SDG, I mean an actual Cauchy or Dedekind real number? | |
Dec 1, 2016 at 12:14 | comment | added | Mikhail Katz | @MikeShulman, sorry about the late response to your comment. Yes, that's what I meant ("or" instead of "and"). Such numbers can exist in certain intuitionistic settings; see a discussion for example in this article. | |
Nov 25, 2016 at 9:53 | answer | added | Franka Waaldijk | timeline score: 3 | |
S Nov 23, 2016 at 16:28 | history | bounty ended | Mike Shulman | ||
S Nov 23, 2016 at 16:28 | history | notice removed | Mike Shulman | ||
Nov 23, 2016 at 16:28 | vote | accept | Mike Shulman | ||
Nov 23, 2016 at 1:03 | answer | added | user44143 | timeline score: 29 | |
Nov 21, 2016 at 18:47 | comment | added | Toby Bartels | Actually, you can make the contrapositive IVT more interesting if you phrase it yet another way: If a real-valued function f defined on a real interval has both positive and negative values, but only positive or negative values, then it has a point of discontinuity, and you can actually find this point by interval-halving. This works in any ω-topos (that is any topos with a natural-numbers object). | |
Nov 21, 2016 at 18:31 | comment | added | Mike Shulman | @TobyBartels I don't have Bishop's book in front of me, so I don't know what he actually said; I actually reconstructed that sketch from an even briefer sketch in another paper that cited Bishop for it. (-: | |
Nov 21, 2016 at 16:58 | comment | added | Toby Bartels | (Proof: by contradiction is valid here; use interval halving; your hand is forced at every stage, no choices to make, so you can go forever; apply continuity at the limiting point c. Since this is a proof by contradiction, this point does not actually exist, of course.) | |
Nov 21, 2016 at 16:44 | comment | added | Toby Bartels | If it inspires anybody, here is a version of the IVT that applies to pointwise continuous functions in any topos (not an answer to Mike's question, but it might give people ideas): If every value of f is positive or negative, then every value of f is positive or every value of f is negative. This is basically a contrapositive of the classical (non-approximate) theorem, and while it is rather weak, it's strong enough for some things. (Basically, if somebody says something intuitively obvious that doesn't require a point c yet proves it with the IVT, then you can probably use this.) | |
Nov 21, 2016 at 16:38 | comment | added | Toby Bartels | Well, regardless of what Bishop may or may not say, your proof sketch certainly looks valid. From a uniformly-continuous perspective, it goes on unnecessarily long; you could stop when the interval length is less than the δ obtained from ϵ by the modulus of uniform continuity (which is why uniform continuity requires only finitely many choices). But by going on forever, you get a point at which you can apply mere pointwise continuity. (I guess that you already know all of that. For that matter, I may have known it once too and forgotten.) | |
Nov 21, 2016 at 14:30 | comment | added | Toby Bartels | @Mike, are you sure that Bishop's proof of IVT from DC applies to any pointwise continuous function? If you've checked the proof, then I beleive you, but you can't rely on Bishop's infallibilty; in his book (and in the Bishop & Bridges rewrite, although not in some other work by Bridges), ‘continuous’ means ‹pointwise continuous and (uniformly continuous on compact intervals)›. | |
Nov 18, 2016 at 20:48 | comment | added | Mike Shulman | @მამუკაჯიბლაძე, there's at least one way to do the coalgebraic reals constructively that ends up equivalent to the Dedekind reals; this is shown at the end of section D4.7 in Sketches of an Elephant. So that would certainly be acceptable. If there's a way to do coalgebraic reals constructively that doesn't end up equivalent to the Dedekind or Cauchy reals, then that wouldn't really be quite what I'm looking for, but it would nevertheless be interesting. | |
Nov 18, 2016 at 18:32 | comment | added | მამუკა ჯიბლაძე | Would "coalgebraic reals" be acceptable ones too? | |
Nov 18, 2016 at 17:35 | history | edited | Mike Shulman | CC BY-SA 3.0 |
clarify "the real numbers"
|
Nov 18, 2016 at 3:28 | answer | added | user44143 | timeline score: 5 | |
Nov 17, 2016 at 12:23 | comment | added | user44143 | That's interesting, I hadn't remembered it from Bishop & Bridges. Perhaps we can eliminate the use of DC. | |
Nov 16, 2016 at 23:34 | comment | added | Mike Shulman | @MattF. it's in Bishop's Foundations of constructive analysis. Basically you bisect the interval like classically, only you test the function values at the midpoints for being $< \epsilon$ or $> -\epsilon$ instead of $\le 0$ or $\ge 0$. Using DC you obtain a sequence of nested intervals $[a_n,b_n]$ of halving length with intersection $c$. If $f(c)<\epsilon$ then by continuity, $f(x)<\epsilon$ on a sufficiently small $[a_n,b_n]$, whence $a_n$ or $b_n$ is the desired point $d$ with $|f(d)|<\epsilon$. | |
Nov 16, 2016 at 22:50 | comment | added | user44143 | What or where is the proof that Pointwise Continuity + Dependent Choice --> Approximate IVT? | |
S Nov 15, 2016 at 20:45 | history | bounty started | Mike Shulman | ||
S Nov 15, 2016 at 20:45 | history | notice added | Mike Shulman | Draw attention | |
Nov 13, 2016 at 19:36 | comment | added | Mike Shulman | @MikhailKatz I assume you mean $\neg (a<0 \vee a=0 \vee a>0)$, or equivalently $\neg(a<0) \wedge \neg(a=0) \wedge \neg(a>0)$. Can such an $a$ really exist? I thought $\neg(a<0)$ was the same as $a\ge 0$, and similarly $\neg(a>0)$ the same as $a\le 0$, which together imply $a=0$. | |
Nov 13, 2016 at 13:22 | comment | added | Mikhail Katz | Just a quick sanity check: let $a$ be a real such that $\neg (a<0\wedge a=0\wedge a>0)$. Then the function $f(x)=ax$ is the well-known counterexample to the extreme value theorem. Now take the function $g(x)=f(x)-\frac{a}{3}$. Is this a counterexample to IVT? If we multiply it by a huge number would this give a counterexample even to the approximate form of the IVT? | |
Oct 27, 2016 at 17:57 | comment | added | Bas Spitters | To construct a function that's not uniformly continuous, one typically uses Kleene's first realizability model and considers Kleene's singular tree. By embedding Cantor space into [0,1] one obtains an unbounded function, which therefore cannot be uniformly continuous. This should be in Beeson's book. It can also be found in Troelstra/van Dalen or Bridges/Richman - Varieties of constructive mathematics. I seem to recall that one can combine realizability with forcing to obtain a model without countable choice and fan. However, I do not recall the source. Still, this does not yet contradict IVT. | |
Oct 26, 2016 at 22:42 | comment | added | Mike Shulman | Of course, a function that's continuous but not uniformly so is not necessarily a counterexample to IVT, but it might turn out to be one. | |
Oct 26, 2016 at 22:34 | comment | added | user44143 | @BasSpitters, you're right, and now I see that section 2.7 of Beeson's paper references this as a counterexample to uniform continuity. I don't understand that counterexample yet, so if you do you're welcome to write it up as an answer. | |
Oct 26, 2016 at 19:56 | comment | added | Bas Spitters | @MattF. This is called the fan rule. Kleene realizability/recursive mathematics gives a counter model to the fan rule. ncatlab.org/nlab/show/realizability However, it does model CAC. | |
Oct 26, 2016 at 17:12 | comment | added | user44143 | I found a reference for the claim: Michael Beeson, either his 1977 paper, sciencedirect.com/science/article/pii/S000348437780003X, secs 2.2, 2.6, 2.8, or in a bit more generality in his 1985 book. It also requires the extensionality of $\phi$, which is true here. | |
Oct 26, 2016 at 14:56 | comment | added | user44143 | Claim: Let $x,y$ range over $[a,b]$ and $m,n$ over $\mathbf{N}$. If $\phi(m,n,x) \rightarrow \phi(m+1,n,x)$, then we can transform a constructive proof of $\forall n\ \forall x\ \exists m\ \phi(m,n,x)$ into a constructive proof of $\forall n\ \exists m\ \forall x\ \phi(m,n,x)$. Special case with $$\phi(m,n,x) = \forall y\ ( |x-y|<1/m \rightarrow |f(x)-f(y)|<1/n)$$: if pointwise continuity is constructively provable then so is uniform continuity. Question for the crowd: is there a known result from which the claim follows? | |
Oct 26, 2016 at 14:22 | comment | added | Ingo Blechschmidt | For anyone looking for a counterexample let me remark that the most naive example does not work: Let $f : \mathbb{R} \to \mathbb{R}$ be a fixed continuous function. Let $X$ be a metric space. The object of Dedekind real numbers in the sheaf topos $\mathrm{Sh}(X)$ is the sheaf $\mathcal{C}_X$ of continuous functions on $X$. The function $f$ induces a morphism $\mathcal{C}_X \to \mathcal{C}_X$ by postcomposition, that is internally a function $\mathbb{R} \to \mathbb{R}$. From the internal point of view, this function is continuous and verifies the strong IVT. | |
Oct 25, 2016 at 21:20 | comment | added | Mike Shulman | @MattF. I thought I'd seen a weak counterexample to the statement "every pointwise continuous function on [a,b] is uniformly continuous", though I don't remember it offhand. But in any case, as I said, a strong countermodel would be even better. | |
Oct 25, 2016 at 19:56 | comment | added | user44143 | In most varieties of constructive math, the functions which are defined on [a,b] and provably pointwise continuous on [a,b] are also provably uniformly continuous on [a,b]; the inferential rule is valid even though the implication is not provable. Or so I suspect, though I've only seen proofs of related things and not of this specifically. In any case, because of this I wouldn't expect to see a weak counterexample. | |
Oct 25, 2016 at 17:34 | history | asked | Mike Shulman | CC BY-SA 3.0 |