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?
$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:
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".