Does a proof by contrapostion guarantee an alternative direct proof?

If $P \Rightarrow Q$ is true and can be proved by "directly proving" its contrapositive $\lnot Q \Rightarrow \lnot P$, does the former, necessarily, also have an alternative direct proof?

Background: The second paragraph in Direct Proof states that proof by contrapositive is a form of indirect proof (though, I fail to see the difference between a direct proof and a proof by contrapositive since the latter seems as natural as any other direct proof and not contrived like for ex: a proof by contradiction).

• By the definition of 'direct', a proof by contrapositive is indirect because it assumes the negation of the conclusion you seek to prove and shows that your assumption p must be false. This is logically equivalent to showing that p entails q. Commented Jun 16, 2015 at 20:21
• Thanks for clearing that up. Commented Jun 16, 2015 at 20:32

Classically, conditional (or direct), contrapositive and proofs by contradiction are equivalent, in the sense that a proof of one can be converted into a proof of another.

Take, for example, a formal proof of $$¬Q\rightarrow ¬P \vdash P \rightarrow Q$$

In the following I use Gentzen's method of natural deduction (1934):

1) $¬Q\rightarrow ¬P$, Premise

2) $P$, Assumption

3) $\neg Q$, Assumption

4) $\neg P$, 1,2, Modus Ponens

5) $\bot$, 2,3, Conjunction Introduction

6) $\neg\neg Q$, 3-5, Negation Introduciton

7) $Q$, 6, Double Negation Elimination

8) $P \rightarrow Q$, 2-7, Conditional Introduction

In some other logics, particularly Intuitionistic Logic - which grew out of L. E. J. Brower's insatisfaction with the non-constructive methods of classic mathematics - this proof is impossible.

If you look attentively, you will see that in step 7 we had to use the double negation elimination rule. In fact, this rule is equivalent with the Excluded Middle Principle $\alpha \vee \neg \alpha$ which says that every sentence $\alpha$ is either true or false.

But intuitionists do not deny the excluded middle principle either: they just say it cannot hold generally, particularly for infinite domains. For instance, consider the sentence "there are primes bigger than $10^{10}$". Well, it could be true: to prove its truth-hood it's "enough" to examine for every $n > 10^{10}$ if there is some $n$ that is prime, one by one. But if this sentence is false we surely cannot prove that!

The conclusion to be drawn is that it depends on what system you are talking about: proofs are equivalent or not in some underlying logic.