Dialogical semantics
The game is governed by rules, such as:
G((? 1 ? ? 2); M) begins by the verifier’s choice of i=1 or i=2. The game is continued as G(? i; M).
G(? ? ; M) is like G(? ; M), except that the roles of the two players are reversed.
For an atomic sentence p, G(p; M) is won by the verifier and lost by the falsifier if p is true in M; the other way around if p is false in M.