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

  • 3
    $\begingroup$ 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. $\endgroup$ – Derek Elkins Aug 4 at 20:57
  • $\begingroup$ sir pls elaborate. $\endgroup$ – Nascimento de Cos Aug 4 at 21:01
  • 1
    $\begingroup$ This question has nothing to do with propositional-calculus. I changed tags accordingly. $\endgroup$ – 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:

enter image description here

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":

enter image description here

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/

  • $\begingroup$ 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$. $\endgroup$ – Graham Kemp Aug 12 at 9:57
  • $\begingroup$ $$\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}$$ $\endgroup$ – Graham Kemp Aug 12 at 10:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.