One such identity is
∀x(a→R(x)) ↔ (a→ ∀xR(x))
Where x doesn't occur free in a.
Naturally, I tried separating the two directions. So for example, in one direction we assume {∀x(a→R(x)), a} and wish to deduce ∀xR(x). We can replace x with some constant c and continue:
a→R(c)
a
R(c) (MP)
But then what? how to generalize?
Actually, treating this identity semantically and using the model definition would make it easier for me(I think I know the proof), but I'm interested in the formal deduction method.
Come to think of it, there are other such identities that rearrange the universal quantifier, which I don't know how to formally deduce.
I highlighted two examples in the following screenshot(it's from Wikipedia):
I'd appreciate any guidance, Thanks.
You have raised an arbitrary variable and an assumption.
$\qquad{\begin{array}{ll}~~1.~\forall x~(a\to Rx)&\text{Premise}\\~~2.~\quad a\to Rc&\text{Universal Instantiation to arbitrary variable }c\\~~3.~\qquad a&\text{Assumption}\\~~4.~\qquad Rc&\text{Modus Ponens}\end{array}}$
You cannot generalise at this point because there is still an active assumption inside the scope of the arbitrary variable. Thus, you require that assumption be raised before introducing that variable.
So ... do that.
$\qquad{\begin{array}{ll}~~1.~\forall x~(a\to Rx)&\text{Premise}\\~~2.~\quad a&\text{Assumption}\\~~3.~\qquad a\to Rc&\text{Universal Instantiation to arbitrary variable }c\\~~4.~\qquad Rc&\text{Modus Ponens}\end{array}}$
Now you can discharge everything in the required order.
Of course, to prove an equivalence, you must also prove the converse. This is much the same: raise any variables and assumptions in the reverse of the order which you aim to discharge them.