# hilbert system first order logic proof

i need to prove the following and i have no idea how to without using soundness and completeness

$\neg \forall x A \rightarrow \exists x \neg A$

using the following axioms:

I1. $A \rightarrow (B \rightarrow A)$

I2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$

N1. $(A \rightarrow B) \rightarrow ((A \rightarrow \neg B) \rightarrow \neg A)$

N2. $\neg \neg A \rightarrow A$

C1. $A \wedge B \rightarrow A$

C2. $A \wedge B \rightarrow B$

C3. $A \rightarrow (B \rightarrow A \wedge B)$

D1. $A \rightarrow A \vee B$

D2. $B \rightarrow A \vee B$

D3. $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \vee B \rightarrow C))$

the next two axioms are for the case when $x \notin FV(A)$

3.i. $\forall x (B \rightarrow A) \rightarrow (\exists x B \rightarrow A)$

3.ii. $\forall x (A \rightarrow B) \rightarrow (A \rightarrow \forall x B)$

the next two are axioms for the case when substituting t instead of x in A wont cause any free variable in t to become bounded by quantifier

$\forall x A \rightarrow A\{t/x\}$

$A\{t/x\} \rightarrow \exists x A$ (A{t/x} means substitute t in place of x in A)

and the following inference rules:

$A,A \rightarrow B$ infer $B$ (MP)

$A$ infer $\forall x A$ (Gen)

-

A good idea is to work with the contrapositive. That is show that $\lnot\exists x\lnot A\to\forall x A$. Then show that $A\to\lnot\lnot A$ and $(\lnot A\to\lnot B)\to (B\to A)$. My guess is that some of these steps you are aware of how to do, or you have seen them.
To show that $\lnot\exists x\lnot A\to\forall xA$, use the deduction theorem. Assume that $\lnot\exists x\lnot A$, use axiom $\lnot A\{t/x\}\to\exists x\lnot A$, as well as the fact that $\lnot A\{t/x\}\to\lnot\exists x\lnot A$ (this follows from the assumption that $\lnot\exists x\lnot A$ is true and the first axiom). Now use axiom N1 to deduce $\lnot\lnot A\{t/x\}$. Then use axiom N2 and the generalisation rule to deduce $\forall x A$.