To be a little more concrete, what it means to prove a negation ¬P (not P) is to assume P and construct an impossibility from it, like 0=1 (assuming those symbo

To be a little more concrete, what it means to prove a negation ¬P (not P) is to assume P and construct an impossibility from it, like 0=1 (assuming those symbols exist in the theory you are working with) or more generally A∧¬A (A and not A) for some A (0=1 being a absurdity, hopefully, because your ambient theory already proves 0≠1). 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.