Logic translation involving numerical quantifiers

Question

A stable party is group whose all members either
$1.$have no person they dislike in the group, or
$2.$have at most one disliked person in the group while also having a person that they like.

Any party with a member who either
$1.$doesn’t like another party member and has no friend to compensate, or
$2.$has at least two persons that she doesn’t like in the same party
is called unstable.

(original post of this definition.)

We denote $x$ Like/Dislike $y$ as $L(x,y)/D(x,y)$
(Note: To make each statement shorter, I will not write '$\forall x\in P$ where $P$ is a party' etc.)

Here is my translation:

$$\forall x(\underset{\text{1.}}{\underline{\forall y~\neg D(x,y)}}\lor\underset{\text{2.}}{\underline{\exists^{\le1}y ~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))}})\tag*{Stable}$$ For the definition of stable party, I think $1.$ already included in $2.$
But why the definition state this twice $?$
Here is the definition without $1.$ \begin{align} &\forall x(\overset{\text{2.}}{\overline{\exists^{\le1}y ~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))}})\\ \equiv&\forall x((\exists^{!0}y~D(x,y)\lor\exists^{!1}y~D(x,y))\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \equiv&\forall x((\forall y~\neg D(x,y)\lor\exists^{!1}y~D(x,y))\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \equiv&\forall x(\forall y~\neg D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))\\ &\hspace{2 ex}\lor\exists^{!1}y~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \equiv&\forall x(\underset{\text{$1.$}}{\underline{\forall y~\neg D(x,y)}}\lor\underset{\text{$2'.$}}{\underline{\exists^{!1}y ~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))}})\\ \end{align}

In another word the definition could be simplify to (or just remove $1.$ from the original definition):

A stable party is group whose all members either
$1.$have no person they dislike in the group, or
$2'.$have exactly one disliked person in the group while also having a person that they like.

---

Take the negation of simplified definition of stable: \begin{align} &\neg(\forall x(\forall y~\neg D(x,y)\lor\exists^{!1}y ~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))))\\ \equiv&\exists x(\exists y~ D(x,y)\land(\exists^{!0}y~D(x,y)\lor\exists^{\ge2}y~D(x,y))\lor\exists y~D(x,y)\land\forall z~\neg L(x,z))\\ \equiv&\exists x(\exists y~ D(x,y)\land\exists^{\ge2}y~D(x,y)\lor\exists y~D(x,y)\land\forall z~\neg L(x,z))\\ \equiv&\exists x(\underset{\text{$2.$}}{\underline{\exists^{\ge2}y~D(x,y)}}\lor\underset{\text{$1.$}}{\underline{\exists y~D(x,y)\land\forall z~\neg L(x,z)}})\ \end{align}

Not stable indeed match with the definition of unstable:

$$\exists x(\underset{\text{$1.$}}{\underline{\exists y~D(x,y)\land\forall z~\neg L(x,z)}}\lor\underset{\text{$2.$}}{\underline{\exists^{\ge2}y~D(x,y)}})\tag*{Unstable}$$

Did i translate this correctly$?$ Any suggestion would be appreciated.

Answer 1

Yes, the definition can indeed be simplified as you say: the requirement of everyone disliking at most 1 other person (where, if they do dislike someone, there is someone else to 'compensate' for it) covers the case where no one dislikes anyone. That is, if no one dislikes anyone, then disliking at most one is trivially. Therefore, 1) implies 2), and therefore $1 \lor 2$ should be equivalent to just $2$

Your demonstration of this is good as well. Translations are correct, and the formal derivation of equivalence as well ... though you may want to flesh out that last step a bit more as follows (also because it nicely shows the 'absorption' of the 'at most one' in the case that there are zero):

\begin{align} &\forall x(\overset{\text{2.}}{\overline{\exists^{\le1}y ~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))}})\\ \overset{\text{Definition } \leq 1}{\equiv}&\ \forall x((\exists^{!0}y~D(x,y)\lor\exists^{!1}y~D(x,y))\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \overset{\text{Definition } !0}{\equiv}&\ \forall x((\forall y~\neg D(x,y)\lor\exists^{!1}y~D(x,y))\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \overset{\text{Distribution } \land \text{ over } \lor}{\equiv}&\ \forall x(\forall y~\neg D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))\\ &\hspace{2 ex}\lor\exists^{!1}y~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \overset{\text{Distribution } \forall \text{ over } \land}{\equiv}&\ \forall x(\forall y~(\neg D(x,y)\land (D(x,y)\to\exists z~L(x,z)))\\ &\hspace{2 ex}\lor\exists^{!1}y~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \overset{\text{Implication}}{\equiv}&\ \forall x(\forall y~(\neg D(x,y)\land (\neg D(x,y)\lor\exists z~L(x,z)))\\ &\hspace{2 ex}\lor\exists^{!1}y~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \overset{\text{Absorption}}{\equiv}&\ \forall x(\forall y~(\neg D(x,y))\\ &\hspace{2 ex}\lor\exists^{!1}y~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z)))\\ \overset{\text{Drop Unncessary Parentheses}}{\equiv} &\ \forall x(\underset{\text{$1.$}}{\underline{\forall y~\neg D(x,y)}}\lor\underset{\text{$2'.$}}{\underline{\exists^{!1}y ~D(x,y)\land \forall y(D(x,y)\to\exists z~L(x,z))}})\\ \end{align}