Determine if the following formulas are logic axioms (First Order Logic)

Considering that the logic axioms of first order logic are given by:

$(A1)$ - All Tautologies.

$(A2)$ - $(\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta))$.

$(A3)$ - $(\forall x \alpha) \rightarrow [\alpha]^{t}_{x}$ if x is free for t in $\alpha$.

$(A4)$ - $\alpha \rightarrow (\forall x \alpha)$ if x is not free in $\alpha$.

$(A5)$ - $x = x$

$(A6)$ - $(x=y) \rightarrow (\alpha \rightarrow \beta)$ if $\beta$ if obtained by substitution of at least one occurrence of x free for y in $\alpha$.

Are the following formulas logic axioms, following this definition? For the formulas that are logic axioms, in which group of axioms is the formula based?

I - $x = y \rightarrow (y=z \rightarrow z=x)$

II - $\forall w \exists x (P(w,x)\rightarrow P(w,w)) \rightarrow \exists x (P(x,x)\rightarrow P(x,x)))$

III - $\forall x(\forall x(c = f(x,c) \rightarrow \forall x\forall x(c= f(x,c))))$

IV - $\forall x((0<x) \rightarrow (0<x+x)) \rightarrow ((0<x) \rightarrow \forall x(0<x+x))$

For example, I is something like (A6), but I can't see if $\beta$ in this case is obtained of $\alpha$ by substitution of at least one occurrence of x free for y.

Considering II, I know it is something like (A3), but when we substitute w for x, because of the $\exists x$, is it a logic axiom?

Considering III, we have something like $\forall x(\forall x \alpha \rightarrow \forall x(\forall x\alpha))$, where $\alpha$ is $c=f(x,c)$. How do I proceed with the analysis? Same case for the generalization of $(0<x+x)$ in IV.

• Edited the question, thanks. – Bruno A Aug 20 '16 at 18:47
• For II, the subst is not allowed, because the new $x$ in $P(x,x)$ has been "captured" by $\exists x$. In formal words, "$w$ is not free for $x$ in $∃x(P(w,x)→P(w,w))$". – Mauro ALLEGRANZA Aug 22 '16 at 8:47
• For I, it is not exactly (A6); a correct instance of it must be like : $x=y \to (x=z \to y=z)$ or $x=y \to (z=x \to z=y)$. – Mauro ALLEGRANZA Aug 22 '16 at 8:51
• So, for I, it is not (A6), so it is not an axiom too, correct? For III, should I use (A4) some way? – Bruno A Aug 22 '16 at 12:56
• For I : Yes, it is not an axiom. Of course, it can be proved from axioms, using the following instance of (A6) : $y=x \to (y=z \to x=z)$ and deriving $x=y \to y=x$ from the following (A6): $x=y \to (x=x \to y=x)$. – Mauro ALLEGRANZA Aug 22 '16 at 13:09