I am struggling to prove that

$\forall a (P(a) \vee \exists b P(b))$ is logically equivalent to $\exists a P(a)$

Here is my attempt to prove it:

~(∀a(P(a) ∨ ∃bP(b)) = ∃aP(a)
~∃a~(P(a) v ∃bP(b)) = ∃aP(a)
~∃a~P(a) and ~∀b~P(b)) = ∃aP(a)
therefore ~∃a~P(a) and ~∀b~P(b)) =/= ∃aP(a)

Is there any method to prove this aside from rules of inference and truth tables?

Can anyone give me some kind of help?

  • $\begingroup$ What kind of method did you have in mind, since you do not want to use rules of inference? Truth tables are pointless since this is a predicate calculus question (and thus truth tables are not used to determine truth). $\endgroup$ – Ove Ahlman Dec 8 '17 at 12:01
  • $\begingroup$ can i use rules of inference then, what bothers me is this predicate p(x) and p(y), i simply can't fathom when predicate and quantifier mix together in one question $\endgroup$ – octeuas Dec 8 '17 at 12:04
  • $\begingroup$ also is this correct > ~(∀a(P(a)∨ ∃bP(b)) =∃aP(a) > ~∃a~(P(a) v ∃bP(b)) =∃aP(a) >~∃a~P(a) and ~∀b~P(b))= ∃aP(a) therefore ~∃a~P(a) and ~∀b~P(b))=/= ∃aP(a) $\endgroup$ – octeuas Dec 8 '17 at 12:05
  • 1
    $\begingroup$ Quantifiers without predicates are not really feasible. I think you might need to read up on predicate logic, Structures, quantifiers, interpretations etc. $\endgroup$ – Ove Ahlman Dec 8 '17 at 12:18
  • 1
    $\begingroup$ The statement is true If the empty structure is not allowed. When I do logic it is allowed, however I know for some (especially compute rscientists) the empty structure is allowed. Regarding your proof in the comments, it is quite unreadable. Try to edit your question instead, and please use LaTeX. $\endgroup$ – Ove Ahlman Dec 8 '17 at 12:21

What you did isn't getting you any closer ...

Also, you should start with the LHS and eventually end up with the RHS: that's much more readable, and less subject to accidental circular reasoning, then what you did.

Now, it is not clear that you can actually do this one using purely equivalence rules anyway, but here is something you can do that approximates it (and is in fact a bit of a mix of a syntactical and semantical proof).

If $a,b,c,...$ denote the objects in your domain, then you can think of an existential like this:

$$\exists x \: \varphi(x) \approx \varphi(a) \lor \varphi(b) \lor \varphi(c) \lor ...$$

and likewise, a universal can be thought of as:

$$\forall x \: \varphi(x) \approx \varphi(a) \land \varphi(b) \land \varphi(c) \land ...$$

So now we can do:

$$\forall x (P(x) \lor \exists y \ P(y)) \approx$$

$$(P(a) \lor \exists y \ P(y)) \land (P(b) \lor \exists y \ P(y)) \land (P(c) \lor \exists y \ P(y)) \land... \Leftrightarrow \text{ (Distribution)}$$

$$(P(a) \land P(b) \land P(c) \land ... ) \lor \exists y \ P(y) \approx$$

$$(P(a) \land P(b) \land P(c) \land ... ) \lor P(a) \lor P(b) \lor P(c) \lor ... \Leftrightarrow \text{ (Absorption)}$$

$$P(a) \lor P(b) \lor P(c) \lor ... \approx$$

$$\exists x \ P(x)$$

The alternative would be to do a formal proof using rules of inference, rather than equivalence, as suggested in the comments.


Here's a proof using a Fitch-style proof checker:

enter image description here

As Graham Kemp mentioned in the comments below, I did not prove what the OP requested. The OP wanted a proof for the following:

$$ \forall x(Px \lor \exists y Py)\leftrightarrow \exists x Px $$

Here is that proof:

enter image description here

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

  • $\begingroup$ Mostly. Notice the bracket placement is actually $\forall x~(Px\vee\exists y~Py)$ rather than $(\forall x~Px)\vee(\exists y~Py)$. [ Although it does usually make only a minor difference to the proof layout; but it is significant in systems where the domain may be empty. ] $\endgroup$ – Graham Kemp Aug 17 at 1:42
  • $\begingroup$ @GrahamKemp Good point. I will have to adjust this proof. $\endgroup$ – Frank Hubeny Aug 17 at 1:56

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.