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)