{'fraction_non_alphanumeric': 0.040749796251018745, 'fraction_numerical': 0.005817384706179918, 'mean_word_length': 4.074005418508484, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A New Game Equivalence and its Modal Logic

We revisit the crucial issue of natural game equivalences, and semantics of game logics based on these. We present reasons for investigating finer concepts of game equivalence than equality of standard powers, though staying short of modal bisimulation. Concretely, we propose a more finegrained notion of equality of"basic powers"which record what players can force plus what they leave to others to do, a crucial feature of interaction. This notion is closer to game-theoretic strategic form, as we explain in detail, while remaining amenable to logical analysis. We determine the properties of basic powers via a new representation theorem, find a matching"instantial neighborhood game logic", and show how our analysis can be extended to a new game algebra and dynamic game logic.


Introduction
Games are a basic model for interactive agency, but how much structure do we want to consider? Game theory offers strategic form games and extensive games, which represent two levels of structure, less or more detailed. Logic of games has also looked at other natural invariances between representations of games, such as equivalence of powers for players. As in other areas of mathematics, the search for natural invariances continues, and in this paper we offer a new notion bridging between game theory and logic: strong power equivalence, that uses powers encoding a sort of qualitative equilibria. We determine its properties in a new representation theorem for the "basic powers" in a game, show that it has a natural associated logic, and that it supports an interesting new game algebra where the methodological principle of compositionality eventually forces us to change from functional to relational strategies. Besides the representation theorem for basic powers, the main technical contribution of the paper is a completeness theorem for the new game logic that we define. The proof uses a technique developed in [3], but requires a non-trivial adaptation due to the presence of extra frame constraints.
We believe that our proposed game equivalence is new, but even so, it fits with a body of earlier work. Our approach is partly inspired by the extensive computational literature on process equivalences, ranging from coarser trace equivalence to more fine-grained notions of bisimulation [10]. Even more central in our approach was the by now standard notion of power equivalence, implicit in the game algebra of Parikh [13], which also links with the set-theoretic forms for games presented in [4]. Another obvious precursor inside game theory is the celebrated transformation analysis of equivalent games with imperfect information by Thompson [14] (refined by Elmes and Reny in [6]), which is close to power equivalence. But game theory also has comparative discussions of the information available in exten-sive forms and in strategic normal forms [7], a style of analysis that remains to be connected to our representation theorems and logics for different levels of describing games.
Finally, it should be said that further intuitions of game equivalence emerge once we consider players' preferences, so that game equivalence can also refer to correlations between available equilibria. This further level is beyond the scope of this paper, but it would be a natural next step to take.

Powers and power equivalence
We begin by reviewing a standard logical notion of game equivalence in terms of powers of the players. For a standard overview of the basic concepts of game theory, see [12]. For more on equivalence of extensive games, see [4,6,14].

Definition 1.
A tree T is a prefix closed subset of N * , subject to the condition that if w · j ∈ T and i < j then w · i ∈ T as well. The empty word ε is the root of the tree.
Definition 2. An extensive game G for a finite set of players A with outcomes in the set O is a tuple (T ,t, o, Π) where T is a finite tree, t a map from T to A, o a map from branches of T to O, and Π a partition of T subject to the following condition: for any pair w, v within the same partition cell of Π, w and v have the same number of children in T , and furthermore t(n) = t(n ′ ). If all partition cells of Π are singletons we call G a game of perfect information, and we omit Π.
Maximal branches of T will also be called full matches, and prefixes of maximal branches are called partial matches.
A strategy for player a ∈ A is a map σ : t −1 [a] → N where w · σ (w) is a child of w for each w with t(w) = a, and σ (w) = σ (w ′ ) whenever w, w ′ are in the same partition cell in Π. A strategy profile is a tuple (σ a ) a∈A of one strategy for each player in A. A strategy profile p completely determines a full match, and hence a leaf of the game tree, so we can speak of the outcome of p, denoting it by o(p). Generally, we say that a full match m of G is guided by the strategy σ for a if for every prefix w of m such that t(w) = a, σ (w) is also a prefix of m. Match(σ ) is the set of σ -guided matches.
We denote the set of games for players A with outcomes in O as G(A, O). For two-player games we call the players by A (Alice) and B (Bob). We set A = B and B = A.
Note that we have not attributed payoffs to matches in a game or preferences over the outcomes, but rather (and more generally) simply outcomes from some fixed chosen set. In this sense we are dealing with game forms rather than proper games. We return to the issue of preferences in Section 7.1.
Given a player a ∈ A we let P a (G ) denote the set of powers of a in G .
Two games G 1 , G 2 ∈ G(A, O) are power equivalent if for all a ∈ A: P a (G 1 ) = P a (G 2 ). We denote this by G 1 ∼ G 2 . If P a (G 1 ) = P a (G 2 ) for some specific a ∈ A, we write G 1 ∼ a G 2 .
Every game G in G(A, O) gives rise to a tuple (P a (G )) a∈A of subsets of O, which represents a crucial aspect of social scenarios: the abilities of participants to force outcomes.
Powers in two-player games, our focus in what follows, are characterized by three formal properties, for a set of outcomes O, and a pair F A , F B of families of subsets of O: Consistency If P ∈ F A and Q ∈ F B , then P ∩ Q = / 0. A representation theorem also holds for perfect information games, with this additional property: For proofs of these results we refer to [2].

Neighborhood logic and bisimilarity
The use of neighborhood semantics to interpret a propositional dynamic logic of powers in determined games dates back to [13]. Here, we review a modal logic GL for powers in two-player games from [2], which drops the game constructions (for these, see Section 6) as well as determinacy, referring explicitly to powers of separate players in the syntax. Given a set of propositional variables Prop, the syntax of GL is given by the following grammar: The semantics for this logic uses neighborhood models that assign each player a neighborhood relation representing the powers of that player relative to each world. Of course, we must impose suitable constraints to ensure that these actually behave as powers of players in some game. The representation result Theorem 1 tells us what these should be: We define the interpretations of all formulas in a game model M = (W, R A , R B ,V ) as follows: Game models come with a natural notion of bisimulation: Forth For all Z such that uR P Z, there exists a Z ′ such that u ′ (R ′ P )Z ′ and the following condition holds: Back For all Z ′ such that u ′ R P Z ′ there is some Z such that uR P Z and the following condition holds: We say that pointed game models M, w and N, v are power bisimilar, written M, w ←→ N, v, if there is a power bisimulation B between M and N such that wBv.
All formulas of GL are invariant for power bisimilarity: The logic GL can be axiomatized by a simple extension of monotone (multi-)modal logic. Here is a version using axiom schemata and a rule of replacement of equivalents: where θ [ϕ/ψ] is the result of substituting some occurrences of the formula ψ by ϕ in θ . We denote this system of axioms by GL and write GL ⊢ ϕ to say that the formula ϕ is provable in this axiom system. Theorem 3. The logic GL is sound and complete for validity on game frames.
The completeness proof is an exercise involving a straightforward canonical model construction, which we omit. Furthermore, GL is decidable and has the finite model property.
3 Rethinking powers and game equivalence 3.1 From powers to strategic equivalence Power equivalence, while a natural and simple notion of game equivalence, is relatively coarse. In particular, it misses much of the interactive nature of games. To illustrate what we mean by this, here is an example from [2].
Consider the two games depicted in Figure 1. In both games, each player can perform two actions "left" and "right", and there are three possible outcomes 1, 2, 3. If Alice moves left, then the outcome is 1 regardless of the action chosen by Bob, but if Alice moves right, the outcome depends on the actions of Bob: if Bob moves left, the outcome is 2, otherwise 3. The difference lies in which player moves first. In the figure, the game where Alice chooses first is depicted to the left, and the game where Bob chooses first to the right. Figure 1: Two power equivalent games.
It is easy to see that each player has the same powers in both games, and this is the basis for standard game logics (the games represent two sides of a standard propositional distribution law). But the interaction of the players looks different: in the right game, A has an obvious strategy for which the possible outcomes are precisely 1 and 2. But in the left game, the only way that A can exclude the outcome 3 is to go left at the start of the game, making 1 the only possible outcome. Thus, it is doubtful if one should see these games as equivalent.
Another way of phrasing the difference is this. The two games differ if we think of powers more 'socially' as what a player is going to force while at the same time recording which choices are left intentionally to the other player. That is, both players have a say, and the notion of power becomes oriented toward both players, more in the spirit of game-theoretic equilibrium. This intuition can be made a bit more precise if we bring in a standard game-theoretic device. Let us display the strategic forms of the two games, with rows corresponding to strategies for A and columns strategies of B: Looking at the yields of columns and rows, the above difference is clear. Here is a finer notion of game equivalence, inspired by the 'matrix logic' of [1]: Definition 6. Let G 1 and G 2 be two-player games over the set of outcomes O. A strategy profile bisimulation between these two games is a relation R ⊆ P 1 × P 2 , where P 1 is the set of strategy profiles of G 1 and P 2 is the set of strategy profiles of G 2 , such that if (σ 1 , τ 1 )R(σ 2 , τ 2 ), then: We call G 1 and G 2 are strategic form equivalent if there is a strategy profile bisimulation R between them, relating every profile in P 1 to some profile in P 2 , and vice versa.
This equivalence concept is more fine-grained than power equivalence. In particular, the power equivalent games displayed in Figure 1 are not strategic form equivalent, as can be seen by inspecting their matrix forms. However, this approach sacrifices much of the logical simplicity of power equivalence. We therefore proceed to modify the notion of power itself in line with the above strategic form perspective.

Basic powers and strong equivalence
Our proposed new game equivalence works as follows.
Definition 8. Two games G 1 and G 2 are strongly power equivalent, written Strong power equivalence is more fine-grained than power equivalence: the two games in Figure 1 are not strongly power equivalent. It also retains a connection to strategic forms.
Proposition 2. Any two strategic form equivalent games are strongly power equivalent, and any two strongly power equivalent games are power equivalent.
All inclusions are strict here. Here are two games that are strongly power equivalent but not strategic form equivalent -displayed in strategic form with outcome set {0, 1}: In the matrix on the right, the profile in the middle upper square is not bisimilar with any profile on the left.
As a prelude to our later logical analysis, we generalize strong power equivalence to games with different outcomes. Given whereR is the Egli-Milner lifting of R. I.e., ZRZ ′ if, for all x ∈ Z, there is x ′ ∈ Z ′ with xRx ′ , and vice versa. It is clear that strong power equivalence is a special case of this.
Having proposed our new notion of game equivalence, we now determine its basic properties. This is the content of the following representation theorem for basic powers. Obviously, the earlier monotonicity condition has to be dropped, since it typically fails on our new reading of powers as also offering choices to the other player. On the other hand, this role for the other player also validates a new condition that did not hold before. Consider any pair F A , F B ⊆ P(O):

satisfies the Non-emptiness, Instantiatedness and Consistency conditions if, and only if, there exists a game G such that F
We can give a more compact statement of these conditions in terms of the above Egli-Milner lifting. Then the Instantiatedness and Consistency conditions together become: for all P ∈ F A , we have P ∈F B , and for all P ∈ F B , we have P ∈F A .
In order to prove the theorem, it will be convenient to work with games in strategic form: Definition 9. A strategic form two-player game with outcomes in O is a tuple (Σ A , Σ B , o) such that Σ A and Σ B are non-empty sets (interpreted as strategy sets for each player) and o : We can define powers and instantiated powers for strategic form games in the expected manner. In particular an instantiated power for Player A is a subset P of O such that, for some strategy σ ∈ Σ A : and dually for B. Since every extensive game has a strategic normal form, and conversely every strategic form game is the strategic normal form of some extensive game of imperfect information, we can work with strategic and extensive games interchangeably (see for example [12]).
It is straightforward to check that the conditions Non-emptiness, Consistency and Instantiatedness hold for the instantiated powers of any game. For the converse, let F A , F B ⊆ P(O) be given, and suppose all three conditions hold for the pair (F A , F B ). We shall construct a game G such that the instantiated powers of each player P in G coincides with the set F P . We construct G as a strategic form game, as follows: • The set Σ A of strategies for A is defined as the collection of all maps c : Σ B → O such that: • The outcome map o sends a strategy profile (c, (Z, u, j)) ∈ Σ A × Σ B to c(Z, u, j).
The set Σ B is non-empty by the Non-emptiness condition, and it will follow from Claim 1 below that Σ A is also non-empty. The appearance of the set O × {0, 1} in this construction is merely a way to create "enough copies" of each set in F B to make sure that certain suitable strategies for A can be defined. In particular, it allows us to establish the following claim: . We can modify this g to obtain a map by mapping u ∈ Z to the triple (g(u), u, 0). We can now define the strategy c as follows: given a triple (g(u), u, 0) in the image of Z under the map g ′ , we set c(g(u), u, 0) = u. For every triple (Z ′ , u ′ , k) not in the image of g ′ , we set c(Z ′ , u ′ , k) to be some arbitrary element of Z ∩ Z ′ , which exists by the Consistency condition. Clearly we get that the image of the set F B × O × {0, 1} under the map c is equal to Z. Furthermore, since c(Z ′ , u ′ , k) ∈ Z ′ for each triple (Z ′ , u ′ , k), we get that c is a legitimate strategy for A in G .
A second claim that we will need is the following: We now show that every instantiated power for either player P is an element of F P , and vice versa. We have four different inclusions to prove, two for each player.
Suppose that Z ∈ Conversely, suppose that Z is an instantiated power for A in G . Then there exists a strategy c for A such that the possible outcomes consistent with c are precisely the members of Z. It follows that To prove the inclusions for B we need the following claim:  (Z, u, k) is of the form c(Z, u, k) for some strategy c ∈ F A , which means that u ′ = c(Z, u, k) ∈ Z. Conversely, if u ′ ∈ Z then by Claim 2 there exists a strategy c for A such that c(Z, u, k) = u ′ . So u ′ is an outcome that is consistent with the strategy (Z, u, k), hence u ′ ∈ Z ′ . So we get Z = Z ′ , and the proof is finished.
We can now easily prove both of the inclusions for B: if Z ∈ F B , then (Z, u, 0) is a legitimate strategy for B for any arbitrarily chosen u ∈ O, and it now follows directly from Claim 3 that Z is an instantiated power for B. Conversely, if Z is an instantiated power for B in G then there is some strategy (Z ′ , u, k) for B witnessing this. By Claim 3 we get Z = Z ′ , and since (Z ′ , u, k) is a strategy for B we have Z ′ ∈ F B . So Z ∈ F B , and we are done.
From this proof, we can also read off the following result: Theorem 5. Our properties of basic powers also capture the powers computed from rows and columns of matrix games.
At present we do not have a representation theorem for basic powers in the special case of perfect information games. It is easy to find additional conditions on powers that hold in this setting, but we have not yet found a complete set.

The logic of basic powers: instantial game logic
What is the game logic that goes with strong power equivalence? Our earlier notion of strategy bisimulation points the way. It resembles the instantial neighborhood bisimulations introduced in [?] as the invariance underlying instantial neighborhood logic. Accordingly, we now introduce a logic for games at this level of structure. The syntax of instantial game logic IGL is given by the following grammar: where Ψ ranges over finite sets of formulas of IGL. We sometimes write [P](ψ 1 , ..., ψ n ; ϕ) rather than The semantics of IGL, as for GL, uses neighborhood models. However, the constraints are different, since we are now dealing with basic powers. These constraints come from our representation result for basic powers Theorem 4. The key clause in the truth definition in instantiated game models M = (W, R A , R B ,V ) runs as follows: If we interpret formulas as 'outcomes', then we see why IGL is a natural language for basic powers: the formula [P](Ψ; Ψ) says that Ψ is a basic power for the player P, while the weaker formula [P] Ψ says that Ψ is simply a power.
Instantial models come with a notion of bisimulation which stands to strong power equivalence as standard neighborhood bisimulations stands to power equivalence: Definition 11. Let M = (W, R,V ) and M ′ = (W ′ , R ′ ,V ′ ) be any neighborhood models. The relation B ⊆ W × W ′ is said to be an instantial neighborhood bisimulation if, for all uBu ′ and P ∈ {A, B}, we have: Forth For all Z such that uR P Z, there is some Z ′ such that u ′ (R ′ P )Z ′ and the following conditions hold: Back For all Z ′ such that u ′ R P Z ′ there is some Z such that uR P Z and the following condition holds: Pointed instantial game models M, w and N, v are instantial neighborhood bisimilar, M, w ←→ N, v, if some instantial neighborhood bisimulation B between M and N has wBv.
Formulas of IGL are invariant for instantial bisimilarity: More can be said about the model theory of instantial neighborhood simulation, but the present facts suffice here.

Axiomatizing IGL
In this section we axiomatize the valid formulas of IGL, thus pinning down the modal logic of basic powers. Our system is a gentle modification of instantial neighborhood logic.
We denote this system of axioms by IGL and write IGL ⊢ ϕ to say that the formula ϕ is provable in this axiom system. Theorem 6. The system IGL is sound and complete for validity over instantial game models.
The soundness part of this result is checked case by case, and the easy argument is omitted. The completeness proof proceeds via a normal form argument, following an idea in [3]. The adaptation to the present setting is not trivial however, since we have to deal with the new frame constraints of Nonemptines, Consistency and Instantiatedness. The main contribution here is thus to prove that the model construction satisfies these constraints. We outline the key parts of the proof below.
Definition 12. The modal depth of a formula is defined inductively by: Definition 13. Given a finite set of propositional variables Q, a formula ϕ is said to be a Q-formula if all propositional variables appearing in ϕ belong to Q.
Given k ∈ ω and a finite set Q of propositional variables, a (Q, k)-description is a consistent Qformula ϕ of modal depth ≤ k, such that for any Q-formula θ of depth ≤ k, we have ϕ ⊢ θ or ϕ ⊢ ¬θ .
Note that there are at most finitely many Q-formulas of depth ≤ k, given that Q is finite. We omit the (standard) argument for this.
The key lemma for the completeness proof is the following: where I is a finite set and for each i ∈ I, Θ i is a finite set of (Q, k)-descriptions, such that: -every member of Θ i provably entails ϕ, and -every member of Γ is provably entailed by some member of Θ i .
For a proof of this lemma, see [3]. Now fix a finite set of propositional variables Q. Given a Q-formula ϕ let ϕ denote the equivalence class of the formula under provable equivalence. For a finite set of formulas Γ set We construct a neighborhood model M = (W, R,V ) as follows: • For a player P let R P be the union of the sets Note that this is well defined, i.e. whether ( ϕ, Γ) ∈ R P is independent of the choice of witnesses ϕ, Γ of the equivalence classes. The following lemma can be proved exactly as in [?], and we refer to that paper for the details: Lemma 2 (Truth lemma). Let M be constructed as above, and let ψ be any basic formula of modal depth ≤ k whose propositional variables all belong to Q and such that all game terms appearing in ψ belong to τ. Then for every (Q, τ, k)-description ϕ, we have: The addition we need to make here is the following lemma: Lemma 3. The structure M construced above is a game model, i.e. it satisfies the Non-emptiness, Consistency and Instantiatedness constraints.
Proof. First, note that all the conditions hold for the image of each relation on an element of W of the form ( ϕ, 0). So we can focus on the images of relations of the form R P on states of the form ( ϕ, k + 1) for some k. The Non-emptiness condition is proved straightforwardly using the axiom (Non-Em), we leave this to the reader. For Instantiatedness, suppose that . By the axiom (Inst) we get ϕ ⊢ [B](θ ; ⊤) as well. Since ϕ is a (Q, k + 1)-description, we can derive from Lemma 1 that there is some set Ψ of (Q, k)-descriptions such that ϕ ⊢ [B](Ψ; Ψ), and such that there exists some ψ ∈ Ψ with ψ ⊢ θ . But since ψ, θ are both (Q, k)-descriptions, clearly this means that θ = ψ, so ( θ , k) = ( ψ, k). But this means that we get (( ϕ, k + 1), Ψ × {k}) ∈ R B and ( θ , k) ∈ Ψ × {k} as required. The converse direction is proved in the same manner.
Combining Lemmas 3 and 2 with the easy observation that any consistent basic formula of depth ≤ k, variables in Q and atomic games among τ is provably entailed by some (Q, k)-description 1 , we obtain Theorem 6.
As a corollary to this proof, we get: The logic IGL is decidable and has the effective finite model property.
IGL is a high-level logic of basic powers in social interaction. The reader may find it of interest to see what the above axioms say when read as statements about games.

Adding game operations
Our third contribution in this paper concerns the addition of structure to games, in the form of natural game operations.

Game algebra of strong powers
In this section we use some basic concepts of universal algebra, see for example [5]. For simplicity, we restrict attention to finite games, so that G ({A, B}, O) is now the set of finite games with outcomes in O. Thus the outcome map of a game G can be viewed a map o from the leaves in G into O.
Consider a set of games on a fixed set of outcomes O. We define operations in a standard manner, with binary +, × corresponding to choice for A, B respectively, and a unary operation − for game dual ('role switch'). The game G 1 + G 2 (G 1 × G 2 ) is defined as follows: let G 1 = (T 1 ,t 1 , o 1 , Π 1 ) and let G 2 = (T 2 ,t 2 , o 2 , Π 2 ). We first construct the tree T ′ by adding a new root r with two successors, and the left successor is the root of a subtree isomorphic with T 1 via a fixed isomorphism i 1 , the right successor is the root of a subtree isomorphic with T 2 via a fixed isomorphism i 2 . The turn function t ′ is defined by setting t ′ (r) = A (t ′ (r) = B). For a node u in the subtree corresponding to the left successor of the root r we set t ′ (u) = t 1 (i 1 (u)) and similarly for a node u in the subtree corresponding to the right successor of the root r we set t ′ (u) = t 2 (i 2 (u)). The outcome map o ′ is defined by setting o ′ (l) = o 1 (i 1 (l)) for a leaf in the subtree corresponding to the left successor of r, and o ′ (l) = o 2 (i 2 (l)) for a leaf in the subtree corresponding to the right successor of r. We define a partition Π ′ by setting The construction of −G i is much simpler, it merely changes the turn assignment by switching players at each position, otherwise keeping everything the same. The equational theory of the algebra G is of special interest here, as it can be viewed as a new weaker propositional logic, where distributivity fails, witness our example in Figure 1. By contrast, for standard power equivalence, this algebra is known to be a distributive de Morgan algebra.
But with strong power equivalence, much more basic principles than distributivity fail. For instance, the operations × and and + are not idempotent, the following equations fail: For the first failure, take a two-player game G in which A has the first move, and simply chooses between two outcomes 0, 1. Then {0, 1} is a basic power of A in G × G , but not in G . Still, many laws known from game algebra do go through.
Proposition 5. The following equations hold in G:

Dynamic game logic for basic powers
Our game algebra still misses one important operation, namely, sequential composition. For this operation to make sense, we need to take a dynamic view of games as state-transforming processes, in the style of dynamic game logic (cf. [13], [9], [2]).

Definition 15.
A dynamic two-player game over a set X (of "states") is a map g : X → G({A, B}, X ), assigning a game with outcome set X to each state in X . We denote the set of dynamic two-player games over X by D ({A, B}, X ).
The operations +, × and − are naturally lifted to dynamic games by defining them component-wise in an obvious manner, and so are the relations ∼, ≃ of power equivalence and strong power equivalence. Now, given dynamic games g 1 , g 2 : X → G({A, B}, X ), we can define the sequential composition g 1 • g 2 by letting g 1 • g 2 (u) be constructed by replacing each leaf l in g 1 (u) by a copy of the game tree g 2 (o 1 (l)), where o 1 is the outcome map associated with g 1 (u).
In this way, we get an extended game algebra. For power equivalence, the complete algebra of the propositional operations plus sequential composition has been axiomatized in [8,15]. For basic powers and strong equivalence in our new sense, however, this is an open problem.
However, we now run into some unexpected trouble: To see why this is so, consider the two perfect information games displayed in Figure 2, which have an obvious instantiantial neighborhood bisimulation between them. The games are not strongly power equivalent, since player B has a basic power {x, y} in the game to the right, but not to the left. But both games can clearly be obtained as the sequential composition of strongly power equivalent games: Figure 2: A threat to compositionality: instantial bisimulation does not preserve basic powers.
This failure might seem a serious challenge to the compositional methodology of dynamic game logic. But when we analyze what goes wrong in the example, the reason is the functional character of strategies. They force a unique choice at each turn, making B too specific in the game on the left.
To remedy this situation, we suggest to widen the notion of a strategy to allow non-determinism, so that strategies may constrain the moves of a player, but not determine them uniquely. This is not altogether foreign in game theory: in fact, mixed strategies can be interpreted in a similar way, and the same move has also been defended for the broader notion of a 'plan' in [2].
Definition 16. A relational strategy for player P in a game G = (T ,t, o, Π) is a binary relation σ over T such that: , and if u, v are in the same partition cell in Π.
The set Match(σ ) of non-deterministic matches guided by a strategy σ is defined in the obvious way. We say that P ⊆ O is a basic relational power of P if there is a relational strategy σ for P in G such that P = {o(m) | m ∈ Match(σ )}. The set of basic relational powers of P is denoted by R P (G ). We say that G 1 , G 2 are semi-strongly power equivalent if R P (G 1 ) = R P (G 2 ), for each P ∈ {A, B}. Finally, we write G 1 ≡ G 2 when G 1 , G 2 are semi-strongly power equivalent.
The relation of semi-strong power equivalence can be lifted to an equivalence relation between dynamic games in the same component-wise manner as before.
The move to relational strategies does not trivialize the new equivalence concept proposed in this paper. The two games in our running example of Figure 1 are not semi-strongly power equivalent, so this slightly coarser equivalence notion is still fine enough to make the distinction that we wanted. Furthermore, we get the result we are after: In this game algebra, we get a number of interesting valid equations known from the game algebra of power equivalence: Proposition 8. The following equations hold in D: Note also that some equations that were not valid in the functional setting now become valid, such as idempotence: x+x = x. In this way the algebra is closer to the algebra of games under power equivalence, but does not collapse to it: the distribution law x × (y + z) = (x × y) + (x × z) still fails, for example.
Relational strategies improve our game algebra. At the same time, our earlier results go through with suitable modifications. In particular, our representation theorem for basic powers is easily amended to capture relational basic powers. Consider the following condition on pairs Finally, our basic game logic can also be extended with game terms to capture this algebraic reasoning, in the style of dynamic game logic, [13], [2]. We will then have instantial modalities describing basic powers of player i in game G: This formalism can be interpreted on our instantial game models, when we provide these with worlddependent basic power relations for all players. The crucial point here is that, with the earlier obstacle to compositionally overcome, we can define the power relation for a product game G 1 • G 2 in the following inductive manner.
This is the basis for obvious recursion axioms for the game operations that lead to the following result.
Theorem 9. The dynamic game logic of relational basic powers is completely axiomatizable.
This logic has interesting further properties that deviate from known systems, especially in its axiomatization of game iteration, which we will treat in a separate publication.

Further directions
In this final section we briefly consider some directions for future reseach, in particular: • Enriching the logic with epistemic modalities to reason about imperfect information.
• Incorporating preference into the framework of basic powers and instantial game logic.
• Placing instantial game logic and strong power equivalence in a wider view perspective on the many possible game logics and notions of game equivalence.

Imperfect information
In this paper, we have worked with imperfect information games from the start. This raises some issues of intuitive interpretation. Imperfect information in games can arise for quite different reasons: players' limited powers of observation of moves, but also players' uncertainty about the strategies of other players. All this brings in what players know about the game, and a richer game logic reflecting this would have to incorporate epistemic modalities. Moreover, imperfect information sits somewhat uneasily with our game algebra, since information sets can cross between subgames, disrupting the obvious compositional structure. We have side-stepped this issue in the definition for our game operations, but at the price of dealing with only a special class of imperfect information games. Clearly, a lot remains to be clarified.

Preference
This paper has studied 'game forms' with abstract outcomes without any specified preference ordering. A natural next step is to consider proper games in which the players have preference orders over the set of outcomes. This is necessary to connect the game equivalences we have considered here with standard game theoretic concepts such as Nash equilibrium or solution methods like the elimination of dominated strategies. Adding modalities for preference is a well-known device in game logics, so we could also do this. But preference does raise questions for our perspective. For instance, the games in Figure 1 have different Backward Induction solutions with preference 2 < 1 < 3 for B, 1 < 3 < 2 for A. We may have to redefine our basic powers in the presence of preference, considering only preference-optimal sets for a player. But solution methods like Backward Induction also incorporate one particular view of rationality: they make an assumption about agents, rather than being part of the neutral mathematics of the game. Perhaps we need to study game equivalences parametrized to particular types of player.

A multitude of game logics
This paper does not claim that there is one best level for viewing games. Extensive form, standard powers, or strategic form all have their virtues, and we have merely claimed that there is room for one more natural new option. All these levels come with their own logical languages matching the invariance relation, [2]: relational modal logic for extensive games, modal neighborhood logic for standard powers, instantial neighborhood logic for our basic powers, and multi-modal logics accessing the different dimensions of matrix games.
This raises a systematic question. How are all these different logics related, given natural transformations from one level of game structure to another? For instance, on finite games, the modal logic of forcing powers can be translated into a µ-calculus on the underlying extensive games, and the same is true of our instantial modalities for basic powers, using the observations in Section 6. But modalities for strategic form games are not easily compared with our forcing modalities: moving across rows or columns means considering alternative strategies for players, something that would require a serious extension of our forcing language. In addition, matrix logics have surprising features that have no counterpart in our forcing logics, such as the undecidability of the full system for three players, which reflect the undecidability of the product logic S5 × S5 × S5 [11].
We believe that systematizing the total picture of game logics and their interrelations holds great interest, but we must leave this for further investigation.