Proving the axioms of $HFOL$ are semantic tautologies for $FOL$ We wish to construct an axiomatic system similar to $HPC$ i.e. Hilbert System for Propositional Calculus, for first order languages, denoted as $HFOL$. 
We wish to prove the following axioms of $HFOL$ are tautologies in order to show $HFOL$ is sound for $FOL$, that is everything we can prove using $HFOL$ is semantically correct in $FOL$ to my understanding. 
The axioms are:$\\\: \\1. \space \phi_1= \forall x(A\rightarrow B)\rightarrow(A\rightarrow\forall xB) \\ 2. \space \phi_2 = \forall x(B\rightarrow A)\rightarrow (\exists xB\rightarrow A)$
We also demand that $x$ is not a free variable in A i.e. $x\notin FV(A).$ Not sure why this demand.
We can also use the generalization rule.
So basically we want to show $\phi_1 ,\phi_2$ are tautologies in $FOL$, more precisely that (to my understanding) we want to show $M,v \models \{ \phi_1, \phi_2\}$ for every possible $M =  (D,I)$ structure in $FOL$ and $v: V\rightarrow D$ from the set of variables in $A,B$ to the domain of the structure. How do you show this? Am I right with the quantifiers? Because I was thinking it might be that for every structure there exists a valuation $v$ that satisfies the axioms. 
I would appreciate many type of proofs, such as proof trees and natural deduction type proofs. Thanks!
 A: You have to show that the provided axioms are valid, i.e. true for every model $M$ and valuation $v$.
Consider the first one and assume that it is not valid, i.e. that :

$M,v \nvDash ∀x(A → B) → (A → ∀xB)$, for some $M$ and $v$.

This means that : $M,v \vDash ∀x(A → B)$ and  $M,v \nvDash (A → ∀xB)$.
Consider the second formula; it means that : $M,v \vDash A$ and $M,v \nvDash ∀xB$.
Now we apply the clause of the semantical specifications related to the universal quantifier, and we have that : 

for some $a \in D$ (where $D$ is the domain of the model) : $M, v(x|a) \nvDash B$ [in plain language : if $∀xB$ does not hold in $M$, tehre is some object $a \in D$ such that $B$ does not hold of it].

Consider now $A \to B$.
We have $M,v \vDash A$ and $x \notin \text {FV}(A)$ [here the proviso is crucial]. Thus, also $M,v(x|a) \vDash A$.
But $M,v(x|a) \nvDash B$.
Thus :

$M, v(x|a) \nvDash (A \to B)$,

contradicting the assumption that : $M,v \vDash \forall x (A \to B)$.

Same approach for the second axiom.
