# The validity of $∀x(Bx↔∃yRxy)↔\big(∀x∃y(Bx→ Rxy)∧ ∀x∀y(Rxy→Bx)\big)$

$$(\forall x.B(x) \leftrightarrow \exists y. R(xy)) \leftrightarrow (\forall x \exists y.B(x)\rightarrow R(xy)) \land \forall xy. (R(x,y) \rightarrow B(x))$$ is a valid formula.

My attempt to prove the validity of RHS→LHS

RHS: $$B(x)$$ is true iff there exists a $$R$$-successor to $$x$$.

LHS: if B(x) is true and there exists an $$R$$-successor to $$x$$, then the both conjuncts seem to make sense and are right. If $$B(x)$$ and there exists no R-successor to $$x$$, then both conjuncts are trivially satisfied.

Hence, RHS→LHS.

The other direction is not so clear. Is there a simple-intuitive way to prove it?

• Can’t we just rewrite the $B(x) \leftrightarrow \exists y R(x,y)$ on the left as the two implications $B(x) \to \exists y R(x,y) \wedge \exists y R(x, y) \to B(x)$? Then after rewriting the second one a little by going back and forth between the implication and the disjunction, and fenagling with the quantifiers just a bit, that should show it’s equivalent with the right-hand side Apr 1 at 19:51
• I notice that your formal sentence is punctuated two different ways in the post title versus in the post body. Comparing them, it becomes clear that the full-stops in the latter are meant to function as delimiters. (And I'm guessing that you pasted the former from the linked Tree Proof Generator.) I definitely prefer the non-periods version, for being unambiguous by itself. Apr 2 at 6:26
• When you say that the L-to-R argument is unclear, do you mean the part where the ∃ in the antecedent becomes ∀ outside the conditional? See whether you agree that "If there is a black sheep, then Q" implies (in fact, is equivalent to) "For each sheep, if it is black, then Q". Apr 2 at 6:35