Logical statement question

I am trying to learn math on my own and am using Frédéric Mynard's "An Introduction to the language of Mathematics" as an introductory textbook for logic and proofs. Unfortunately, most of the exercises don't contain solutions, and I ignore if I am right or wrong with the answers. Could you provide advice about whether my answer for the following exercise is correct?

If the universe of discourse is the set of players, introduce appropriate predicates and propositions to give the logical form of the statement “The players will go back to work if agreement is reached about their salaries, but this will be achieved, if at all, only if some of them take early retirement.”

Let A(x): “x reaches an agreement about his salary”, G(x): “x goes back to work” and ER(y): “y takes early retirement”. Then:

∀x ((A(x) → G(x)) ∧ [((A(x) → G(x)) → (∃y ER(y))]

• Almost. The second half of your logical expression is not correct. – Don Thousand Apr 7 at 21:08
• I see. I'll turn it around in my head a little more, then. The second half uses connector 'only if', so it should be of the form p → q, where p: "This will be achieved' and q: " Some players take early retirement". I imagine that my mistake could lie in taking the 'this will be achieved' to refer to the whole previous statement (perhaps I should restrict it to one of the predicates, probably A(x)). – Manuel Del Río Rodríguez Apr 7 at 21:21

The statement can be interpreted in several reasonable ways, but I would say the 'this' in 'this will be achieved' refers to all the players coming to an agreement.

So, I would write the second part as $$\forall x \ A(x) \to \exists x \ ER(x)$$

And the first part I would interpret likewise as: all the players go back to work if all the players come to an agreement. That is, I wouldn't look at this as every player individually coming to an agreement and, if they do, going back to work, which would allow for some players to come to an agreement and going back to work while others do not come an agreement ... and as such may not go back to work

So, the first part I would do as:

$$\forall x \ A(x) \to \forall x \ G(x)$$

Together:

$$(\forall x \ A(x) \to \forall x \ G(x)) \land (\forall x \ A(x) \to \exists x \ ER(x))$$