Intermediate value theorem is equivalent to (some constructive taboo)

[jkingdon]

The intermediate value theorem is https://us.metamath.org/mpeuni/ivth.html

In iset.mm we will only be able to prove special cases such as https://us.metamath.org/ileuni/ivthinc.html but can we put a finer point on this?

The proof by bisecting intervals in [Bauer] ("Classical proof" of Theorem 5.1) appears to need real number trichotomy (analytic LPO). It might be a bit tricky to formalize in iset.mm because I don't think we have convergence theorems which directly map to the descending chain argument there, but https://us.metamath.org/ileuni/climcvg1n.html or something like it should be sufficient with only a moderate amount of adaptation, because the intervals are decreasing in size at a bounded rate.

Next question: can we show the intermediate value theorem implies a taboo (and is it analytic LPO or some other taboo)? The problem somewhat reminds me of #4042 but I don't have a specific argument in mind.

More reading:

• A Proof that there's No Constructive Proof of the Intermediate Value Theorem (blog post by Chris Grossack) makes an argument based on "Soundness and Completeness of the topos semantics of constructive logic". Whether this has any direct application to deriving a taboo in iset.mm I'm not sure, but there are pretty pictures (similar to the figure in section 5.1 of [Bauer]).

[digama0]

The most obvious taboo to target is totality of less-equal. WLOG we can assume the second number is zero. Given $x$ which we want to compare to zero, construct the function $f(x)=if(x<0,-x,if(x>1,x-1,0))=x+(|x-1|-|x|-1)/2$. By IVT, there is some $y$ such that $f(y)=x$. By weak trichotomy, either $y<1$ or $y>0$, but the first case implies $x\le 0$ and the second implies $x\ge 0$.

[jkingdon]

The most obvious taboo to target is totality of less-equal.

Also known as analytic LLPO (per chart at https://us.metamath.org/ileuni/mmil.html under "Different flavors of constructive mathematics").

Given x which we want to compare to zero, construct the function . . .

This definition relies on decidability of less-than. (pretty much every theorem involving if has a condition that the proposition in the if is decidable).

[digama0]

The reason I gave an alternative definition with abs was exactly to forestall this objection, it's a continuous function which you can define without decidability of less equal. The definition with if is there to help understand the purpose of the function (and why the inequalities I assert later hold)

[digama0]

This is also the same function (more or less) used on https://grossack.site/2025/06/10/ivt-not-constructive . It can also be written as $\max(\min(x,0),x-1)$.

[digama0]

Using LLPO and dependent choice, you can prove the IVT along the lines of [Bauer] theorem 5.1. You construct a descending sequence of intervals by $[a_{n+1},b_{n+1}]=[a_n,c_n]$ if $f(c_n)\ge 0$ and $[a_{n+1},b_{n+1}]=[c_n,b_n]$ if $f(c_n)\le 0$. Because these two cases are non-exclusive, you have to pick one when both apply, which is why this construction uses DC. (You can actually weaken it to just use CC because $c_n$ is contained in $a_0+(b_0-a_0)\mathbb{Q}$ so you can just decide $f(x)\le 0\lor f(x)\ge 0$ independently for each of them.)

[jkingdon]

The reason I gave an alternative definition with abs was exactly to forestall this objection, it's a continuous function which you can define without decidability of less equal. The definition with if is there to help understand the purpose of the function (and why the inequalities I assert later hold)

Ah OK now I see what you mean with the two definitions. We have a bunch of abs related theorems in iset.mm (and the min/max of two reals for that matter) and you are correct that these are well defined constructively. The key continuity theorem is presumably https://us.metamath.org/ileuni/abscncf.html (which we already have).

[HallaSurvivor]

Thanks for thinking about this! I'm planning to cite this thread in an update to my blog post, and I want to give you both credit. Is that ok, and do you have websites you would want me to link?

[jkingdon]

Thanks for thinking about this! I'm planning to cite this thread in an update to my blog post, and I want to give you both credit. Is that ok, and do you have websites you would want me to link?

Heh, I think of it as being more cite-worthy once I get something formalized (I do expect to take a try in the coming days/weeks, once I'm done with some other things I'm formalizing). This is for a few reasons including that I am not smart enough to find holes in the argument (if any) without the proof verifier to help me go through it. But hey, I'm all for citing work in progress too, so go for it.

As for websites to link, for me I don't know if there's the perfect math site but https://sfba.social/@soaproot and the Metamath iset.mm page at https://us.metamath.org/ileuni/mmil.html should be the best ones I would think.

That's all on behalf of me - I'll let Dr. Carneiro speak for himself on his end.

[digama0]

I'm not sure I can take credit for the function and general argument; it's a classic (but not classical!) proof and both Bauer and Grossack are using this function.

[HallaSurvivor]

Sure, but even if I wanted to say that you were talking about it here, is there a website you'd like me to link?