Now to prove P by contradiction, is to assume, the contrary, ¬P and construct an impossibility. But what you have really done here is prove ¬¬P. Now if you are a normal mathematician, you are classical, and hence you believe every statement A is either true or false, i.e. A∨¬A (A or not A, from any statement A, i.e. the law of the excluded middle). It just so happens that if you accept the law of the excluded middle then from ¬¬P you can deduce P.

An interesting question is why is the meaning of a proof of negation the construction of an absurdity? I guess this is philosophical, but if you accept the point of logic is to only conclude true things, then concluding an absurdity must be impossible, and hence if you assume something that leads to an absurdity, it follows that there must be no proof of the assumption because otherwise you'd have a proof of absurdity, and hence the meaning of a negation is showing that there is no proof of the pre-negated statement. In logic, ⊥ is used as the symbol for absurdity. Hence ¬P is really shorthand for P⇒⊥ (P implies absurdity), which is why earlier I identified A∧¬A with absurdity since when you have A and A implies absurdity, you immediately deduce absurdity.

- [1] "https://existentialtype.wordpress.com/2017/03/04/a-proof-by-...

A demonstration by "Reductio ad absurdum" can also be done in multivalent logic, for instance in trivalent logic, where a statement can be true or false or neither true nor false, therefore "Tertium non datur" is not applicable. In my opinion, trivalent logic is the simplest kind of logic that is applicable to mathematics or to the real world. Its subset that is bivalent logic is interesting as an object of study but not as a technique that can be useful for practical reasoning or for mathematical demonstrations.

If I understood you correctly, you want to distinguish the following 2 kinds of demonstrations, where P1 and P2 are propositions:

1. One demonstrates that "P1 implies not P1". From this it can be concluded that P1 cannot be true.

2. One demonstrates that "P1 implies not P2". But it is known that P2 is true. From these 2 facts it can be concluded that P1 cannot be true.

Which of these 2 you call "proof by contradiction"?

Probably a better name is needed, because both kinds of demonstrations end in a contradiction, the first contradicts the premise, while the second contradicts an independently known fact.

EDIT:

Another poster has provided a link to someone who uses the following definition:

"A proof by contradiction is a proof of a positive by refutation of the negative."

I believe that such a definition refers to a thing so trivial that it does not deserve a special name.

Obviously if P is a proposition and it is shown that "not P cannot be true" (refutation of the negative), only in bivalent logic it can be concluded that P must be true. In trivalent logic, that only proves that P is either true or neither true nor false.

It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction. Technically, what you've actually done is proven ¬(¬P). Now if you're a classical logician, you would say that ¬(¬P) is equivalent to P; if you're a constructivist, you wouldn't.

So proof by contradiction isn't in the constructivist's toolbox, with the proviso that many people think they're doing a proof by contradiction when they're not actually.