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