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

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)]$$

• A proof is not just a sequence of formulas that you write down. You have to say why each step follows from the previous. You also need to specify a proof system (i.e. axioms and rules of inference) so that you (and we) know what you are allowed to do. If you are not already working in one, then I would recommend looking into a natural deduction system. – Derek Elkins Aug 4 at 20:57
• sir pls elaborate. – Nascimento de Cos Aug 4 at 21:01
• This question has nothing to do with propositional-calculus. I changed tags accordingly. – Ruggiero Rilievi Aug 5 at 7:45

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))$$.

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/

• You do not need LEM. Rather than assuming the existence on line 2, instead just immediately assume $Pa$, and then introduce the existence, and from there derive $Qa$, so as to discharge the assumption and deduce $Pa\to Qa$ in the context of arbitrary term $a$. – Graham Kemp Aug 12 at 9:57
• $$\small\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}}\fitch{~~1.~~\exists x~A(x)\to\forall x~B(x)\hspace{10ex}\textsf {Premise}}{\raise{7ex}{[a]}~\begin{array}{|l}{\fitch{~~2.~~A(a)\hspace{16ex}\textsf{Assume}}{~~3.~~\exists x~A(x)\hspace{13ex}\exists\,\mathsf I~2\\~~4.~~\forall x~B(x)\hspace{12.5ex}\to\!\mathsf E~1,3\\~~5.~~B(a)\hspace{16ex}\forall\,\mathsf E~4}\\~~6.~~A(a)\to B(a)\hspace{11.5ex}\to\!\mathsf I~2{-}5}\end{array}\\~~7.~~\forall x~(A(x)\to B(x))\hspace{11ex}\forall\,\mathsf I~6}$$ – Graham Kemp Aug 12 at 10:17