Proof for logical implication : $\exists_x A(x) \rightarrow \forall_x B(x) \implies \forall_x [A(x) \rightarrow B(x)]$

Question

Proof for logical implication : $\exists_x A(x) \rightarrow \forall_x B(x) \implies \forall_x [A(x) \rightarrow B(x)]$

Can you please see whether the proof is fine or not?

We know that $ {\forall_x B(x) \implies \exists_x B(x)} \\ [\exists_x A(x) \rightarrow \forall_x B(x)] \implies [\exists_x A(x) \rightarrow \exists_x B(x)] \implies \exists_x \neg A(x) \lor \exists_x B(x) \implies \\\exists_x [A(x) \rightarrow B(x)]$

Please correct me if I am wrong. I have doubt in that bold alphabet step (can use or not, what happens when we have for all of $x$ in front of $A(x)$. I am doubtful if it is valid or not ... )

$\forall_x A(x) \rightarrow \forall_x B(x) \implies [\forall_x A(x) \rightarrow \exists_xA(x)\rightarrow \forall_x B(x)] $

Can I say $\forall_x A(x) \rightarrow \forall_x B(x) \implies [ \exists_xA(x)\rightarrow \forall_x B(x)] \implies \forall_x [A(x) \rightarrow B(x)]$

Answer 1

There is an easy, informal, way to prove that $\exists x A(x) \to \forall x B(x)$ implies $\forall x (A(x) \to B(x))$.

It is well-known that $\exists x A(x) \to C$ is equivalent to $\forall x (A(x) \to C)$, provided that the variable $x$ does not occur free in $C$. So, from $\exists x A(x) \to \forall x B(x)$ it follows that \begin{align}\tag{1} \forall x (A(x) \to \forall x B(x)) \end{align} since $x$ is not free in $\forall x B(x)$. Now, $(1)$ means that, given an $x$ such that $A(x)$ holds, then $B(y)$ holds for every $y$, in particular for $y = x$. Therefore, $\forall x (A(x) \to B(x))$ holds.

We proved that $\exists x A(x) \to \forall x B(x)$ implies $\forall x (A(x) \to B(x))$.

Answer 2

The question is:

Can I say $\forall_x A(x) \rightarrow \forall_x B(x) \implies [ \exists_xA(x)\rightarrow \forall_x B(x)] \implies \forall_x [A(x) \rightarrow B(x)]$

Running the first conditional in a tree proof generator resulted in a countermodel:

Since $A$ is only true for $0$, $\forall x Ax$ is false, but $\exists xAx$ is true. Since $B$ is not true for any members of the domain, $\forall xBx$ is false. This allows the antecedent to be true and the consequent to be false.

A tree proof succeeded for $[ \exists_xA(x)\rightarrow \forall_x B(x)] \implies \forall_x [A(x) \rightarrow B(x)]$ which is the goal.

Rather than showing that proof, here is a natural deduction proof in a Fitch-style proof checker. Since this proof checker uses "A" to code universal quantification, I replaced the symbol "A" with "P" and "B" with "Q":

The strategy of the proof was to use the law of the excluded middle (LEM) on $\exists xPx \lor \neg \exists xPx$.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/