THE ESSENCE OF THE QUANTIFIER GAME This game has been known for at least two centuries. You propose, oppose (refute, strengthen) or agree with claims to maximize points you collect. There are two players: ExistsP (usually proposer) and ForAllP (usually opposer). Just true and false claims: *********************************************** Note: +1 for one player means -1 for other player for simplicity. Claim form: C = ForAll x in Instance Exists y in Solution: p(x,y) where p is a predicate. refute(C,ExistsP,ForAllP) protocol ForAllP provides instance x ExistsP solves instance x ruturning a solution y if p(x,y) ExistsP wins (successful defense; refute returns false) else ForAllP wins (successful refutation; refute returns true; +1 ForAllP) ================= Everything else is reduced to refutation. ================= agree(C,ExistsP,ForAllP) protocol refute(C,ForAllP,ExistsP) if p(x,y) agreement is successful (nobody wins) else unsuccessful (+1 ExistsP) Claim form: C = Exists x in Instance ForAll y in Solution: !p(x,y) refute(C,ExistsP,ForAllP) protocol ExistsP provides instance x ForAllP solves instance x ruturning a solution y if !p(x,y) ExistsP wins (successful defense) else ForAllP wins (successful refutation; +1 ForAllP) agree(C,ExistsP,ForAllP) protocol refute(C,ForAllP,ExistsP) if !p(x,y) agreement is successful (nobody wins) else unsuccessful (+1 ExistsP) Notes: refute(C,ExistsP,ForAllP) = !refute(!C,ForAllP,ExistsP) if same instance and solution are used. In other words, if there is a way to refute a claim, the same approach works to defend the negation of the claim. There is a function quality(x,y) which returns the quality of solution y for instance x. For the first claim form, the function quality(x,y) assumes only two values, say 0 and 1. p(x,y) = (quality(x,y) = 1) Maximization Claims: *********************************************** Claim form: C(q0) = ForAll x in Instance Exists y in Solution: quality(x,y)>=q0 refute(C,ExistsP,ForAllP) protocol ForAllP provides instance x ExistsP solves instance x ruturning a solution y if quality(x,y)>=q0 ExistsP wins (successful defense) else ForAllP wins (successful refutation; +1 ForAllP) agree(C,ExistsP,ForAllP) protocol refute(C,ForAllP,ExistsP) if quality(x,y)>=q0 agreement is successful else unsuccessful (+1 ExistsP) strengthen(C,C',ExistsP,ForAllP) where C'.q0 > C.q0 protocol refute(C',ForAllP,ExistsP) if quality(x,y)>=C'.q0 strengthening is successful else unsuccessful (+1 ExistsP) Note: agreement is a special case of strengthening: (C.q0)-(C'.q0)=0. Claim form: C(q0) = Exists x in Instance ForAll y in Solution: quality(x,y)