Without a falsum constant, your rule of ex falso quodlibet should look something like $\phi, \neg \phi \vdash \psi$. So from the contradictory assumptions, $\neg\neg a$ and $\neg a$, you may immediately derive $a$.
$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{\neg\neg a}{\vdots\\\fitch{\neg a}{a \qquad \text{ex falso quodlibet }\neg a, \neg\neg a \vdash a }\\\vdots}$$
PS: If ex falso quodlibet looks like $\phi\wedge\neg\phi\vdash\psi$, simply introduce a conjunction then use it.
PPS
If ex falso quodlibet is not accepted as fundamental, but disjunctive syllogism is, then introduce a disjunction and use that. $$\fitch{\neg\neg a}{\vdots\\\fitch{\neg a}{\neg a\vee a\qquad:\text{disjunctive introduction }\neg a\vdash \neg a\vee a\\a \qquad\qquad:\text{disjunctive syllogism }\neg a\vee a, \neg\neg a \vdash a }\\\vdots}$$
P$^3$S
Disjunctive Syllogism and Ex Falso Quodlibet are interprovable - each may be justified only by accepting the other - so which is considered fundamental by a proof system is a matter of preference. (EFQ has a smaller format.)
$$\tiny\fitch{((p\lor q)\land\lnot p)\to q:\text{Premise of Disj.Sylogism}}{\fitch{p\land\lnot p}{\lnot p:\text{Conj. Elim.}\\p:\text{Conj.Elim.}\\p\lor q:\text{Disj.Intro}\\(p\lor q)\land\lnot p:\text{Conj.Into.}\\q:\text{Cond.Elim.}}\\(p\land\lnot p)\to q:\text{Cond.Into}}\fitch{(p\land\lnot p)\to q:\text{Premise of Ex Falso Quodlibet}}{\fitch{(p\vee q)\land\lnot p}{\lnot p:\text{Conj.Elim.}\\p\lor q:\text{Conj.Elim.}\\\fitch{p}{p\land\lnot p:\text{Conj.Intro.}\\q:\text{Cond.Elim.}}\\p\to q:\text{Cond.Into.}\\\fitch{q}{}\\q\to q:\text{Cond.Intro.}\\q:\text{Disj.Elim.}}\\((p\vee q)\land\lnot p)\to q:\text{Cond.Into.}}$$
P$^4$S Oh! As Mauro comments, if $\phi\to\psi,\phi\to\neg \psi\vdash \neg \phi$ is considered as the negation introduction rule, then $\phi,\neg\phi\vdash\psi$ (EFQ) could be considered the corresponding negation elimination rule. Thereby cutting out the need for a falsum symbol.
If you discharge an assumption labelled $z$ you should remember to actually label the assumption.
Also, ex falso quodlibet is not a rule of discharging; the rule to discharge $y$ is negation introduction, which needs to be followed by double negation elimination (though some do combine it into Reduction Ad Absurdum (RAA)).
$$
\dfrac{
\dfrac{
\dfrac{
\dfrac{
\lower{1.5ex}{[\neg (P \to Q)]^z} \quad
\dfrac{
\dfrac{
\dfrac{[\lnot P]^y\quad[P]^x}{\bot}{\lnot E}
}{Q}{\rm efq}
}{P\to Q}{\to I^x}
}{\bot}{\rm efq}
}{\lnot\lnot P}{\lnot I^y}
}{P}{\lnot\lnot E}
}{\neg (P \to Q) \to P}{\to I^z}
$$
This was an example in Jean Gallier's Discrete Mathematics book. I feel like I got the mechanical parts understood. Still, my head hurts when thinking about how I assumed both $P$ and $¬P$ to prove something. How do you guys understand this? How can we assume both $P$ and $¬P$, isn't that absurd?
Yes, that is how Reduction to Absurdity proofs operate: "If this assumption was true it, then what follows would be absurd, so therefore it cannot be true."
In this proof: When given $\lnot (P\to Q)$ should we also assume $\lnot P$, then we could prove $P\to Q$ (through the ex falso quodlibet subproof), which is absurd, so therefore $\lnot (P\to Q)$ entails $P$, and so we deduce $\lnot(P\to Q)\to P$.
Here's the fitch style representation which may be easier to follow.
$$\def\fitch#1#2{\quad\begin{array}{|l}#1 \\\hline #2\end{array}}\fitch{}{\fitch{~1.~\lnot(P\to Q)}{\fitch{2.~\lnot P}{\fitch{~3.~P}{~4.~\bot\hspace{14ex}\lnot e, 2,3\\~5.~Q\hspace{14ex}\text{efq},4}\\~6.~P\to Q\hspace{12ex}{\to}i,3-5\\~7.~\bot\hspace{17ex}\lnot e,1,6}\\~8.~\lnot\lnot P\hspace{18ex}\lnot i,2-7\\~9.~P\hspace{21ex}\lnot\lnot e,8}\\10.~\lnot(P\to Q)\to P\hspace{10ex}{\to}i,1-9}$$
In this notation we keep track of the order in which assumptions are raised and discharged by indentation. Here we see that a contradiction can be derived on raising the third assumption, and so we may validly derive $Q$ within that context (because whatever $Q$ may be, it is at least as true as an absurdity).
Ex falso Quodlibet: If we can say "false is true", then we may say anything is true.
Best Answer
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\}$.