changing the axiom $\forall x(A(x) \to B) \to (\exists xA(x)\to B) $ of Hilbert proof system for perdicate logic

Question

What type of logic would it be if we change the axiom

$$ \text{old} = \forall x(A(x) \to B) \to (\exists xA(x)\to B) $$

to the new rule

$$ \text{new} = \forall x(A(x) \to B) \to (\forall xA(x)\to B) $$

in the Hilbert proof system. Would it produce a system weaker, stronger, or equivalent to first-order logic (predicate logic)?

Answer 1

It would be weaker: $\forall x \ A(x)$ is stronger than $\exists x \ A(x)$, and thus $\forall x \ A(x)\to B$ is weaker than $\exists x \ A(x)\to B$: you're Strengthening the Antecedent, which makes the conditional weaker.

So, you have a weaker axiom, and thus a weaker system. Indeed, the new system is no longer complete. It cannot prove, for example, the very statement $\forall x \ A(x)\to B$

Answer 2

With a naked eye, you could see the two statements are equivalent when the domain is not empty; however, if the domain is empty then the second statement would be false hence taken as an axiom it would lead to a trivial useless theory.

I remember that the foundations I saw assume that the domain is not empty hence everything should be ok.

Everything boils down to statement:

$$ \forall_x \Phi(x)\Rightarrow \exists_x \Phi(x) $$

It'd by false for the empty domain but, for each $\Phi,\,$ it can and did serve as a subsystem of axioms for some classical foundational systems.