Considering the list of axioms:
$(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$.
I am trying to write a proof for some theorems. However, I am a little confused.
$ \vdash (\forall x_1(R_1^1(x_1) \lor R_2^1(x_1))) \rightarrow (R_2^1(x_1) \lor R_1^1(x_1)) $
For this one, could I use (A3), given that $\forall x_1$ on the left side of $\rightarrow$?
$ \vdash R_1^1(c_1) \rightarrow (R_1^1(c_2) \rightarrow (R_1^1(c_1) \land R_1^1(c_2))) $
For this one, could I use the tautology $\alpha \rightarrow (\beta \rightarrow(\alpha \land \beta))$, given that $R_1^1(c_1)$ is the same relational symbol, but applied to different constants?
$ \vdash \forall x_1(\forall x_2(R_1^1(x_1) \rightarrow (R_1^1(x_2) \rightarrow R_1^1(x_1))))$
Same question as before (combining the first ones), could I use the tautology $\alpha \rightarrow (\beta \rightarrow \alpha)$ and then (A4)?
First: Yes, though you have to combine (A3) with a tautology in order to get to swap the $R_2^1$ and $R_1^1$ disjuncts in the conclusion.
Second: Yes, this is an instance of (A1).
Third: No, (A3) will let you remove a $\forall$ from something you've already proved, not add it. In fact I'm almost sure your axioms are not enough to prove this, if all you have is Modus Ponens. Specifically, the axioms would all be true under a variant semantics where $\forall x\alpha$ always evaluates to false when $x$ is free in $\alpha$ (and MP preserves this truth). Since your goal is not true in this that variant semantics, it can't be proved.
Are you sure you don't have a separate Generalization rule in addition to your axioms and MP?