Existential and universal quantifiers provide an extremely useful language for making formal statements. You must understand them. A game between a prover and a verifier is a level of abstraction within which it is easy to understand and prove such statements.
The Loves Example: Suppose the relation (predicate) Loves(p1, p2) means that person p1 loves person p2. Then we have
|∃p2 Loves(Sam, p2)||“Sam loves somebody.”|
|∀p2 Loves(Sam, p2)||“Sam loves everybody.”|
|∃p1∀p2 Loves(p1, p2)||“Somebody loves everybody.”|
|∀p1∃p2 Loves(p1, p2)||“Everybody loves somebody.” ...|