This isn’t a proof by contradiction

A short rant on bad proofs.

Recently I came across a proof concerning orthonormal basis of the following theorem (don’t worry if you know nothing about it):

Theorem. Let V be a vector space with inner (dot) product \langle\cdot,\cdot\rangle. Let B = \{b_1,\ldots,b_n\} be an orthonormal set of vectors, i.e. the vectors are pairwise orthogonal of norm 1. Then this set is linearly independent.

The proof I read goes as follows:

Proof Assume by contradiction, that B is not linearly independent. This means that there is a non-zero solution \alpha_1, \ldots, \alpha_n to the equation

    \[\sum_{i} \alpha_i b_i = 0\]

. However, this means that for every i=1,\ldots,n we have

    \begin{align*}0 &= \langle 0, b_i\rangle \\ &= \langle\sum_j \alpha_j b_j, b_j\rangle \\ &= \sum_j \alpha_j\langle b_j, b_i\rangle \\ &= \alpha_i\langle b_i, b_i\rangle \\ &= \alpha_i\end{align*}

However, we assumed that \alpha_i are non-zero, but we just showed that they must be zero. This is a contradiction with our assumption, hence the assumption is wrong, so \alpha_i must be zero. \qed

You can read the original proof here, it’s the same, but with more details on why the equalities here hold, which this is irrelevant for this post.

You might already see that something is odd here, especially given the title of this post. How is this exactly a proof by contradiction? Well, in the end we got a contradiction with the assumptions, so technically it is proof by contradiction. However, it is practically a very direct proof. Where did we use the assumption? It wasn’t useful by any means. We had some statement p that we wanted to prove, so we assumed \neg p, then showed that p holds, and then concluded that it cannot be that p\wedge \neg p, hence p. It’s quite a mental gymnastics here, don’t you agree?

This example may seem artificial, but you can clearly see that I didn’t come up with it on my own. I claim that this pattern can be seen often in the wild, especially when students are presenting proofs on the tutorials.

Example of a good proof by contradiction

A very well known and simple example is the proof that \sqrt{2} is irrational. In other words, the theorem states that there are no integers p, q\neq 0 such \sqrt{2} = \frac{p}{q}.

Proof. Assume by contradiction that there are integers p, q\neq 0 such that \sqrt{2} = \frac{p}{q}. We may assume without loss of generality, that p and q are coprime. Then we have a sequence of equivalent equalities:

    \begin{align*}\sqrt{2} &= \frac{p}{q} \\ 2q^2 &= p^2 \\ q^2 &= 2{p'}^2 \end{align*}

where p’ is \frac{p}{2}. This is an integer as well, by the Euclid’s lemma. So, by the same lemma we get that q must be divisible by 2, which is a contradiction with our assumption, that p and q are coprime. \qed

Notice that in this proof we’re actually leveraging the assumption, which wasn’t the case in the former theorem.

What is a proof by contradiction?

Disclaimer. This section is very technical and formal. This may be hideous to some readers. If you despise formal logic and hate Bourbakists, then skip this section for your own sake. I try to formalize what is a proof and why we actually can do a proof by contradiction.

Let’s first establish what is a proof. I don’t want to get in to much details, as this isn’t particularly engaging topic (check out my notes from Logic R if you are interested in a very formal and technical definition). In our case, we can think of a proof of a statement \phi with assumptions T as a sequence of sentences \phi_1,\ldots,\phi_n = \phi, where a sentence must be an assumption from T, a tautology, or be concluded directly from some previous statements in the proof. If there exists a proof of \phi assuming T, then we say that T proves \phi, which is often written as T\vdash\phi.

A proof by contradiction is an approach of proving rather than a technical term. I’ll try to formalize this with so called deduction theorem. It states that if we show that T proves \phi\rightarrow\psi, then T\cup\{\phi\} proves \psi and vice versa. This is again a technical theorem to formalize the fact that if we want to prove an implication A implies B we may simply assume A and then prove that B must hold.

Let’s say we want to prove some theorem \phi. To show that \phi is true, we could show that the following implication is true: \neg\phi\rightarrow\bot (where \bot is basically false, you could interpret it as a sentence x\neq x, which is always false). We could do that as (\neg\phi\rightarrow\bot) \leftrightarrow \phi. So, every proof by contradiction has the following scheme: First prove that T\cup\{\neg\phi\}\vdash\bot, by deduction theorem T\vdash\neg\phi\rightarrow\bot. Thanks to modus ponens we can then extend the proof of this implication and finally show that T\vdash\phi.


I like tidy and deliberate proofs. I also like when a presenter of a solution to some problem on the blackboard gives the viewers a nice and enjoyable experience. This post provides an example of one of the common shortcomings in presenting proofs. It’s not faulty reasoning, but it’s unnecessary and could be simplified and organized at a low cost. I try to pay attention to the preciseness and cleanliness of my solutions. If you ever see me presenting and saying something in a bad fashion, then please don’t mind telling me that!

Story of a bug

Debugging is of course a major part of programming. Arguably most of the time it’s not the most satisfying part of the job, it’s an unfortunate necessity rather than the goal itself. Moreover, I think that most of the bugs I make aren’t interesting (e.g. typos, wrong usage of a library function, nullptr dereferences, off-by-one errors etc.). But sometimes, on rare occasions, one can stumble upon a subtle and sophisticated bug. Resolving such a bug brings true catharsis, gives massive satisfaction and is the ultimate learning experience.

I want to share a story about a man who was staring at the screen with no clue of what was happening, but finished with the great joy of resolving a problem that improved my engineering skills and opened a new dimension of thinking about multithreaded programs. Okay, I know, I got a little bit carried away and perhaps exaggerated. However, I hope that you will feel at least a little impressed by the end of the article.

Continue reading “Story of a bug”

Why I’ve spent my Easter break customizing Neovim

Greeting screen

Alright, so you might think that there are better ways to spend your Easter break than sitting all of your evenings customizing Neovim with no prior knowledge. You’re probably right. Sceptics may also say that I’ve reproduced VSCode instead of simply using it. They are also probably right. Or are they? ­čĄö

Continue reading “Why I’ve spent my Easter break customizing Neovim”

What is this blog about?

For some time I had this need to somehow share my thoughts with the outer world. I have a tendency to overwhelm people I talk with, so I decided to create this webpage. If you want to read some of my articles then I hope you may find something interesting or valuable. If you want to know more about me, then had to the Projects and About me pages.

I highly encourage you to leave your thoughts on my writing in the comments, they are accessible without registration.

Also, I’ve decided to run this page mainly in English, some posts may be in Polish though (which is my native language).

Have a great day ­čÖé

Claude Monet – Woman with a Parasol ÔÇô Madame Monet and Her Son

Wyra┼╝enia regularne a algorytm Floyda-Warshalla

Kr├│tka notatka o fajnym po┼é─ůczeniu mi─Ödzy dwoma ┼Ťwiatami

Na jednych z pierwszych zaj─Ö─ç JFiZO zosta┼é przedstawiony konstruktywny dow├│d na r├│wnowa┼╝no┼Ť─ç si┼éy wyra┼╝e┼ä regularnych oraz deterministycznych automat├│w sko┼äczonych (DFA). Pokazanie, ┼╝e dla ka┼╝dego regexa istnieje r├│wnowa┼╝ny DFA jest proste, sprawa komplikuje si─Ö w drug─ů stron─Ö. Tak mi si─Ö przynajmniej na pocz─ůtku wydawa┼éo, ale im d┼éu┼╝ej o tym my┼Ťla┼éem, tym bardziej odczuwa┼éem wra┼╝enie, ┼╝e gdzie┼Ť ju┼╝ ten dow├│d widzia┼éem.

Tutaj mo┼╝na sobie zobaczy─ç moje notatki z JFiZO i nie tylko.

Continue reading “Wyra┼╝enia regularne a algorytm Floyda-Warshalla”