Theorems & proof by contradiction The following formula seems to be regarded as the essence of proof by contradiction:

p → (q ∧ ~q) ⊢ ~p

Or perhaps this one:

~p → (q ∧ ~q) ⊢ p

If this is the case, what are the mathematical theorems that have this logical form?
I looked at various proofs that are routinely presented as proofs by contradiction, for example the proof that the square root of 2 is irrational, but it turns out they are all more complex than ~p → (q ∧ ~q) ⊢ p and different in principle.
Alternatively, what is the justification for saying ~p → (q ∧ ~q) ⊢ p is the typical form of a proof by contradiction?
Alternatively, if ~p → (q ∧ ~q) ⊢ p is not the typical form of a proof by contradiction, which form is?
 A: $q \wedge \neg q \to A$ is a valid rule of inference in most logics, constructive or otherwise. That doesn't require "proof by contradiction"; merely "ex falso quodlibet". If you've proved false, you can prove anything. This is intuitively justifiable by the idea that "there's no way to produce $\bot$ from the axioms, so if you have a proof which somehow managed to produce $\bot$, you can carry through exactly the same proof replacing $\bot$ with $A$ throughout".

"Proof by contradiction" is different, and basically means "$\neg (\neg p)$ implies $p$". To prove $P$ by contradiction, you suppose $P$ is false, and then you prove falsity from that assumption; and then having shown that $\neg P$ is false, you invoke "$\neg (\neg P) \to P$" ("double-negation elimination") to tell you that $P$ must have been true after all.
An example of a proof by contradiction is as follows:

Theorem. There is a pair of irrational numbers whose product is irrational.
Proof. Suppose not. Then all pairs of irrational numbers have rational product.  But there are only countably many rationals, and there are uncountably many irrationals; and for any $a \not = 0$, the map $b \mapsto a \times b$ is injective; so we have exhibited an injection from an uncountable set to a countable set. This is a contradiction: we can derive falsity from this. So we have shown that "no pair of irrational numbers has rational product" is false, and so by double-negation elimination there must be a pair of irrational numbers with irrational product.

In this case, $P$ is the proposition "there is a pair of irrational numbers whose product is irrational", and we derived falsity from the theorem "if you have an injection from uncountable to countable, then you can prove False".
A: A proof by Contradiction is a proof technique: You assume $p$. You then show that that leads to a contradiction, i.e. that the assumption implies $q$ as well as $\neg q$ for some statement $q$. From this, you discharge the assumption and conclude $\neg p$. So yes, in that sense, $p \to (q \land \neg q) \vdash \neg p$ seems to capture that pretty well
The fact that actual proofs by Contradictions look much more complicated than this is because it can take many steps to derive $q$ and $\neg q$ from the assumption $p$. Indeed, as such, maybe a better representation would be something like $(p \vdash (q \land \neg q)) \vdash \neg p$ ... but now we run into notational and interpretational issues of what exactly we mean by $\vdash$.  
So, it is better to just stick to $p \to (q \land \neg q) \vdash \neg p$ ... but please note that in every proof by contradiction, there really is such a statement $q$ that you can point to.  In the typical proof that $\sqrt{2}$ is irrational, for example, the assumption that $\sqrt{2}$ is rational leads to the statement that $\sqrt{2} = \frac{m}{n}$ where not both $m$ and $n$ are even, as well as to the statement that $\sqrt{2} = \frac{m}{n}$ for those same $m$ and $n$ but now they are both even. And so there are the statements $q$ and $\neg q$
A: The inference pattern:

"if something leads to a contradiction the contrary follows", 

is known in the literature with different names: as Indirect proof, as  Reductio ad absurdum and as Proof by Contradiction.
Usually we do not make the distinction into a genuine indirect proof:

if $\lnot A$ leads to a contradiction, then $A$ can be inferred,

and a proof of a negative proposition: 

If $A$ leads to a contradiction, then $\lnot A$ can be inferred. 

This distinction is crucial to understand the role of negation in Intuitionsitic Logic.
A typical example is the proof of irrationality of a real number $r$: assume that $r$ is rational, derive a contradiction, and conclude that $r$ is irrational .
The confusion derives from not realizing that to be an irrational number is a negative property: 

there do not exist integers $n, m$ such that $r = \dfrac n m$.

Thus, the proof assumes the irrationality of $r$ : $\exists n,m \ (r = \dfrac n m)$, and derive a contradiction.
Then conclude, using Negation introduction, that:

$\lnot \exists n,m \ (r = \dfrac n m).$

