How about a little absurdity?

Assume you want to prove a Theorem X. If you’re a fan of reductio ad absurdum (RAA), you start by saying “Assume that Theorem X is false. Hence…” and after some reasoning, you reach a contradiction.  You write as a closing sentence, “This contradiction shows that Theorem X must be true.”

I want to argue about the following questions: Do we need only one use of the rule of contradiction? Can we start a proof as above and not use an argument by contradiction but at the end?

The answers depend on the logic in which the arguments take place. In the short paper I show  that this is true in propositional logic. That is,

any valid propositional formula can be proved by using RAA just once. (*)

A classical result by Glivenko can be obtained as a corollary: For any propositional formula $\phi$, you can prove $\phi$ in classical logic if and only if you can prove $\neg\neg\phi$ without using RAA.

It can also be shown that Glivenko’s theorem doesn’t go through predicate logic (using $\forall$ and $\exists$). Since the statement (*) above implies Glivenko, we conclude that in predicate logic there are theorems only having proofs that

1. can’t begin as in our first paragraph, and conclude with only one contradiction to obtain the result; or
2. have at least two uses of RAA.

One example of this is the theorem-scheme of double negation shift: for every $\phi(x)$ the following is a theorem:
$$
\forall x(\neg\neg\phi(x)) \limp \neg\neg\forall x(\phi(x)).
$$

If you manage to prove this without any form of RAA, your proof is wrong. And if you managed to prove this correctly in the format of the first paragraph, you are indeed using RAA once more in the middle. Beware: Any of $\neg\neg\phi \limp\phi$, $\phi\o\neg\phi$, or $(\neg\phi \limp\neg\psi)\limp(\psi \limp\phi)$,  among others, need at least one use of RAA!

EDIT: 
I was informed that this proof has already appeared in the book “Elements of logical reasoning” (CUP 2013) by Jan von Plato and uses a normalization result published in “Normal derivability in classical natural deduction,” Jan von Plato and Annika Siders, Review of Symbolic Logic, 2012. See my next post.