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)