# Refutation Protocol Explained

First we explain the mathematical subgame that is based on quantifier games in logic dating back at least to the 19th century. Then we generalize to general refutation protocols where you have personalized protocols like Survivor from the reality TV show.

In the mathematical subgame we have two players ExistsP and ForAllP. ExistsP is the player for existential quantifiers and ForAllP is the player for universal quantifiers. ExistsP is the proposer and ForAllP the opposer.

## ForAllExists

Propose: ExistsP makes a claim k(c) of the form ForAllExists, e.g., ForAll x in InstanceSet Exists y in Solution: p(x,y,c).

The refutation protocol is: ForAllP wants to refute k(c). ForAllP provides x0 and ExistsP provides y0. If !p(x0,y0,c) the refutation is successful and ForAllP successfully refutes. ForAllP wins reputation and ExistsP loses.

ForAllP wants to strengthen k(c) to k(c1) so that k(c1) => k(c). If ExistsP can refute k(c1) then the strengthening attempt is not successful and ForAllP loses reputation.

## ExistsForAll

Propose: ExistsP makes a claim k(c) of the form EA, e.g., Exists x in InstanceSet ForAll y in Solution: q(x,y,c).

The refutation protocol is: ForAllP wants to refute k(c). ExistsP provides x0 and ForAllP provides y0. If !q(x0,y0,c) the refutation is successful and ForAllP successfully refutes. ForAllP wins reputation and ExistsP loses.

ForAllP wants to strengthen k(c) to k(c1) so that k(c1) => k(c). If ExistsP can refute k(c1) then the strengthening attempt is not successful and ForAllP loses reputation.

## Beyond Logic

Now we switch to SCG (Scientific Community Game) where we can easily express the mathematical claims decribed above but also many more non-mathematical claims like survivor claims: I am the best. We switch now to a more generic terminology: ExistsP = proposer ForAllP = opposer Propose: The proposer makes a claim c where the refutation protocol is p with predicate pp(...) where ... stands for all the variables collected during the protocol. The opposer wants to refute c. The proposer and opposer follow the refutation protocol which might involves several steps between proposer and opposer. If !pp(...) the refutation is successful and the opposer successfully refutes. The opposer wins reputation and Alice loses. In some SCG playgrounds it makes sense to strengthen. The opposer wants to strengthen k(c) to k(c1) so that k(c1) => k(c). If the proposer can refute k(c1) then the strengthening attempt is not successful and the opposer loses reputation.