Numerically definite quantification in logic

Question

I am attempting to translate the following sentence into formal logic:

"At most, two people are strong and they hate each other" Where Sx: x is strong and Hxy: x hates y

I have translated this as:

(∃x)(∃y)(Sx^Sy)^Sz)->(x=y∨x=z)^(Hxy^Hyx)

However I am not sure whether the order should look more like this:

(∃x)(∃y)(x=y∨x=z)->(Sx^Sy)^Sz)^(Hxy^Hyx)

I would appreciate any help in clarifying this, thank you.

I am a beginner in logic, so please do not judge my attempts too harshly!

Answer 1

This is a very awkward English statement, and it is quite ambiguous to me.

I can see at least three different readings:

1. There are definitely two people that are strong and they hate each other, but that there are no other strong people

This would translate as:

$$\exists x \exists y (x \not = y \land Sx \land Sy \land \forall z (Sz \rightarrow (z= x \lor z = y) \land Hxy \land Hyx)$$

2. There are at most two strong people, and whenever you have two strong people they will hate each other

This would translate as:

$$\forall x \forall y ((x \not = y \land Sx \land Sy) \rightarrow (\forall z (Sz \rightarrow (z= x \lor z = y)) \land Hxy)) $$

3. There is at most 1 pair of strong people hating each other (so you may have other strong people, but there would be no more than one mutual hate relationship between two strong people)

This would translate as:

$$\forall x \forall y ((x \not = y \land Sx \land Sy \land Hxy \land Hyx) \rightarrow \forall v \forall w ((v \not = w \land Sv \land Sw \land Hvw \land Hwv) \rightarrow ((v = x \land w = y) \lor (v = y \land w = x))))$$