Negation rules in natural deduction There are various treatments of using negation in natural deduction for classical logic.
Let me quote bits of it:
$$\frac{}{\top}\top I$$
$$\frac{\bot}{A}\bot E\quad ex\ falso\ quodlibet$$
$$\frac{A\rightarrow\bot}{\neg A}\neg I$$
$$\frac{}{A\vee \neg A}tertium\ non\ datur$$
$$\frac{A\quad \neg A}{\bot}law\ of\ contradiction$$
$$\frac{A}{\neg\neg A}double\ negation\ 1$$
$$\frac{\neg\neg A}{A}double\ negation\ 2$$
$$\frac{\begin{equation}\begin{array}{c}{[\neg A]\\ \vdots\\ \bot}\end{array}\end{equation}}{A}indirect\ proof$$
What is a standard way of building this, what are the axioms and how are the other rules are proved?
You might answer this by referring to some reference.
 A: The only true "negation rule" needed is reductio ad absurdum aka proof by contradiction:
$$\dfrac{\begin{equation}\begin{array}{c}{[\neg A]\\ \vdots\\ \bot}\end{array}\end{equation}}{A}\bot$$
It is important to note that RAA is not an instance of negation introduction (see  below) but actually a separate rule.
$\neg A$ can be defined as syntactic sugar for what is actually $A \to \bot$, and $\top$ as $\neg \bot$ and hence $\bot \to \bot$. There is no deduction rule needed for switching between the two, they are treated as literally same formula that just looks different:
$$\neg A  \quad = \quad A \to \bot$$
$$\top \quad =  \quad\neg \bot \quad = \quad \bot \to \bot$$
Negation introduction and elimination is then a special case of implication introduction and elimination (negation elimination is what you call law of contradiction, and implication elimination is also known as modus ponens):
$$\frac{\begin{equation}\begin{array}{c}{[A]\\ \vdots\\ \bot}\end{array}\end{equation}}{\neg A}\neg I
\quad = \quad 
\frac{\begin{equation}\begin{array}{c}{[A]\\ \vdots\\ \bot}\end{array}\end{equation}}{A \to \bot}\to I 
$$
$$$$
$$\frac{A\quad \neg A}{\bot}\neg E
\quad = \quad
\frac{A\quad A \to \bot}{\bot}\to E
$$
EFQL is just RAA with no assumption discharged (see the comments for a discussion on the difference between the two):
$$\frac{\bot}{A}\text{EFQL}
\quad \rightsquigarrow \quad
\frac{\bot}{A}\bot
$$
The other rules can then be derived from these primitive rules:
For double negation,
$$\dfrac{A}{\neg\neg A}\neg \neg I
\quad \rightsquigarrow \quad
\dfrac{\dfrac{[\neg A]^1 \quad A}{\bot}\neg E}{\neg \neg A}\neg I^1
\quad = \quad
\dfrac{\dfrac{[A \to \bot]^1 \quad A}{\bot}\to E}{(A \to \bot) \to \bot}\to I^1
$$
and
$$\dfrac{\neg \neg A}{A}\neg \neg E
\quad \rightsquigarrow \quad
\dfrac{\dfrac{\neg \neg A \quad [\neg A]^1}{\bot}\neg E}{A}\bot^1
\quad = \quad
\dfrac{\dfrac{(A \to \bot) \to \bot \quad [A \to \bot]^1}{\bot}\to E}{A}\bot^1
$$
For the axioms,
$$\dfrac{}{\top}\top I 
\quad = \quad
\dfrac{}{\neg \bot}\top I
\quad \rightsquigarrow \quad
\dfrac{[\bot]^1}{\neg \bot}\neg I
\quad = \quad
\dfrac{[\bot]^1}{\bot \to \bot}\to I^1
$$
and finally, $$
\dfrac{}{A\vee \neg A}\text{TND}
\quad \rightsquigarrow \quad
$$
see here; their $(* B)$ is our $* E$  (eliminiation) and $(* E)$ is $* I$ (introduction).
So natural deduction doesn't need axiom as primitives: Everything can be derived from the basic set of inference rules $\{\land I, \land E, \lor I, \lor E, \to I, \to E, \bot\}$.
