19
$\begingroup$

I've recently been learning about non-classical logics and skepticism regarding the law of excluded middle.

This has been hindering by progress in classical mathematics because it's made me slightly depressed when doing proof by contradiction.

I am basically looking for reason to continue using this proof technique and continuing my study of classical mathematics.

Update: After viewing This math overflow thread, and discussion relating to top answers on this question, my concerns have essentially been solidified. My only motivation for doing classical mathematics now is that classical mathematics can give us new research areas / theorems to explore, but ultimately, this is only before they are transformed into a constructive version, and applied elsewhere, in 99% of cases.

$\endgroup$
5
  • $\begingroup$ Comments have been moved to chat; please do not continue the discussion here. Before posting a comment below this one, please review the purposes of comments. Comments that do not request clarification or suggest improvements usually belong as an answer, on Mathematics Meta, or in Mathematics Chat. Comments continuing discussion may be removed. $\endgroup$
    – Xander Henderson
    Apr 5 at 17:23
  • 1
    $\begingroup$ Have you considered that most proofs by contradiction can be converted to using the contrapositive? Have you considered that a theorem proved by contradiction is still true so its results are applicable everywhere they would be if the proof had been more to your liking? $\endgroup$
    – John Douma
    Apr 6 at 16:47
  • $\begingroup$ @JohnDouma have you considered the possible un-soundness of mathematics? Non-constructive proofs that cannot be converted to constructive ones pose questions $\endgroup$
    – Fraser Pye
    Apr 7 at 0:15
  • 2
    $\begingroup$ @FraserPye That's ridiculous. $\endgroup$
    – John Douma
    Apr 7 at 2:08
  • $\begingroup$ @FraserPye, the issue of soundness/unsoundness is not an issue that separates classical from intuitionistic mathematics, because there are equiconsistency results between them. $\endgroup$ Apr 7 at 9:36

6 Answers 6

26
$\begingroup$

I assume that software development counts as sufficiently distinct from mathematics.

The correctness of algorithms are often proved by contradiction. For an algorithm to be correct, we need to show that it produces a correct output for all valid inputs. This can be done by supposing there is some input with a wrong output, and then reaching a contradiction. This is often easier than a direct proof, because

  • We get to make a stronger assumption (that the input is valid and the output is not), and
  • The goal is to derive any contradiction, rather than just the specific statement that the output is correct.

Furthermore, the lack of constructivity is no issue. We don't need a proof that shows the algorithm is correct and that some concrete object satisfying some property exists. We just want to know that the algorithm is correct.


Consider also a proof that an algorithm is incorrect, i.e. a proof that some valid input exists for which the output is incorrect. If this proof is constructive then we can use the concrete counterexample to write a test case, which will be useful for testing the software after attempting to fix the bug. The concrete counterexample might also be useful for stepping through the algorithm with a debugger, in order to find the exact point at which the algorithm "goes wrong" and hence understand the bug. So a constructive proof is definitely preferable here.

On the other hand, even a non-constructive proof (i.e. a proof that the algorithm is incorrect, but without exhibiting a concrete input which it fails on) can still be enlightening, since we can see which features or parts of the algorithm are used in the proof, and that could help to isolate the bug to one of those features or parts. And a proof at all is useful for telling us that a bug definitely exists (and work is needed to address it), which we wouldn't know otherwise.


I realise that the above argument in favour of proofs by contradiction is, ironically, non-constructive, since I didn't provide any specific algorithm which is easier to prove (or refute) by contradiction. However, the question as written asks for "reason[s] to continue using this proof technique", which I believe I have provided.

I've also referred only to algorithms which are "easier" to prove by contradiction, rather than those which "have only been" proved by contradiction. However, the nature of software development is that one often comes up with an algorithm for a particular purpose (which might be based on a standard algorithm, but nonetheless needs justification), and then the developer's proof of that algorithm is the only one written for that specific algorithm. Hence if they prove it by contradiction, it will have only been proved that way.

$\endgroup$
16
  • $\begingroup$ Do you happen to have a link to a worked example of an algorithm being proved correct by contradiction? $\endgroup$
    – Eugene
    Apr 3 at 22:32
  • 3
    $\begingroup$ @Eugene Here's an example of a proof by contradiction for Prim's algorithm (which finds a minimum spanning tree of an undirected graph). Here's one for breadth-first-search (which finds distances in an unweighted graph). These are famous algorithms so there will be many proofs by other methods, of course. $\endgroup$
    – kaya3
    Apr 3 at 22:48
  • 2
    $\begingroup$ A lot of questions in computer science are decidable (in a constructive sense) to begin with. That Prim's Algorithm example doesn't need full LEM. The question "is S minimum weight" is decidable, since there are a finite number of trees and therefore a finite number of possible weights, so even a constructivist would accept that proof. $\endgroup$ Apr 4 at 0:09
  • $\begingroup$ @SilvioMayolo Sure, but the question isn't only about whether LEM is really needed to do mathematics; it's about whether proofs by contradiction are applicable outside of mathematics. I already said there are proofs by other methods for these algorithms. $\endgroup$
    – kaya3
    Apr 4 at 0:12
  • 2
    $\begingroup$ @FraserPye: For many algorithms, particularly of the divide-and-conquer type, a constructive proof may be somewhere between very hard and impossible to write. Most proofs for such algorithms use infinite descent, and it is not immediately obvious how you would rewrite such a proof to avoid the use of infinite descent or an equivalent technique that also tacitly relies on LEM. Computer scientists typically do not care about constructivism for these proofs, so you probably won't find such proofs in the literature, either. $\endgroup$
    – Kevin
    Apr 5 at 16:53
18
$\begingroup$

In 1964, Hohenberg and Kohn proved by contradiction that the ground-state energy of a molecule or material is (up to a constant) a unique functional of its density $\rho$. This is surprising: the ground-state energy is the minimal eigenvalue of the time-independent Schrödinger equation $H \lvert \Psi \rangle = E \lvert \Psi \rangle$, and the wavefunction $\lvert \Psi \rangle$ is 3$N$-dimensional, where $N$ is the number of electrons. It is also quite powerful: $\rho$ is a spatial density, three-dimensional for any $N$.

This theorem is not strictly "within mathematics", and it is also not especially deep or complicated. The universal functional it prescribes remains unknown sixty years later. But it almost instantly (bolstered by a workable approximation developed just one year later) created the field of density functional theory, which is one of the most popular methods for electronic structure in chemistry and materials science.

$\endgroup$
0
17
$\begingroup$

The Penrose-Hawking singularity theorem in astrophysics (and therefore "outside mathematics") was proved using nonconstructive techniques relying on classical logic (and the law of excluded middle). This was pointed out by historian Geoffrey Hellman. For a related study, see

Katz, K.; Katz, M. "Meaning in classical mathematics: Is it at odds with Intuitionism?" Intellectica 56 (2011), no. 2, 223-302. https://arxiv.org/abs/1110.5456 and https://www.persee.fr/doc/intel_0769-4113_2011_num_56_2_1154

$\endgroup$
7
  • $\begingroup$ I’m not sure if this is the same thing that you refer to (I don’t know enough to judge), but near the end of Bryce DeWitt’s review of The Large Scale Structure of Space-Time by Hawking/Ellis [Science (N.S.) 182 #4113, 16 November 1973, pp. 705−706] (JSTOR) DeWitt criticizes a proof in Hawking/Ellis (on pp. 249−251) for making use of Zorn’s lemma, with DeWitt ending with: (continued) $\endgroup$ Apr 3 at 11:56
  • 1
    $\begingroup$ The physicist’s job is not done until he can show, by an explicit algorithm or construction, how one could in principle always select a member from every such set of developments. Failing this he has proved nothing. See also this mathoverflow answer. Three papers that deal with this issue are (there are other papers, but these three seemed to me the most relevant when I was briefly looking into this issue a few months ago): (continued) $\endgroup$ Apr 3 at 11:56
  • 4
    $\begingroup$ @DaveL.Renfro, You are certainly right: other nonconstructive aspects of classical mathematics are also routinely used in physics, and not merely the law of excluded middle. An example would be the notion of a Calabi-Yau manifold, which is fundamental in certain branches of theoretical physics. To prove the existence of such manifolds, one uses high-level PDE techniques that certainly rely on ZFC and classical logic (this example was also mentioned in the article in intellectica that I linked in my answer). $\endgroup$ Apr 3 at 11:59
  • 5
    $\begingroup$ It could be that the physicists' work is "not finished" until they produce a more constructive proof; nevertheless, they do seem to use nonconstructive techniques in a routine fashion. @DaveL.Renfro $\endgroup$ Apr 3 at 12:05
  • 1
    $\begingroup$ @FraserPye, As you point out, this depends on which the area of physics you are in exactly. If you work with Calabi-Yau manifolds, you are certainly using the ZFC background (+classical logic) routinely. $\endgroup$ Apr 4 at 11:16
16
$\begingroup$

Does "$\forall x : \mathbb{R} . \ x \geq 0 \lor x \leq 0$" count as a theorem? This is not provable constructively (it's equivalent to LLPO), but is used freely by physicists and computer scientists the world over. In fact, if you ask the people who are really working with "applications", like the biologists and engineers for instance, I guarantee you that they'll ask you what's the use of your math that doesn't allow dichotomy of $\leq$!

Just because there are constructive versions of lots of interesting theorems (usually under some extra definability conditions on the inputs) doesn't mean that the "nonconstructive" results aren't worthwhile! And this is coming from someone who spends a lot of time thinking about constructive math. See this recent blog post, for instance, or any number of my answers on this website. I try quite hard to make my proofs constructive whenever possible, provided it doesn't overcomplicate exposition. All that to convince you it's not defensiveness or a dislike of constructive math that makes me say: Frankly, your question comes off as quite immature (not to mention dismissive of "regular" mathematicians). I'm sure that's not your intent, it's just something to be aware of.

Going back to the mathematics, these extra definability conditions can be really hard to pin down! It wasn't until quite recently that an algorithm for computing gröbner bases (which was already used in practice!) was actually proven to always terminate. Moreover, as you'll find by just searching for "contradiction" in the linked pdf, this proof crucially uses classical logic in multiple places (not to mention casework, which almost certainly violates LEM, but I haven't checked). Again, the actual practitioners (by which I mean the software engineers developing mathematica, sage, etc) don't care at all about constructive versus classical proofs! Now, of course, some version of the correctness of this algorithm is almost certainly provable constructively. But I highly doubt anybody knows what the right definability conditions on the ideals should be! Also, in case you doubt the utility of this algorithm, you should know that gröbner bases are roughly the analogue of gaussian elimination for arbitrary systems of polynomials. There's a reason that the mathematica team was so eager for a more efficient algorithm!

More concerningly still, constructively the notion of "finite" breaks down entirely. Indeed, quoting from Blass's An induction principle and pigeonhole principles for k-finite sets:

THEOREM $4$. Assume that, for all finite $X$ and all $f : X+1 \to X$, there exist $x$ and $y$ in $X+1$ with $f(x) = f(y)$ but $x \neq y$. Then the law of the excluded middle holds

The pigeonhole principle, I'm sure you'll agree, is used constantly in applications. For transparency, I should say that the pigeonhole principle is constructively provable if $X$ has decidable equality, but I guarantee you that people working in applications absolutely don't consider this subtlety.


Lastly, I actually have a question for you (and I'm sincerely interested in your answer!): What do you think of the various ways one can nonconstructively show that a constructive proof exists (though we may not be able to produce such a proof)?

For example, Robertson-Seymour prove that for each graph $H$ there exists an algorithm taking in a graph $G$ and deciding whether $H$ is a minor of $G$ (indeed, the algorithm runs in time $O(|G|^3)$!). However, their proof is nonconstructive, and for even quite simple $H$ we have no idea what this algorithm is!

In your mind, does this count as a constructive result? The algorithm is certainly constructive... And we know an algorithm exists... We just can't get our hands on it!

Similarly, how do you feel about theorems like the following: "If $\varphi$ is a geometric formula which is classically provable, then $\varphi$ is also constructively provable". This theorem is, itself, nonconstructive (since it relies on the completeness theorem for topos semantics), but it asserts the existence of a constructive proof. Would you consider $\varphi$ "constructively true" for your purposes?


I hope this helps ^_^

$\endgroup$
17
  • 1
    $\begingroup$ I really like the first half of this answer, but I find the stuff below the line very confusing. Proving that "$X$ is provable" is not sufficient to conclude $X$, even classically, much less constructively. $\endgroup$
    – Z. A. K.
    Apr 5 at 8:57
  • 3
    $\begingroup$ Personally, and assuming I understand the example, this is exactly the sort of reason that I think classical computability and the effective topos are fundamentally flawed from the perspective of caring about having a mathematics where all the results allow computing actual answers/examples. I suspect the majority of computability arguments would still go through, but these, "solved by an unknowable algorithm," results are exactly the ones I don't want. $\endgroup$
    – Dan Doel
    Apr 5 at 17:40
  • 1
    $\begingroup$ @DanDoel -- I think that's a perfectly reasonable stance! I much prefer having an actual constructive proof-in-hand compared to merely knowing a constructive proof exists. Of course, I also think it's a cute party trick to be able to prove constructive theorems nonconstructively :P $\endgroup$ Apr 5 at 20:30
  • 1
    $\begingroup$ @HallaSurvivor I am still skeptical about how you "know the algorithm exists". What if it doesn't? If you really question what you "know" you will realize that you don't really know anything for certain. It's a facet of the universe, we live in mystery, I will believe it when I see it. $\endgroup$
    – Fraser Pye
    Apr 5 at 22:04
  • 1
    $\begingroup$ @HallaSurvivor: Thanks for engaging. Sorry for being unclear in my previous comment. I understand Barr's thm & the completeness results for geometric logic, that's not the part confusing me. I'm confused by you going from "a constructive proof of $\varphi$ exists" to asking whether OP would consider "$\varphi$ constructively true" . A yes answer to this question cannot be mathematically reasonable, and this has nothing to do with constructivism: even going from "I have shown that there is a proof of $\varphi$" to "I have shown that $\varphi$ holds", without any adjectives, is not reasonable.1/ $\endgroup$
    – Z. A. K.
    Apr 6 at 1:57
5
$\begingroup$

True proof by contradiction is captured by the deductive rule ( ( ¬A ⇒ ⊥ ) ⊢ A ), which allows you to deduce A if you can deduce that ¬A implies a contradiction. Besides your chosen axioms, this rule is essentially the only non-constructive assumption you need in your foundational system for mathematics. It is equivalent over the other (constructive) deductive rules to LEM (excluded middle). I mention this because viewing the issue using LEM instead of proof by contradiction (despite being equivalent) is helpful for furnishing many natural examples. Some of my examples below are indeed literal instances of LEM.

Hex has a winning strategy for the first player

The (currently known) proof that the first player has a winning strategy has two parts:
  (1) The second player has no winning strategy.
  (2) At least one player will win.
Although the proof of (2) is constructive, the proof of (1) is not, and hence the proof of the full theorem is not constructive either. Till today, nobody knows a winning strategy for the first player, and it is infeasible to compute it even though it is in theory possible, since the number of possible game plays is astronomically gigantic.

Brouwer's fixed-point theorem

This theorem is non-constructive in an essential way; there is a computable continuous operator on the unit square that has no computable fixed-point! Hence any proof of this theorem must be non-constructive!

This theorem is also an easy consequence of the Borsuk-Ulam theorem, which implies that the latter theorem also cannot be constructively proven. And that latter theorem implies that an ideal teddy bear covered completely with fur cannot have its fur combed completely flat. Is that application enough?


From here on we consider programs in a fixed Turing-complete programming language.

The halting problem is well-defined

Given any program P and input X, either P halts on X or P does not halt on X. Well? Do you agree? If you do, then you must have used a non-constructive proof! The reason is simple; there is no program to compute the answer from P,X.

I think this fact is concrete enough that it should be accepted just for its own intrinsic meaning.

Kolmogorov complexity is well-defined

For every string X, there is a minimum m∈ℕ such that some inputless program of length m outputs X. Isn't this obviously true? But if you want to prove it, you would necessarily need a non-constructive proof. The reason is that if you have a constructive proof, then you can construct a program K that computes this m from X, and construct an inputless program S that outputs the (length-lexicographically) first string Y such that K(Y) > length(S), which must exist since there are only finitely many possible outputs by programs of each length. Note that S can obtain its own length, by the standard quine technique. But then length(S) ≥ K(Y) by definition of K, which is impossible.

Why is Kolmogorov complexity relevant outside Mathematics? We like to have good compression algorithms, and in a very precise technical sense Kolmogorov complexity is a lower bound on compression (up to a constant additive factor). And this theorem tells us that there is absolutely no systematic way to obtain the best compression possible, even in principle.

Minimal plane-tiling extensions of Wang tile sets exist

Given any set T of Wang tiles, there is a minimum number c of Wang's special 11 tiles (for an aperiodic tiling) that need to be added to T to get a set that can tile the plane. But there is no non-constructive way to prove this, otherwise there would be a program that solves the halting problem.

This fact is extremely concrete and is not directly expressing any computation-related statement.

$\endgroup$
4
  • $\begingroup$ Now that I think of it, the halting problem is proven by contradiction yes, which now makes me skeptical. $\endgroup$
    – Fraser Pye
    Apr 4 at 21:57
  • 3
    $\begingroup$ @FraserPye: Anyone can be skeptical of anything. It doesn't change the facts. The real world continues existing and obeying classical FOL whether you like it or not. And so other people who use classical FOL will continue to deduce truths about the real world starting from true assumptions, again whether you like it or not. As Pilcrow said, your ability to use this website is due to an incredible amount of physics, engineering and computer science, all of which has been built by people based on classical FOL. $\endgroup$
    – user21820
    Apr 5 at 2:02
  • 3
    $\begingroup$ The halting problem theorem is not proved 'by contradiction.' It is a constructive proof of a (partially) negative statement. "For every Turing machine $H$, there (constructively) exists a Turing machine $M$ and input $I$ such that $H$ does not report the halting behavior of $M(I)$." $\endgroup$
    – Dan Doel
    Apr 5 at 5:36
  • $\begingroup$ @DanDoel: Indeed. Note also that FP conflated "halting problem answer" with "halting problem unsolvability". The former is a non-constructive object, whereas the latter (as per your comment) is a constructive theorem. $\endgroup$
    – user21820
    Apr 5 at 5:58
2
$\begingroup$

Every area of math has a set of underlying assumptions. Which assumptions you choose will determine which conclusions can be derived.

As an example consider, Euclidean geometry assumes parallel lines never cross. Many students never learn about non-Euclidean geometry. When they do learn about non-Euclidean geometries, it doesn't make Euclidean geometry invalid. Because the initial assumptions differ, this creates a divergence into two or more entirely different spheres of math. Indeed, many would say Euclidean geometry seems to be the most broadly applicable geometry. This despite the fact that other geometries which break Euclidean underlying assumption(s) have existed for hundreds of years. Euclidean geometry describes classical physics perfectly well. However, to grasp relativity non-Euclidean geometries become essential.

  • Each sphere has its use and applications.*

The set of assumptions chosen should be appropriate for the practical application or context to which one hopes to apply the results.

$\endgroup$
2
  • $\begingroup$ Feel free to correct or clarify my definitions. Instead of parallel lines I should use the parallel postulate. $\endgroup$
    – nickalh
    Apr 4 at 10:15
  • 2
    $\begingroup$ You wrote "The set of assumptions chosen should be appropriate for the practical application or context to which one hopes to apply the results" but this is precisely the OP's question: is classical logic appropriate for applications? Your answer does not address the issue. $\endgroup$ Apr 4 at 15:30

You must log in to answer this question.

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