I'm studying first-order logic with Hilbert proof system (I'm completely new to this) and I need to proof one of the basic identities: $ \neg (\forall x) \neg \phi \implies (\exists x) \phi $
This is what I made:
$ A1: \neg[(\forall x) \neg \phi] \qquad Hypothesis \\ A2: \neg (\neg \phi[a/x]) \qquad U.I \\ A3: \neg (\neg \phi[a/x]) \implies \phi[a/x] \qquad Theorem \\ A4: \phi[a/x] \qquad M.P(A2, A3) \\ A5: \exists x \phi \qquad E.G \\ A6: \neg (\forall x) \neg \phi \implies (\exists x) \phi \qquad D.T \quad A1-A5$
The theorem at A3 is one I proved in Hilbert System.
Is this proof good? Or it makes absolutely no sense, I have a lot of doubts in A2 and A5.
Thanks.
A2 is, as you feared, incorrect. You are basically instantiating a universal that is part of a larger statement, and you cannot do that. To see why not, let's take $\neg \forall x \phi(x)$. So this means that not everything has property $\phi$, and that means that there is something that does not have property $\phi$, ... But we don't know wat that object is. So, if I try to infer $\neg \phi(a)$, I may be inferring something that is not the case, since it is possible that $a$ does have property $\phi$.