# Predicate logic proof

Prove the following formula.

$$\vdash (\exists x)(A \land B) \lor (\exists x)(A \land C) \equiv (\exists x)(A \land (B \lor C))$$ The question is number 10 in chapter 6 in "Mathematical Logic" by Tourlakis.

My try :

$$(\exists x)(A \land B) \lor (\exists x)(A \land C)$$ $$A \land (\exists x)B \lor A \land (\exists x)C$$ $$A \land ((\exists x)B \lor (\exists x)C)$$

I got stuck in that step.

• It's not true, the $\to$ direction fails. Commented Mar 30, 2014 at 0:30
• I see now you have a typo in the firsr connective,you mean $\land$ instead of $\lor$. Start by distributing $\exists$ over $\lor$. Commented Mar 30, 2014 at 0:36
• Which part exactly i have to do the distribution on ? Commented Mar 30, 2014 at 0:42
• See answer below. Commented Mar 30, 2014 at 0:45

You must follow Git Gud's answer and complete the proof with the formal details according to theorems and rules of your textbook.

We must use 6.1.7 Theorem. (Distributivity of $\forall$ over $\land$) : $\vdash (\forall x)(A \land B) \equiv (\forall x) A \land (\forall x) B$, page 158.

Start with : $(\exists x)(A \land (B \lor C)$ and rewrite with $\forall$ :

$\lnot (\forall x) \lnot (A \land (B \lor C))$

then use De Morgan : $\lnot (\forall x) (\lnot A \lor \lnot (B \lor C))$, De Morgan again : $\lnot (\forall x) (\lnot A \lor (\lnot B \land \lnot C))$, distribute : $\lnot (\forall x) ((\lnot A \lor \lnot B) \land (\lnot A \lor \lnot C))$, and De Morgan again : $\lnot [(\forall x) (\lnot (A \land B) \land \lnot (A \land C))]$.

Now we apply Th 6.1.7 :

$\lnot [(\forall x) \lnot (A \land B) \land (\forall x)\lnot (A \land C)]$.

Now, we "switch" again from $\forall$ to $\exists$ :

$\lnot [\lnot (\exists x) (A \land B) \land \lnot (\exists x) (A \land C)]$.

Finally, we apply again De Morgan :

$\lnot \lnot [(\exists x) (A \land B) \lor (\exists x) (A \land C)]$

and Double Negation :

$(\exists x) (A \land B) \lor (\exists x) (A \land C)$.

• But we want to proof $(\exists x)(A \land B) \lor (\exists x)(A \land C)$ not $\land$. Commented Mar 30, 2014 at 20:18
• When you applied de morgan before applying 6.1.7, you took the negation outside beside the quantifier. Can you really do that ? Iam confused Commented Mar 30, 2014 at 20:57
• The external negation is never moved; until the last step (double negation) it stay in front of the complete formula. Commented Mar 30, 2014 at 21:03