Then we progressed for a while to prenex normal form where a claim is an interpreted logic sentence in a structure. The protocol corresponds to the quantifiers.
A better way to describe claims (still in prenex normal form) is to refer to a "rich" structure. We replace "interpreted logic sentence" with "interpreted logic sentence in a rich structure defined in a programming language". The quantifiers are only used to define the communication between the scholars in the corresponding semantic game; they describe the supporting actions to be carried out by humans.
The quantifier-free part of a prenex normal form is called the matrix. For SCG, the matrix is a program with return type Boolean. We don't require that the matrix be expressed in some logic; we use a Turing-complete programming language to express it. This makes it easier to define labs because programming is more user-friendly than a logic when it comes to expressing predicates efficiently.
Finally, we gave up the restriction to prenex normal form. A claim is now an interpreted logic sentence in a rich structure. We use the semantic game also to deal with Boolean operators.
The phrase: "Interpreted logic sentence in a rich structure" is intentionally ambiguous because we don't refer to a specific logic. The reason is that semantic games are defined for many logics that are relevant to formal sciences and the SCG approach works with all of them. Three prominent logics are first-order predicate logic, second-order predicate logic and independence-friendly logic.