18
$\begingroup$

Although mathematicians usually do not work in constructive mathematics per se, their results often are constructively valid (even if the original proof isn't).

An obvious counter-example is the law of excluded middle itself, discovered by Aristotle between 400 and 300 B.C.

LEM is a result in the field of propositional logic. However, what about results outside of logic, like number theory or analysis? The simplest such result I know of is the existence of step functions, but I don't know when that was discovered.

I'll leave "not constructively valid" a bit open-ended, but just saying that there is no known constructive proof doesn't count. A valid answer could show that the result implies a constructive taboo, or that it's independent of a constructive type theory or set theory, for example. (In the case of step functions, their existence implies the analytic LPO, a constructive taboo.)

Improve this question
$\endgroup$
7
  • 18
    $\begingroup$ Depends on what you mean by "result". "Every real number is either positive, negative, or zero" is something that was surely "known" long before a formal definition of real numbers was found. $\endgroup$
    – Will Sawin
    Commented Feb 22 at 17:18
  • 1
    $\begingroup$ Could some result from the Elements depend on it perhaps? $\endgroup$
    – Wojowu
    Commented Feb 22 at 17:25
  • 3
    $\begingroup$ Along the lines of @WillSawin's comment, perhaps we should stipulate that the statement shouldn't be just an instance of excluded middle (or something very close to it). $\endgroup$
    – Andrej Bauer
    Commented Feb 22 at 19:03
  • 2
    $\begingroup$ The very first postulate in Euclid's Elements is “to draw a straight line from any point to any point” (“ᾘτήσθω ἀπὸ παντὸς σημείου ἐπὶ πᾶν σημεῖον εὐθεῖαν γραμμὴν ἀγαγεῖν”). The fact that any two points in the plane $\mathbb{R}^2$ are connected by a line is equivalent to the robust division principle, which is not provable constructively. $\endgroup$
    – Gro-Tsen
    Commented Feb 23 at 12:25
  • 2
    $\begingroup$ First postulate aside, going through Euclid's Elements, it's often hard to decide whether the statement is “constructively valid”, because even thinking classically Euclid is a bit careless about stating when points are supposed to be distinct and such stuff, so we can probably make pretty much everything valid by sprinkling “apart” fairy dust whenever he speaks of two points and such. But is this cheating? $\endgroup$
    – Gro-Tsen
    Commented Feb 23 at 12:53

3 Answers 3

Reset to default
18
$\begingroup$

According to Wikipedia, in 5th century BCE, Bryson of Heraclea spoke of a special case of the intermediate value theorem. If we're very generous, that would be an early occurrence of a constructively invalid theorem, although in the particular case of Bryson of Hearclea, the function under consideration is a specific one, and it can easily be seen to achieve intermediate values.

A fully non-constructive version of the intermediate value theorem (still relying on Wikipedia) was shown in 1817 by Bernard Bolzano, so let's run with that.

Rolle's theorem is non-constructive and dates back to 1691. (Rolle only considered poylnomials, but even then the theorem fails constructively, see Will Swain's comments below.)

The fundamental theorem of algebra goes back to 1608, but once again it took time to get the formulation correct and to prove it. And of course Fred Richman showed how to constructivize the theorem.

There is a pattern here. Someone, a long time ago, had an inkling to state a special case of a non-constructive theorem, or perhaps an inexact or incorrect version of the theorem. The special case has a constructive proof, but the general one does not. However, the general theorem often can be rephrased in a classically equivalent form that is constructive. I am afraid it's very easy to move the goalpost in the present situation.

Improve this answer
$\endgroup$
11
  • 1
    $\begingroup$ The solution to $f'(c)=0$ can't be made into a continuous function in the coefficients of $f$ in a neighborhood of a constant polynomial. On the interval $[-1,1]$ the polynomial $ax^2 + b (x^3-x)$ has derivative $2ax + b (3x^2-1)$ which for $|a|> |b|$ has a unique root in $[-1,1]$ which is some nonconstant function of $a/b$ and thus not continuous as a function of $(a,b)$ around $(0,0)$. So doesn't that mean it's not constructive? $\endgroup$
    – Will Sawin
    Commented Feb 22 at 19:41
  • $\begingroup$ @WillSawin: That's a common trap. By the same reasoning the statement "above every real there is an integer" would have to be non-constructive because there's no continuous map $f : \mathbb{R} \to \mathbb{Z}$ satisfying $f(x) > x$ for all $x$. (What you should try to do instead is: assuming $f'(c) = 0$ always has a solution, construct a discontinuous map.) $\endgroup$
    – Andrej Bauer
    Commented Feb 22 at 19:47
  • $\begingroup$ I am staring at the graph of the zeroes of the derivative of $a x^2 + b (x^3 - x)$ (parametereized by $(a,b)$) but I can't see how to extract a discontinuous map in the neighborhood of $(0,0)$. Can you? $\endgroup$
    – Andrej Bauer
    Commented Feb 22 at 20:11
  • 2
    $\begingroup$ If one writes $a = t^2+u^2, b=u^2$ then there is a unique solution for all $t,u$ except $(0,0)$ but that unique solution is not continuous at $(0,0)$. However, the solution at $(0,0)$ is still not unique, so it's not quite a map. $\endgroup$
    – Will Sawin
    Commented Feb 22 at 20:15
  • 3
    $\begingroup$ Just running quickly through the text on the surface without understanding it, it looks like in the examples he gives the polynomials have integer coefficients, which probably fixes things. $\endgroup$
    – aws
    Commented Feb 23 at 10:27
7
$\begingroup$

A somewhat different type of example, not as early as the ones in Andrej Bauer's answer, but perhaps a bit more resistant to "moving the goalposts," is an ineffective result in number theory.

For example, Thue's theorem says that if $f$ is an irreducible bivariate form of degree at least 3 over the rational numbers, and $r$ is a nonzero rational number, then the equation $f(x,y) = r$ has only finitely many integer solutions. Thue's original proof in 1909 was ineffective (I think the ineffectivity can be traced to the mean value theorem, so this is related to the Rolle's theorem example mentioned by Andrej Bauer).

As for goalpost-moving, Thue's theorem is now effectively solvable, because of theoretical advances since Thue's time. But there are other results in this area that remain ineffective. I believe that another way to move the goalposts is to rephrase the theorem as stating that the number of solutions is "not infinite." In spite of these caveats, these number-theoretic results have the merit that even thoroughly classical mathematicians understand immediately that there is something fundamentally nonconstructive about them. I think that it helps that these results are "discrete" rather than "continuous." By contrast, if you cite Rolle's theorem or the fundamental theorem of algebra, then you'll have to work fairly hard to get the typical classical mathematician to understand exactly what's "nonconstructive" about it.

Improve this answer
$\endgroup$
5
  • $\begingroup$ That's 1909? We can probably find earlier examples in algebra, such as Hilbert's Nullstelensatz from 1893? $\endgroup$
    – Andrej Bauer
    Commented Feb 23 at 11:52
  • 1
    $\begingroup$ @AndrejBauer Was Hilbert's proof nonconstructive in the sense being discussed here? I've never looked into this carefully. I know people often say that it was nonconstructive, but I don't know if they just mean that the proof doesn't give an explicit procedure for computing the polynomial(s) of interest. Also, if the question is about results that cannot be proven constructively (as opposed to were not proven constructively at first), I think the Nullstellensatz does not qualify. $\endgroup$
    – Timothy Chow
    Commented Feb 23 at 14:04
  • $\begingroup$ I should referesh my memory. Perhaps I am thinking of Hilbert's basis theorem. There is an "effective" Nullstellensats, that's true. $\endgroup$
    – Andrej Bauer
    Commented Feb 23 at 17:50
  • $\begingroup$ @AndrejBauer Colin McLarty's paper, Theology and its discontents: The origin myth of modern mathematics, has some relevant information (see pp. 9-10 in particular), though maybe not enough to settle the matter. $\endgroup$
    – Timothy Chow
    Commented Feb 23 at 22:57
  • 2
    $\begingroup$ @AndrejBauer I just looked at A Course in Constructive Algebra. From a modern perspective, Hilbert's basis theorem is a theorem about Noetherian rings. But there are various possible definitions of a Noetherian ring that are equivalent classically but inequivalent constructively. If we choose the "right" definition then there is a constructive proof of Hilbert's basis theorem. But now we surely have moved the goalposts, and haven't said whether Hilbert's original proof was nonconstructive. $\endgroup$
    – Timothy Chow
    Commented Feb 24 at 1:04
-2
$\begingroup$

IIRC "If two angle bisectors of a triangle are congruent, then the triangle is isoscles." is a theorem that has only been proven non-constructively.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I don't know whether or not it is known that this can fail constructively (which surely depends on what "constructively" means), but the question says "just saying that there is no known constructive proof doesn't count." $\endgroup$
    – LSpice
    Commented Feb 23 at 11:45
  • 4
    $\begingroup$ Please provide a reference for your claim. My immediate reaction is this: equality of reals is $\neg\neg$-stable, so it suffices to show that if one of the bisectors is shorter than the other, then the triangle is not isosceles – and that's going to be a constructive proof. In other words, I don't believe you :-) (Might you perhaps be conflating "has a proof by contradiction" with "does not have a constructive proof"?) $\endgroup$
    – Andrej Bauer
    Commented Feb 23 at 11:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .