How does proof by contradiction work in an axiomatic system? In terms of mathematical logic, how does proof by contradiction (or reductio ad absurdum) work in an axiomatic system? Is it a part of axioms for propositional logic? or can it be deduced from other axioms?
 A: In the axioms for first order logic I've seen, proof by contradiction is an axiom.
The three axioms I've read are:
$A\Rightarrow (B\rightarrow A)$
$(A\Rightarrow (B\Rightarrow C))\Rightarrow ((A\rightarrow B)\Rightarrow (A\Rightarrow C))$
$(-A\Rightarrow -B)\Rightarrow((-A\Rightarrow B)\Rightarrow A)$
The last one is proof by contradiction. As axioms on first order sentential logic there are all independent. You could definitely axiomize logic in a different way with different axioms such that proof by contradiction is deductable.
My source of these axioms seems to indicate that proof by contradiction is so basic, fundamental, and clear that it should be an axiom.
Hope this helps :)
Edit: If you read out the final axiom in words you can see it is proof by contradiction. Also these axioms only use implication which is defined via these axioms. Conjugation and disjunction (and and or) can be defined from these axioms.
A: $\def\\{-\!\!\!}$In propositional logic, proof by contradiction means the following argument form, where ${\bf F}$ denotes any statement which is always false:
$$\eqalignno{
  &(\neg p)\to{\bf F}\cr
  \\\\\\\\&\\\\\\\\\\\\\\\\\\\\\cr
  \therefore\quad&p\cr}$$
To say that this argument form is valid means that in any case where the hypotheses (in this example only one hypothesis) is true, the conclusion is also true.  Another way of saying this is that the propositional formula $\langle\hbox{hypotheses}\rangle\to\langle\hbox{conclusion}\rangle$ is a tautology.  To confirm validity in this example we look at
$$((\neg p)\to{\bf F})\to p$$
and construct a truth table.
$$\matrix{p&\neg p&(\neg p)\to{\bf F}&((\neg p)\to{\bf F})\to p\cr
  T&F&T&T\cr F&T&F&T\cr}$$
The final result is always true, so the statement is a tautology and the argument form is valid.
A: In natural deduction systems for classical logic you can find a rule that looks like this:


*

*From $\neg \neg P$, may infer $P$.


If we define $\neg P$ to be $P \to \bot$, the formula $\neg \neg P$ states that the absurdity of P is absurd.
When proving something by contradiction, we start with the assumption $\neg P$, and attempt to show that it leads to absurdity, and conclude $P$ from that. Once we have a deduction from $\neg P$ to absurdity, we can apply the implication introduction and get $\neg P \to \bot = \neg \neg P$. Then, we can apply rule (1) and get $P$.
