Make an analysis of each of the following derivations in $ \mathbb S_1^= $, that is, mark the axioms, the rules of inference, $ \mathbb S_1^= $ - theorem and, if applicable, the hypotheses auxiliaries used. However, the derivation may not be $ \mathbb S_1^= $ - deduction, that is, it may prove to be a deductive fallacy in $ \mathbb S_1^= $.
Let $ \lnot \exists x \alpha [x] $ and $ \forall x \lnot \alpha [x] \mathbb L_1^= $, such that
$ \lnot \exists x \alpha [x] \vdash_{S_1^=} \forall x \lnot \alpha [x] \mathbb L_1^= $.
I-) $ \lnot \exists x \alpha [x] $
II-) $ \lnot \lnot \alpha [c] $
III -) $ \alpha [c] $
IV -) $ \exists x \alpha [x] $
V -) $ \exists x \alpha [x] \land \lnot \exists x \alpha [x] $
VI -) $ \lnot \alpha [c] $
VII -) $ \forall x \lnot \alpha [x] $
V-) It is wrong, right?
Well, it is valid, however you do not need to assume a double negation, when a position will do.
It also helps to indent or otherwise mark your subproofs.
$\def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}} \\\begin{array}{|l}~~1.~\lnot\exists x~\alpha[x]\hspace{16ex}\textsf{premise}\\\hline\begin{array}{|l}~~2.~\alpha[c]\hspace{20ex}\textsf{assume (with a fresh arbitrary variable)}\\\hline~~3.~\exists x~\alpha[x]\hspace{16.5ex}\textsf{existential generalisation}\\~~4.~\exists x~\alpha[x]\land\lnot\exists x~\alpha[x]\hspace{5ex}\textsf{conjunction}\end{array}\\~~5.~\lnot\alpha[c]\hspace{19.5ex}\textsf{indirect proof}\\~~6.~\forall x~\lnot\alpha[x]\hspace{16ex}\textsf{universal generalisation (since c is arbitrary)}\end{array}$