When is proof by contradiction necessary?

It’s been a while since I have written a post in the “somewhat philosophical” category, which is where I put questions like “How can one statement be stronger than an another, equivalent, statement?” This post is about a question that I’ve intended for a long time to sort out in my mind but have found much harder than I expected. It seems to be possible to classify theorems into three types: ones where it would be ridiculous to use contradiction, ones where there are equally sensible proofs using contradiction or not using contradiction, and ones where contradiction seems forced. But what is it that puts a theorem into one of these three categories?

This is a question that arises when I am teaching somebody who comes up with a proof like this. “Suppose that the sequence is not convergent. Then … a few lines of calculation … which implies that . Contradiction.” They are sometimes quite surprised when you point out that the first and last lines of this proof can be crossed out. Slightly less laughable is a proof that is more like this. “We know that . Suppose that . Since the derivative of has absolute value at most 1 everywhere, it follows that , which is a contradiction. Therefore, .” There, it is clearly better to work directly from the premise that via the lemma that to the conclusion that . However, the usual proof of the lemma does use contradiction: one assumes that the conclusion is false and applies the mean value theorem.

The result of all this is that I don’t have a good tip of the form, “If your theorem is like this then try a proof by contradiction, and otherwise don’t.” For the remainder of this post I’ll discuss another couple of examples that show some of the complications that arise.

EDP13 — quick summary

I don’t have any major new themes to talk about in this post. We are continuing to look for ways of decomposing matrices that would give rise to proofs of strengthenings of EDP, but I would say that at the moment we are still at the stage of trying to get a feel for the problem. (If you are reading this and wondering what the decomposition problems are that I am talking about, then I suggest having a look at EDP10 and EDP12.)

The difficulty we face seems to be this. (I do not have full confidence in what I am about to write. It could be that I will change my mind, and it could be that others already have a different and better analysis.) I’ll take for the purposes of illustration the problem of writing a diagonal matrix with unbounded trace as a sum where the and are HAPs and . After trying a few things, I have started to feel as though it isn’t going to be easy to find a completely explicit construction for this. That is partly because no pattern has jumped out at me from the output from Moses’s experiments, though I have not looked as hard as I might. So the best I can think of to do at the moment is something like this (but almost certainly not precisely this).

1. By some kind of wild guess, choose some HAPs and some positive constants .

2. Form the matrix , which has trace .

3. Make those choices in such a way that is significantly larger than .

4. Prove that it is possible to cancel out the off-diagonal part of this matrix and at most half the diagonal part by subtracting a sum of the form , with also significantly smaller than .

“Hello World!”

As anyone who has been following the discussion of EDP will be aware, I am interested in programming, but have until very recently favoured an extremely high-level language called BLOG. The principle of this language is that you describe in English in a blog post or comment what you want an algorithm to do, after which a probabilistic process operates. At the end of this process, if you are lucky, your description gets translated into a language that a computer can understand and the algorithm is implemented. The amazing thing is that one often is lucky. I believe that BLOG is closely related to a language called GRADSTUDENT that various mathematicians have used in the past. (My attention was drawn to the latter language on some blog or other, possibly even this one, but I can no longer find the reference.) [It has now been supplied to me.]

However, BLOG and GRADSTUDENT have certain disadvantages. One is that one does not have complete control over what one is doing. Another is that one feels slightly guilty using it. I have recently decided that it is high time I learnt to program in a more traditional language, and last week I went to a short course put on by the Cambridge computer science faculty called “C for absolute beginners”.

EDP12 — representing diagonal maps

In this post I want to use my unfair advantage as host of this blog to push an approach that is the one that I am currently most interested in. So let me precede it with the qualification that although I shall present the approach as favourably as I can, it may well be that Moses’s SDP approach or Gil’s polynomial approach will in the end turn out to be more fruitful. I should also add that this new approach makes use of a crucial insight from the SDP approach, which is the idea that one can prove a result about all sequences , including our troublesome friend 1, -1, 0, 1, -1, 0, … if we bound the discrepancy below by an expression of the form .

Lewis’s theorem

Before I explain the new result, I’d like to discuss a result from the geometry of Banach spaces. (I don’t need to do this, but it is a very nice result and this is a good excuse to write about it. If you just skim this section and take note of the definition of “well spread out” below, that will be enough to follow the rest of the post.) The result is a special case of an important theorem of Dan Lewis, though the proof that I shall sketch is a little different from Lewis’s.

EDP11 — the search continues

I do not have too much to say about the new programme to use SDP to solve EDP, other than that it is still being actively pursued. One remark I would make is that I have rather forgotten recently about keeping the wiki updated, and SDP is a major omission from it. It would be good to have a theoretical account of the method (which I suppose I could paste quite easily from one of my existing posts), and an experimental page devoted particularly to data connected with this approach, with links to all the matrices, sequences and plots that have been produced.

So far, the data has had some expected features (such as the sequence values tending to be larger when is smooth) and some puzzling ones (such as the fact that is much much larger than ). An initial hope for the method was that the experimental data would give rise to a very precise conjecture, but so far that has not happened. There are, however, various avenues that have not been fully explored, and I still have some hope that we will suddenly stumble on some data that we can fully understand.

EDP10 — a new and very promising approach

From time to time, there has been an input into this project that has given rise to a burst of optimism (on my part anyway). Perhaps the first was the rapid discovery of very long sequences with low discrepancy, and especially the fact that these sequences had interesting structure to them. (The length led me to hope that the conjecture might be false, or at the very least that it might be possible to construct sequences with extremely slow-growing discrepancy, and the structure led me to hope the opposite.) I’m probably forgetting a few things, but the next one I remember is Terence Tao’s amazing observation that we could restrict attention to multiplicative functions if we were prepared to change the problem very slightly. We then discovered (though we sort of knew it anyway) that multiplicative functions are not easy objects to understand …

Since I posted EDP9, there has been a development that has radically changed my perception of the problem, and I imagine that of anyone else who is following closely what is going on. It began with this comment of Moses Charikar.