Logical consequence predicate logic

Question

(∃x)(P(x) ∧ ¬(C = x)) ∨ (∃y)(¬P(y) ∧ C = y) (formula A)

is a logical consequence of:

(∀z)(P(z) ⇔ ¬(C = z))  (formula B)

This would imply that if B is true then A is also true (modus ponens) and if B is untrue then A is also untrue (modus tollens).

Let's say you need to prove that A is a logical consequence of B. I would imagine you would rewrite formula B's equivalence to a disjunction of conjuctions. But from there I'm kinda stuck on what to do.

Any help is appreciated.

Answer 1

Hint

(B) is $(∀z)[(P(z) \to ¬(C = z)) \land (¬(C = z) \to P(z))]$.

Then we use the tautological equivalence: $(A \to B) \equiv (\lnot A \lor B)$ to get:

$(∀z)[(\lnot P(z) \lor \lnot (C = z)) \land ((C = z) \lor P(z))]$.

Now, apply Distributivity.

We have to note that we have logical consequence and not equivalence; thus from the formula above we get the existentially quantified one: $\forall z \alpha \vDash \exists z \alpha$ and then, having transformed the inner conjunction into a disjunction (using Distributivity) we can "distribute" $\exists$ over $\lor$ [see Prenex operations] to safely move from : $\exists z (\varphi \lor \psi)$ to:

(A) $\exists x \varphi \lor \exists y \psi$.