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).

The game is based on dialogs between ExistsP and ForAllP. ForAllP tries to "trick" ExistsP into an inconsistency. But this does not mean that the claim is false. The goal of the dialogs is showing inconsistency, not logical falsity.

Just true and false claims

Note: +1 for one player means -1 for other player for simplicity.

Claim form: C = ForAll x in InstanceSet 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)
Player ForAllP has tricked player ExistsP into contradicting itself. Therefore ForAllP wins a point.

Agreement 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)
Player ForAllP agreed with claim C but ExistsP (now in opposer role) tricked ForAllP into a contradiction (ForAllP could not defend). Therefore ExistsP wins a point.

Claim form: C = Exists x in InstanceSet 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)
Agreement 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)

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

Many algorithmic problems are maximization problems.

Claim form: C(q0) = ForAll x in InstanceSet 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)
Agreement and strengthening are reduced to refutation. 
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)
Player ForAllP claimed a stronger claim but failed to defend the stronger claim against ExistsP. ForAllP contradicts itself. Therefore ExistsP gains a point.

Note

Agreement is a special case of strengthening: (C.q0)-(C'.q0)=0.

Claim form: C(q0) = Exists x in InstanceSet ForAll y in Solution: quality(x,y) < q0 

refute(C,ExistsP,ForAllP)
protocol
ExistsP provides instance x
ForAllP solves instance x ruturning a solution y
if quality(x,y) < q0 ExistsP wins  (successful defense)
else ForAllP wins (successful refutation; +1 ForAllP)
Agreement and strengthening are reduced to refutation. 
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.