Constructive intermediate value theorem
Constructive intermediate value theorem
I have given real numbers $x_1,x_2,y_1,y_2$ such that $x_1 > x_2$ and $y_1 < y_2$. The the claim is that there exists some $lambda in (0,1)$ such that $lambda (x_1 - x_2) + (1-lambda)(y_1-y_2) = 0$. In order to proof this, one needs ( at least in my opinion) the intermediate value theorem. But the intermediate value theorem does not hold in constructive mathematics (that is without the law of excluded middle; or constructive mathematics acts in intuitionistic logic). For a proof of this c.f. this paper.
Is there any constructive way to show the above equation?
$begingroup$
@GiuseppeNegro the "construction" is not "constructive" enough for this purpose; it uses "either the left or the right works, so pick one, and ..." but constructions of this kind (especially with an infinite number of such choices) are forbidden in that context
$endgroup$
– Richard Rast
Sep 18 '18 at 13:43
$begingroup$
@RichardRast: OK. On the other hand, if the function is differentiable, the Newton's method is available. That definitely is constructive. Am I right? This would provide a way of solving more general problems of the kind of this question
$endgroup$
– Giuseppe Negro
Sep 18 '18 at 13:56
$begingroup$
@GiuseppeNegro I'm not an expert on constructive mathematics, but according to Dr. Google, Cauchy's theorem has a constructive proof. If Newton's method is constructively proved to converge to a solution, that should be valid. But I think the conditions on it converging might be nontrivial and require additional "constructive metadata" (like an explicit neighborhood around the point in which blah blah blah) ...
$endgroup$
– Richard Rast
Sep 18 '18 at 14:05
$begingroup$
(cont.) but the accepted answer below is the intent of the discipline, to move away from general theorems that prove existence and toward constructions which (theoretically) give more information. Below we have the exact form of the answer, which in practice is often more useful than just knowing the answer exists.
$endgroup$
– Richard Rast
Sep 18 '18 at 14:08
2 Answers
2
Just solve the equation for $lambda$. You get $lambda =frac y_2-y_1x_1-x_2+y_2-y_1$.
You can explicitly solve the equation;
$$lambda= fracy_2-y_1x_1-x_2-y_1+y_2.$$
Thanks for contributing an answer to Mathematics Stack Exchange!
But avoid …
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Required, but never shown
Required, but never shown
By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy
$begingroup$
Anyway, the intermediate value theorem can be proved in a "constructive" way. (I put the "..." because I don't know a word about constructive mathematics). By bisecting iteratively, you construct a sequence that turns out to be Cauchy, and so it has a limit.
$endgroup$
– Giuseppe Negro
Sep 18 '18 at 10:19