The axiom systems of predicate logic

Question

I'm writing an article about logic for absolute dummies, so I want to make everything crystal clear; now I'm going to discuss predicate logic. After Googling, I found there are mainly 2 slightly different kinds of axiom systems for it, both are present here. let's simply call the first system in the link FOL1, and the alternative system FOL2.

Here's my question:

1. Why does $x$ have to be bound in $A$ in the 5th axiom $(A\to∀xA)$ in FOL1? Can this axiom be replaced by $A∣-∀xA$ ?

2. Why is there an extra quantification in axiom $4$ in FOL1 than in FOL2? This axiom in FOL1 seems easier to explain.

Answer 1

Question 1:

Variables must be bound because we don't work with open sentences in proof systems, yet it is possible to assign a truth value to open sentences.

The truth value of an open sentence $A$ with an free variable $x$ is true if and only if the value of its closure $\forall x A$ is true.

Question 2:

The difference between axiom 4 in FOL1 and FOL2 is that the rule in FOL1 $\forall x(A\rightarrow B) \rightarrow (\forall x A \rightarrow \forall x B)$ allows $x$ to be free in $A$. The rule in FOL2 $\forall x (A\rightarrow B)\rightarrow (A\rightarrow \forall x B)$ on the other hand explicity states that $x$ must not be free in $A$, therefore FOL1 rule is broader than FOL2's.