# Language, Proof & Logic (LPL) Exercise 11.21 - Sentences 7, 9

I'm working on LPL's Exercise 11.21, which asks to provide translations of the English language sentences into First Order Logic sentences. Unlike the majority of exercises in the book, as I understood, this one requires an experienced instructor to check them as it cannot be verified by the automatic grading system which governs the rest of the course.

For that reason I'd like to ask you to check my translations here for the 2 sentences, for which I received "We could not determine whether your sentence was correct" from the grading system.

The predicates to be used

• Pet(x) - x is a pet
• t < t' - t is earlier than t'
• Hungry(x, t) - x was hungry at time t
• Owned(x, y, t) - x owned y at time t
• Gave(x, y, z, t) - x gave y to z at time t

Exercise 11.21

Translate the following into FOL.

7) If Max ever gave Claire a pet, she owned it then and he didn't.

9) Max fed all of his pets before Claire fed any of her pets.(Assume that "Max's pets" are the pets he owned at 2:00, and the same for Claire.)

My (proposed) solutions

7) $$\forall x \forall t \Bigg( Pet(x) \rightarrow \\ \bigg( \exists u \big( Gave(max, x, claire, u) \land u < t \big) \rightarrow \\ \Big( Owned(claire, x, t) \land \neg Owned(max, x, t) \Big) \bigg) \Bigg)$$

9) $$\exists t \Bigg( \\ \forall x \Big( \big( Owned(max, x, 2:00) \land Pet(x) \big) \rightarrow \exists u \big( u < t \land Fed(max, x, u) \big) \Big) \\ \land \\ \neg \exists x \Big( Owned(claire, x, 2:00) \land Pet(x) \land \exists u \big( u < t \land Fed(claire, x, u) \big) \Big) \Bigg)$$

• @AndreySurovtsev Did you try my sentence for 7) below? – Bram28 Dec 23 '18 at 17:15
• @Bram28 yes, it works, sorry for the late response – Andrey Surovtsev Jun 13 at 20:44

$$\forall x \forall t ((Pet(x) \land Gave(max, claire, x, t)) \rightarrow (Owned(claire,x,t) \land \neg Owned(max,x,t)))$$