1
$\begingroup$

$(\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?

$\endgroup$
3
  • $\begingroup$ 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 $\endgroup$
    – Stephen Donovan
    Apr 1 at 19:51
  • $\begingroup$ 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. $\endgroup$
    – ryang
    Apr 2 at 6:26
  • $\begingroup$ 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". $\endgroup$
    – ryang
    Apr 2 at 6:35

0

Reset to default

You must log in to answer this question.