This my post is about mathematical logic, but first I will explain the story about people who asked or answer this question.
A famous mathematician Timoty Gowers asked this question: What is the difference between direct proofs and proofs by contradiction.
We, people, are capable of doing irrational things and to be discouraged.
I wrote an unthoughtful comment at Timoty Gowers’s blog. And this has caused Gowers to be discouraged and don’t continue to search an answer for his question. Yes, all of us, even Fields medalists such as Gowers are capable for doing irrational things.
On the other hand the irrational thing which I have done, was that I simply posted that somehow stupid comment despite of knowing that there are more about this (as described below). Note however that at the time of posting that comment I have not yet formulated the below exactly.
The trouble with my comment is that it applies only to the standard axiomatic theory of first order predicate logic. My comment is wrong for the way mathematics is usually written and is communicated. And this way differs of the customary formal predicate logic.
In customary informal mathematics the words “for all” and “exists” are not exact equivalent of $latex {\forall}&fg=000000$ and $latex {\exists}&fg=000000$ from first order predicate logic. The main difference is that we can have more than one proposition under a quantifier.
Examples:
For all $latex {x \in \mathbb{R}}&fg=000000$ we have $latex {e^x > 0}&fg=000000$ and therefore $latex {e^x > – 1.}&fg=000000$
In the standard first order predicate logic this would be written as two separate formulas:
$latex {\forall x \in \mathbb{R} : e^x > 0}&fg=000000$; $latex {\forall x \in \mathbb{R} : e^x > – 1}&fg=000000$.
Have you noticed that in the informal mathematics we usually require $latex {x \in \mathbb{R}}&fg=000000$ only once and don’t write it twice as in the above formal formula?
Certainly we can invent a formalistic for this, like:
$latex {\forall x \in \mathbb{R} : ( e^x > 0 ; e^x > – 1)}&fg=000000$.
Here we have multiple propositions under an universal quantifier.
It can be considered formally:
$latex {\forall x \in U : ( P_0 ( x) ; \ldots ; P_n ( x))}&fg=000000$ is a shorthand for $latex {\forall x \in U : P_0 ( x) ; \ldots ; \forall x \in U : P_n ( x)}&fg=000000$.
Now an example about existence quantifiers:
There exists $latex {n \in \mathbb{N}}&fg=000000$ such that $latex {n > 2}&fg=000000$ and therefore $latex {n^2 > 4}&fg=000000$.
To formalize this, consider $latex {\exists n \in \mathbb{N} : n > 2}&fg=000000$ as a definition. After this formula we have $latex {n}&fg=000000$ defined and it must confirm to the proposition $latex {n > 2}&fg=000000$.
This could be written formally as:
$latex {( \exists n \in \mathbb{N} : n > 2) ; n^2 > 4}&fg=000000$.
In customary logic this could be expanded to
$latex {( \exists n \in \mathbb{N} : n > 2) ; ( \exists n \in \mathbb{N} : n^2 > 4)}&fg=000000$.
To formalize this after the $latex {\exists}&fg=000000$ definition we could introduce a new constant symbol ($latex {n}&fg=000000$ in our example) and a new theorem ($latex {n > 2}&fg=000000$ in our example). I leave as an exercise to describe the mapping from my formalistic (where $latex {\exists}&fg=000000$ denotes not just existence but also a definition) to the reader.
Now to the claimed topic of this post, the difference of proof by contradiction and a direct proof:
Suppose now we want to prove a proposition $latex {\forall x \in U : R ( x)}&fg=000000$.
Proof by contradiction:
Suppose $latex {\neg \forall x \in U : R ( x)}&fg=000000$. Then $latex {\exists x \in U : \neg R ( x)}&fg=000000$.
After this we can have a sequence $latex {( \exists x \in U : \neg R ( x)) ; P_0 ; \ldots ; P_n ; 0}&fg=000000$ of propositions using this $latex {x}&fg=000000$.
Or we can prove it directly: Then we would have a sequence
$latex {P_0 ; \ldots ; P_n ; \forall x \in U: ( Q_0 ( x) ; \ldots ; Q_n ( x) ; R ( x))}&fg=000000$.
The choice of direct proof or proof by contradiction should depend on which of these two sequences of formulas is simpler.
Now suppose we want to prove a proposition $latex {\exists x \in U : R ( x)}&fg=000000$.
Proof by contradiction:
Suppose $latex {\neg \exists x \in U : R ( x)}&fg=000000$. Then $latex {\forall x \in U : \neg R ( x)}&fg=000000$.
Then we would have a sequence of propositions
$latex {\forall x \in U : ( \neg R ( x) ; P_0 ; \ldots ; P_n ; 0)}&fg=000000$.
Or we can prove it directly: Then we would have a sequence
$latex {(\exists x \in U: P_0 ( x)) ; P_1(x) \ldots ; P_n ( x) ; R ( x)}&fg=000000$.
The choice of direct proof or proof by contradiction should depend on which of these two sequences of formulas is simpler.
I leave open the following topic of discussion:
Show examples that sometimes a direct proof and sometimes a proof by contradiction is shorter.
Remark: All I have written here is about classic logic. I don’t deal with intuitionistic logic.