within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \rightarrow P(x))$.
The axioms are:
1) tautology axioms: every tautology is an axiom (where tautologies are the formulas for which exists a homomorphism from a tautology in propositional logic)
2) distributivity axioms: all formulas of the form $\forall x (\phi \rightarrow \psi) \rightarrow (\forall x \phi \rightarrow \forall x \psi)$
3) existence axioms: $\exists x \phi(x) \rightarrow \neg \forall x \neg \phi(x)$ and $\neg \forall x \neg \phi(x) \rightarrow \exists x \phi(x)$ for every formula $\phi$
4) generality axiom: all formulas of the form $\phi \rightarrow \forall x \phi$, whereby $\phi$ is a formula in which x isn't present
5) equality axioms: all formulas that have one of the forms $u=v, u=v \rightarrow u = u, (u=v \wedge v = w) \rightarrow u=w$, wherby u,v,w are any variables
6) Leibniz-axioms: all formulas of the form $(u_1 = v_1 \wedge \cdots \wedge u_n = v_n) \rightarrow f(u_1, \cdots, u_n) = f(v_1, \cdots, v_n)$ where f is a function symbol and axioms of the form $(u_1 = v_1 \wedge \cdots \wedge u_n = v_n) \rightarrow (R(u_1, \cdots u_n) \leftrightarrow (R(v_1, \cdots, v_n)) $ where R is a relation symbol.
7) substitution axioms: for a variable x, formula $\phi$, term t that is allowed to be substituted for x in $\phi$: $(\forall x \phi) \rightarrow \phi(x/t)$
With these axioms and Modus ponens I've been trying to derive the formulas mentioned above.
Here are my solutions so far:
(1) I've derived a formula of the form $\forall z \exists y R(z,y) \rightarrow \forall z \neg \forall y \neg R(z,y)$ and now I'm trying to bring the x in the second part instead of the y. So is $\forall z \neg \forall y \neg R(z,y) \rightarrow \forall z \neg \forall x \neg R(z,x)$ correct due to the substitution axiom or is it wrong to apply the substitution axiom because of the $\forall z \neg$ before the $\forall y$? (And if the latter is the case, how can the $\forall x$ be brought in?
(2) I've tried to derive the formula a couple of times, but I alway run into problems with the $\exists$. How can it be placed at the beginning of the whole formula?