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.
For a structural, natural deduction presentation, the rules for $\top$ just contain $$\dfrac{}{\Sigma\vdash\top}\top\mathrm{I}$$ and that's it. There is no elimination rule. One way to see why this makes sense is that dually we want an elimination rule for $\bot$ but we certainly don't want an introduction rule. Another argument for this is that we can view $\top$ as a $0$-ary case of conjunction. For (binary) conjunction, we have an introduction rule with two premises and two elimination rules. Therefore, $\top$ should have an introduction rule with zero premises and zero elimination rules.
If we define (as is often done) $\neg\alpha$ as $\alpha\to\bot$, your FI rule (which I assume stands for something like "falsum introduction") is revealed to be a special case of $\to$ elimination. This rule is often called $\neg$ elimination, if $\neg$ is primitive (and especially if we can use an empty right-hand side of $\vdash$ to represent contradiction). I assume this is what NE is supposed to stand for, but that rule doesn't really have the appropriate form for an elimination rule. As I mentioned in an answer to an earlier question of yours, these rules are not ideally stated from a structural proof theory perspective since they combine multiple logical connectives.
We can derive the $\top$ introduction rule via the definition of $\top$ as $\neg\bot$ using your rules via: $$\dfrac{}{\dfrac{\Sigma\cdot\bot\vdash\bot}{\Sigma\vdash\top}\rlap{\mathrm{NI}}}\rlap{\mathrm{Axiom}}$$
Best Answer
The rules you list comprise a natural deduction system for intuitionistic logic. The sequent $\lnot A\to \bot\vdash A$ is not valid in intuitionistic logic, so it is not provable in your system.
To prove $\lnot A\to \bot\vdash A$, you need to be working with a natural deduction system for classical logic, which means adding an additional rule to your system. One common choice is to add double negation elimination itself; this makes your proof a valid one. Other common choices are adding reductio ad absurdum (proof by contradiction) or the law of excluded middle.