Nash Equilibria and Their Elimination in Resource Games

1 Introduction

We will consider (individual) ideal resource games defined formally in Section 3. Each player i of a game will be endowed with a multiset of resources ✏i. An action for Player i will be to contribute a multiset of resources, subset of ✏i. 1 An outcome will be a context consisting of a multiset of resources resulting from the contributions of every player. Then, each player i has a goal γi, which is a resource, represented by one formula of Log. An outcome X satisfies the goal of Player i if there is a proof of X ` γi in the logic Log. This will mean that the resources in X can be consumed so as to produce γi. We will first consider preferences over outcomes that are dichotomous. (Section 4.) We can thus initially say that Player i prefers an outcome X over an outcome Y iff X ` γi and Y 6` γi. Some formal results will lead us to define in a second part parsimonious preferences, a finer notion of preference where i may be qualitatively indifferent between X and Y , but still prefer X over Y because i's contribution is strictly less in X than in Y . (Section 5.)

Games of resources aim at representing the strategic interactions between rational agents where some combinations of resources replace the abstract notions of action and preferences. In games of resources, players may be endowed with some resources and have preferences upon some resources to be available after the game is played. Players' actions also consist in making available some of the resources they are endowed with.

In this paper, we propose a class of games of resources that exploits the formalisms and reasoning methods coming from the literature in knowledge representation and computational logics, namely resource-sensitive logics: e.g., Linear Logic, Separation Logic, BI Logic [Girard, 1987; Reynolds, 2002; O'Hearn and Pym, 1999]. The languages of these logics allow a fine-grained description of resources, processes, and their harmonious combinations. In computer science, they have been quite successful at modeling systems for multi-party access and modification of shared structures, by allocation and deallocation of resources. Not based on naïve set theory or classical reasoning, the resources used in this paper will thus be supported with a rich logical language, elaborated semantics, and reasoning methods.

A resource is represented by one formula of a resourcesensitive logic Log. To make a start we assume here that Log is some propositional variant of Linear Logic.

We present two decision problems defined also in Section 3, the first of which is deciding whether an action profile is a Nash equilibrium. When dealing with resources, interesting questions arise as to whether some undesirable equilibria can be eliminated by a central authority by redistributing the available resources among the agents [Harrenstein et al., 2015]. We will thus study the decision problem of rational elimination. 2

One contribution of this paper is to demonstrate that it is possible to obtain rather general results for a large class of games of resources depending on the formal properties of the logic Log we start with. This offers the opportunity to tailor a game to the needs of a certain application without changing framework. We can indeed choose any sensible fragment of a resource-sensitive logic.

2 Elements of Linear Logic

A good introduction to Linear Logic and its variants is [Troelstra, 1992]. We will use logics defined on the language of propositional Linear Logic. The technical aspects of the paper can be grasped without a great understanding of the

1 Ideal resource games are said to be ideal because any subset of the endowments can be used by the players.

2 Rational construction [Harrenstein et al., 2015], is not presented here for reasons of space. We report briefly about it in Section 6.

Table 1: Sequent rules used in the proofs.

language. See for instance [Porello and Endriss, 2010] for an illustration of its modeling power in social choice theory. The results will however draw upon the proof theory and its rules. The ones we use here are presented in Table 1. A sequent is a statement Γ ` ∆ where Γ and ∆ are finite multisets of occurrences of formulas of Log. Often, we can conveniently write a multiset ¶A1↪ ▷ ▷ ▷ ↪An♦ as the list of formulas A1↪ ▷ ▷ ▷ ↪An. An intuitionistic sequent is a sequent Γ ` A with only one formula to the right. A sequent Γ ` ∆ is provable in Log if there exists a linear proof using the rules of the logic Log.

Intuitively, Γ ` ∆ being provable means that the resources in Γ can be transformed into the resources in ∆.

MLL is the multiplicative fragment:

where p is a propositional formula. MALL is the fragment with both additive and multiplicative operators:

A resource captured by a proposition of Linear Logic, can be atomic like one atom of hydrogen H or of oxygen O. It can be a tensor combination of resources, e.g., H2 ⌦O being a molecule of water. It can be a process transforming resources, e.g., (H2 ⌦ O) ⌦ (H2 ⌦ O) ( H2 ⌦ H2 ⌦ O2 would be the well known chemical reaction of electrolysis. Working harmoniously with resources and resource transformation processes with this meticulous control over their combination is made possible using resource-sensitive logics. In a game where a player is endowed with 2n molecules of water and a player is endowed with n processes of electrolysis, it is possible to consume these resources and produce 2n molecules of hydrogen gas and n of oxygen gas. But not more!

The logic is affine when it admits the structural rule of weakening (W) (see Table 1). We can quickly summarize the complexity of some fragments and variants of Linear Logic that could be used as the Log parameter to instantiate resource games. MALL is PSPACE-complete; MLL is NP-complete; Affine MLL is NP-complete; Affine MALL is PSPACEcomplete; Intuitionistic MALL is PSPACE-complete; Intuitionisitc MLL is NP-complete. See [Lincoln et al., 1992; Kanovich, 1994]. The results of this paper will be applicable to every fragment mentioned here.

Linear vs. affine reasoning and preferences Weakening (rules (W) in Table 1) in the logic Log or lack of it thereof, has important consequences. Weakening gives a monotonic flavor to the process of deduction in the logic. Weakening says that if something is deducible in a situation Γ, it will be deducible in every superset of Γ. Following the terminology in Linear Logic, in this paper, logics admitting weakening will be said to be affine and logics without weakening will just be said to be linear.

In the affine case, A↪ B ` A is a provable sequent. If γi = A, Player i will find her objective satisfied with an outcome ¶A↪B♦. In the linear case, we have in general A↪B 6` A (unless B is a vacuous resource equivalent to 1). If γi = A, Player i will not be satisfied with an outcome ¶A↪ B♦ as she wants A and nothing more.

3 Ideal resource games

Definition 1. An ideal resource game (IRG) is a tuple G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) where:

• ÷ N = ¶1↪ ▷ ▷ ▷ ↪ n♦ is a finite set of players;
• ÷ ✏i is a finite multiset of formulas of Log (i's endowment).
• ÷ γi is a formula of Log (i's goal);

Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n), we define: the set of possible actions of i as the set of multisets chi(G) = ¶C ♣ C ✓ ✏i♦, and the set of profiles in G as ch(G) = Qi2N chi(G). When P = (C1↪ ▷ ▷ ▷ ↪Ck) 2 ch(G) and 1  i  k, then P-i = (C1↪ ▷ ▷ ▷ ↪Ci-1↪Ci+1↪ ▷ ▷ ▷ ↪Ck). That is, P-i denotes P without player i's contribution. The outcome of a profile P = (C1↪ ▷ ▷ ▷ ↪ Cn) is given by the multiset of resources out(P ) = U1in Ci.

We will define "i strongly prefers P" in due time, reflecting dichotomous preferences first (Sec. 4) and parsimonious preferences second (Sec. 5).

Definition 2. Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n). A profile P 2 ch(G) is a Nash equilibrium iff for all i 2 N and for all Ci 2 chi(G), we have that i does not strongly prefer (P-i↪ Ci) over P .

Let us note NE(G) the set of Nash equilibria in ch(G).

A basic decision problem is the one of determining whether a choice profile is a Nash equilibrium.

NASH EQUILIBRIUM (NE)

• (in) An ideal resource game G and P 2 ch(G).

Some profiles that are not equilibria can have desirable outcomes. Some equilibria can have outcomes that are undesirable. Hence, it is interesting to investigate how resource distribution schemes influence how undesirable game equilibria can be eliminated and how desirable game equilibria can be constructed.

In the tradition of social mechanism design, redistribution schemes can be used by a central authority to enforce some behavior, either by disincentivizing a behavior or incentivizing a behavior.

We will study redistribution schemes in ideal resource games. Let ✏ be an endowment function such that for every player i we have ✏(i) = ✏i, a multiset of formulas of Log. A redistribution scheme of ✏ is an endowment function ✏0 such that

Given the ideal resource game G✏ = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏(1)↪ ▷ ▷ ▷ ↪ ✏(n)) we can apply a redistribution scheme where we modify the endowment function ✏ into ✏0 . We thus obtain the ideal resource game G✏0 = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏0 (1)↪ ▷ ▷ ▷ ↪ ✏0 (n)).

We will look at whether the outcome of a resource game can be rationally eliminated [Harrenstein et al., 2015]. That is, whether there is a resource redistribution such that no Nash equilibrium of the new resource game yields this outcome.

RATIONAL ELIMINATION (RE)

• (in) An ideal resource game G✏ and P 2 ch(G✏ ).
• (out) Is there a redistribution ✏0 of ✏ such that for all P 0 2 ch(G✏0 ): if out(P 0 ) = out(P) then P 0 62 NE(G✏0 )?

The decision problems are better understood with a specific type of preference in mind. Sec 4.2 and Sec 5.1 will illustrate them in due time, thus distinguishing the influence of dichotomous and parsimonious preferences.

4 Dichotomous preferences

Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) be an ideal resource game. For P 2 ch(G) and Q 2 ch(G), we say that player i 2 N strongly prefers P over Q (noted Q ≺i P) iff out(P) ` γi and not out(Q) ` γi.

Proposition 1. Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) be an ideal resource game, two profiles P 2 ch(G) and Q 2 ch(G), and a player i 2 N. When sequent validity in Log is in NP, the statement Q ≺i P is a NP^ coNP = BH2 predicate. When sequent validity in Log is in PSPACE, the statement Q ≺i P is a PSPACE predicate.

Proof. The corresponding language is L = ¶(P↪Q) ♣ Q ≺i P♦ = L1 \ L2 with L1 = ¶(P↪Q) ♣ out(P) ` γi♦, and L2 = ¶(P↪Q) ♣ not out(Q) ` γi♦. In particular, when Log is in NP, we clearly have that L1 is a NP language and L2 is a coNP language.

4.1 Finding Nash equilibria

Proposition 2. NE is as hard as the problem of checking sequent validity in Log, even when there is only one player.

We provide the full proof. 3

Proof. By applying the rules L ⇠ and R ⇠,

iff

is immediate. Thus we can w.l.o.g. consider only the intuitionistic sequents of Log in the following reduction.

Let Γ ` δ be the intuitionistic sequent where Γ is an arbitrary multiset of formulas of Log and δ is an arbitrary formula.

We can construct the ideal resource game G such that G = (¶1♦↪ δ↪ Γ[¶δ♦). G is thus the one-player ideal resource game where Player 1's goal is to achieve δ, and Player 1 is endowed with Γ [ ¶δ♦ (this is a set union but we could have chosen the endowment Γ ] ¶δ♦ as well). A profile in G is a choice of Player 1, that is, a subset C1 of Γ [ ¶δ♦. In this case for any profile P in G, out(P ) = P .

3 The other hardness proofs of this paper are analogous and will therefore be omitted.

We show that Γ ` δ iff Γ 2 NE(G).

From right to left, suppose that Γ 2 NE(G). This means that for all C1 ✓ Γ [ ¶δ♦, if C1 ` δ then Γ ` δ. Let in particular C1 = ¶δ♦. Indeed, C1 ✓ Γ [ ¶δ♦. Moreover, by (ax) we have δ ` δ. Hence, Γ ` δ follows.

From left to right, suppose that Γ ` δ. We need to show that Γ 2 NE(G). That is, for all C1 ✓ Γ [ ¶δ♦, if C1 ` δ then Γ ` δ. Since we supposed Γ ` δ, this is trivially true.

To establish an upper-bound on the complexity of NE let us first outline an algorithm for solving its complement. That is, checking whether a profile is not a Nash equilibrium. Let P 2 ch(G) be a profile. To determine whether P 62 NE(G), we can employ the following simple non-deterministic algorithm.

Algorithm 1 Naïve algorithm for NE

• 1: non-deterministically guess (i↪C 0 i ) 2 N ⇥ chi(G).
• 2: return P ≺i (P-i↪C 0 i ).

The following proposition is straightforward.

Proposition 3. If the problem of sequent validity checking of Log is in NP then NE is in coNP BH2 and indeed in ⇧ p 2 . If the problem of sequent validity checking of Log is in PSPACE then NE is in PSPACE.

We prove our first technical lemma.

Lemma 1. Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) be an ideal resource game . When Log is affine, P 62 NE(G) iff 9i 2 N : P ≺i (P-i↪ ✏i).

Proof. Suppose P 62 NE(G). There is i 2 N and Ci 2 chi(G) s.t. P ≺i (P-i↪Ci). By definition, out((P-i↪Ci)) ` γi and out(P) 6` γi. We have Ci ✓ ✏i, so by applying weakening (W) with every instance of formulas in ✏i ∩ Ci, we can prove that out((P-i↪ ✏i)) ` γi. We thus have that there is i 2 N s.t. P ≺i (P-i↪ ✏i). The other way around is immediate from the definition of Nash equilibria.

The next proposition follows immediately:

Proposition 4. Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) be an ideal resource game. When Log is affine: NE(G) 6= ; and (✏1↪ ▷ ▷ ▷ ↪ ✏n) 2 NE(G).

Lemma 1 helps us to establish the following result.

Proposition 5. When Log is affine, if the problem of sequent validity checking of Log is in NP then NE is in ∆ p 2 . If the problem of sequent validity checking of Log is in PSPACE then NE is in PSPACE.

Proof. Sketch. We use Algorithm 2. For correctness, note that the instructions of the lines 2-5 are equivalent to a test of whether out(P) 6` γi and out((P-i↪ ✏i)) ` γi, that is, P ≺i (P-i↪ ✏i). Lemma 1 ensures that exactly when there is an i 2 N such that P ≺i (P-i↪ ✏i) we can conclude that P is not a Nash equilibrium. The complexity is easy to establish.

Algorithm 2 Algorithm for NE with dichotomous preferences and affine Log

1: for each i 2 N do: 2: if (out(P) ` γi): 3: continue; 4: else if (out((P-i↪ ✏i)) ` γi): 5: return false. 6: return true.

4.2 Elimination

A very simple illustration of RATIONAL ELIMINATION is given by the ideal resource game G✏ = (¶1↪ 2♦↪ γ1 = B↪ γ2 = A↪ ¶A♦↪ ¶B♦). There are two players. Player 1 wants B but is endowed with ¶A♦, while Player 2 wants A but is endowed with ¶B♦. The game G✏ can be represented as follows. (We indicate the realized objectives assuming that Log is affine.)

One can rapidly check that all profiles are Nash equilibria. However, the profile (¶A♦↪ ¶B♦) is more 'socially desirable' than the others since it satisfies both players' goal.

A centralized authority could effectively eliminate the others by redistributing the resources present in G✏ so as to obtain G✏0 = (¶1↪ 2♦↪ γ1 = B↪ γ2 = A↪ ¶B♦↪ ¶A♦). The game G✏0 can be represented as follows.

The only Nash equilibrium is now the one with outcome ¶B↪ A♦. As a consequence of Prop. 4, we already know:

This is very specific to the affine case (and dichotomous preferences), and even then, it is of course not true of all Nash equilibria. To decide whether some outcome is rationally eliminable, one naïve approach consists in trying all possible redistributions and check whether the outcome is a Nash equilibrium in the resulting ideal resource game. Instead, we are going to exploit a pleasant property, analogous to [Harrenstein et al., 2015, Corollary 4].

Proposition 6. Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) be an ideal resource game. When Log is affine, the profile P such that out(P) = Uj ✏j is not rationally eliminable.

Let G✏ = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏(1)↪ ▷ ▷ ▷ ↪ ✏(n)) be an ideal resource game. For each player i 2 N, we define G[✏Bi] where [✏ B i] is the redistribution of ✏ where all resources are assigned to i, that is:

Because there is only one active player in G[✏Bi] , we will sometimes write a profile of G[✏Bi] as (Ci) with Ci 2 chi(G[✏Bi] ) instead of (;↪ ▷ ▷ ▷ ↪ ;↪ Ci↪ ;↪ ▷ ▷ ▷ ↪ ;), by abuse of notation.

Lemma 2. Let G✏ be an ideal resource game and P 2 ch(G✏ ). P is rationally eliminable iff there is a player i 2 N and a profile Q 2 ch(G[✏Bi] ), such that out(Q) = out(P) and Q 62 NE(G[✏Bi] ).

Proof. From right to left. Suppose Q 62 NE(G[✏Bi] ) for some i 2 N. Let also P 2 ch(G✏ ) be a profile and assume out(P) = out(Q). When there is at most one player with a non-empty endowment, as in [✏ B i], there is a one-toone correspondence between the set of profiles and the set of outcomes. Thus, there is one and only one profile in G[✏Bi] with outcome out(P) and it is Q. So there is a redistribution of ✏, namely [✏ B i], such that for all profiles Q 2 ch(G[✏Bi] ) with outcome out(P), we have Q 62 NE(G[✏Bi] ). So P is rationally eliminable.

From left to right. Suppose that P is rationally eliminable. Thus, there is a redistribution ✏0 of ✏ such that for all P 0 2 ch(G✏0 ), if out(P 0 ) = out(P) then P 0 62 NE(G✏0 ). So let R 2 ch(G✏0 ) be an arbitrary profile with out(R) = out(P). By assumption, we have that R 62 NE(G✏0 ). By definition of Nash equilibria, this means that there is i 2 N and C 0 i 2 chi(G✏0 ) such that R ≺i (R-i↪C 0 i ). Now consider the game G[✏Bi] . We have out(R) 2 chi(G[✏Bi] ) and out((R-i↪ C 0 i )) 2 chi(G[✏Bi] ). Let the profile R1 2 ch(G[✏Bi] ) with R1 i = out(R) and R1 j = ; when j 6= i. Let R2 2 ch(G[✏Bi] ) be the profile with R2 i = out((R-i↪C 0 i )) and R2 j = ; when j 6= i. Since, R ≺i (R-i↪C 0 i ), we also have R1 ≺i R2 . So R1 62 NE(G[✏Bi] ). The profile R1 is the only profile of G[✏Bi] with outcome out(P). So we can conclude.

Proposition 7. When Log is linear, RE is in NP BH2 when Log is in NP, and in PSPACE when Log is in PSPACE.

Proof. Sketch. We can use Algorithm 3. It guesses a player i

Algorithm 3 General algorithm for RE

1: non-deterministically guess (i↪C 0 i ) 2 N ⇥ chi(G[✏Bi] ). 2: return P ≺i (P-i↪C 0 i ).

and a deviation in the game G[✏Bi] for Player i from the profile (out(P)) 2 ch(G[✏Bi] ), and checks whether Player i has an incentive to do this deviation. By Lemma 2, if such a player and deviation exist and only if they exist, the profile P is rationally eliminable in G✏ . So the algorithm is correct. Using Prop. 1, basic complexity theory permits to conclude.

Proposition 8. When Log is affine, RE is in ∆ p 2 when Log is in NP, and in PSPACE when Log is in PSPACE.

Proof. Sketch. Consider Algorithm 4.

By Lemma 2, P is eliminable in G iff there is i 2 N where (out(P)) 62 NE(G[✏Bi] ). By Lemma 1, we know that (out(P)) 62 NE(G[✏Bi] ) iff P ≺i ([✏ B i](i)).

Proposition 9. RE is as hard as the problem of checking sequent invalidity in Log.

Algorithm 4 Algorithm for RE with dichotomous preferences and affine Log

1: for each i 2 N do: 2: if (P ≺i ([✏ B i](i))): 3: return true. 4: return false.

5 Parsimonious preferences

Weakening (W) is sometimes a desirable property of Log and of our preferences of resources. However, it has the untoward consequence of incentivizing players to spend all their resources in ideal resource games with dichotomous preferences. This is well exemplified for instance by Prop. 4.

We can teach our players parsimony by attaching to them finer preferences that take into account the realization of their objective, but also the optimality of their contribution.

In an ideal resource game G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n), we now say that player i 2 N strongly prefers P 2 ch(G) over Q 2 ch(G) (noted Q ≺i P) iff at least one of the following conditions is satisfied:

• ÷ not out(P) ` γi and not out(Q) ` γi and Pi ⇢ Qi
• ÷ out(P) ` γi and not out(Q) ` γi
• ÷ out(P) ` γi and out(Q) ` γi and Pi ⇢ Qi

Similar preferences have been called pseudo-dichotomous in the literature.

Proposition 10. Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) be an ideal resource game, two profiles P 2 ch(G) and Q 2 ch(G), and a player i 2 N. When sequent validity in Log is in NP, the statement Q ≺i P is a coBH4 predicate. When sequent validity in Log is in PSPACE, the statement Q ≺i P is a PSPACE predicate.

Proof. When Log is in NP, the definition of parsimonious preferences directly yields that the problem is in (coNP^ coNP) _ (NP^ coNP) _ (NP^NP). It corresponds to the class coBH4. See [Wechsung, 1985, Lemma 1.4].

5.1 Redistribution and parsimony

Consider again the ideal resource game of Section 4.2. (Unless stated otherwise, suppose we are in the affine case.) With parsimonious preferences, we have NE(G) = ¶(;↪ ;)♦. The profile (¶A♦↪ ¶B♦) is not a Nash equilibrium as it was with dichotomous preferences. It would be more desirable from a social welfare point of view than any other outcome (it satisfies both players), but the players would nonetheless not be individually rational by choosing it. They have indeed no bearing upon the outcome that satisfies them and thus are rational in withholding their resources.

Nonetheless, like in the case of dichotomous preference, we can effectively eliminate the current Nash equilibrium in G✏ (and construct the Nash equilibrium yielding ¶A↪ B♦) by redistributing the resources present in G✏ so as to obtain G✏0 = (¶1↪ 2♦↪ γ1 = B↪ γ2 = A↪ ¶B♦↪ ¶A♦). The only Nash equilibrium is now (¶B♦↪ ¶A♦).

Unlike dichotomous preferences, parsimonious preferences do not ensure the existence of a Nash equilibrium even in the affine case. Consider the ideal resource game H✏ = (¶1↪ 2♦↪ γ1 = A↪ γ2 = A ⌦ A↪ ¶A♦↪ ¶A♦). There are two players. The game H✏ can be represented as follows.

The game H✏ has no Nash equilibrium: At (;↪ ;), Player 1 does not realize her objective, but she can deviate and play ¶A♦ to satisfy it. At (¶A♦↪ ;), Player 2 has an incentive to deviate and play ¶A♦ to realize her objective. At (¶A♦↪ ¶A♦) Player 1 has an incentive to deviate and play ;. (In the affine case this is because she can still satisfy her objective by contributing less. In the linear case, this is because she can satisfy her objective while she does not before deviating.) At (;↪ ¶A♦), Player 2 does not satisfy her objective and thus has an incentive to deviate to play ;.

5.2 Finding Nash equilibria

Proposition 11. The problem NE is as hard as the problem of checking sequent invalidity in Log, even when there is only one player.

In the ideal resource game G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n), we can use Algorithm 1 to check whether a profile P 2 NE(G), even for parsimonious preferences. We have a result analogous to Prop. 3

Proposition 12. If the problem of sequent validity checking of Log is in NP then NE is in coNP BH4 and indeed in ⇧ p 2 . If the problem of sequent validity checking of Log is in PSPACE then NE is in PSPACE.

When Log is affine and we adopt parsimonious preferences, Algorithm 5 can be used to check whether P 2 NE(G).

Algorithm 5 Algorithm for NE with parsimonious preferences and affine Log

1: for each i 2 N do: 2: if (out(P) ` γi): { 3: for each A 2 Pi do: 4: if (out((P-i↪ Pi ∩ ¶A♦)) ` γi): 5: return false. 6: } else { 7: if (out((P-i↪ ✏i)) ` γi): 8: return false. 9: }

10: return true.

Proposition 13. When Log is affine, if the problem of sequent validity checking of Log is in NP and we adopt parsimonious preferences, then NE is in ∆ p 2 . If the problem of sequent validity checking of Log is in PSPACE, then NE is in PSPACE.

Proof. Sketch. To justify Algorithm 5, the following observation may help. When Log admits weakening, it is equivalent to the algorithm, where we substitute the lines 3 and 4 with:

3': for each Ci ⇢ Pi do: 4': if (out((P-i↪ Ci)) ` γi):

(In the worst case, the number of loop calls would be exponential in the size of Pi while it stays linear instead in the proposed version.) The reader can verify that P 2 NE(G) is a P NP[⌃i(1 + ♣Pi♣)] predicate.

5.3 Elimination

Lemma 2 also holds for parsimonious preferences. It is easy to see that the proof carries over. Algorithm 3 can still be used in the case of parsimonious preferences because Lemma 2 is still granted. We thus have the analogous to Prop. 7 for parsimonious preferences.

Proposition 14. When Log is linear, RE is in NP BH4 when Log is in NP, and in PSPACE when Log is in PSPACE.

We can do better in the affine case. Let G = (N↪ γ1↪ ▷ ▷ ▷ ↪ γn↪ ✏1↪ ▷ ▷ ▷ ↪ ✏n) be an ideal resource game and let P 2 ch(G) be a profile. We can use Algorithm 6 to check whether a profile P 2 ch(G) is rationally eliminable.

1: for each i 2 N do: 2: if ((out(P)) ≺i ([✏ B i](i))): 3: return true. 4: for each A 2 out(P ): 5: 6: return true.

if ((out(P)) ≺i (out(P) ∩ ¶A♦)): 7: return false.

Proposition 15. When Log is affine, RE is in P BH4 and indeed in ∆ p 2 when Log is in NP. It is in PSPACE when Log is in PSPACE.

Proof. Sketch. Lemma 2 which still holds with parsimonious preferences ensures that it is enough to consider the redistributions [✏ B i] for some player i. Algorithm 6, then checks for each of these redistributions whether Player i has an incentive to deviate in the game G[✏Bi] from the profile (out(P )) 2 ch(G[✏Bi] ) to any one of ([✏ B i](i)) 2 ch(G[✏Bi] ) or (out(P) ∩ ¶A♦) 2 ch(G[✏Bi] ) for some A 2 out(P). It is weakening (W) that justifies that it is enough to consider these profiles, because X 6` γi implies Y 6` γi for any multisets Y ✓X.

If f is the number of formulas in the outcome of P, at most n(1 + f) profiles will be compared to P. So the algorithm can be simulated by a deterministic oracle Turing machine in polynomial time with at most n(1 + f) calls to an oracle deciding parsimonious preferences (Prop. 10). The results then follow from the definitions of the complexity classes.

Proposition 16. RE is as hard as the problem of checking sequent invalidity in Log.

6 Conclusions

For both decision problems, for both types of preferences, we have studied four cases where proof-search in Log can have the following properties: affine vs. linear, and NP-complete vs. PSPACE-complete. Putting all together, it is easy to see that we have this theorem.

NP BH4 ✓ ⌃ p

2 -easy (Prop. 14) P BH4 ✓ ∆ p

Some proofs are rather repetitive and have been left out.

We did not present rational construction for reasons of space. Let an ideal resource game G✏ and a profile P 2 ch(G✏ ) be given, rational construction (RC) asks whether there is a redistribution ✏0 of ✏ such that there is P 0 2 ch(G✏0 ) where out(P 0 ) = out(P ) and P 0 2 NE(G✏0 ). We report that when Log is NP-complete, then RC is in ⌃ p 3 when Log is linear and in ⌃ p 2 when Log is affine. RC is PSPACE-complete when Log is PSPACE-complete. Those results hold for dichotomous and for parsimonious preferences.

Electric Boolean Games [Harrenstein et al., 2015] are an extension of Boolean games where playing a certain action has a numeric cost, and agents are endowed with a certain amount of 'energy'. Deciding whether a profile is a Nash equilibrium in a Boolean game is coNP-complete [Bonzon et al., 2006]. In Electric Boolean Games, deciding whether a profile is rationally eliminable is NP-complete. The trend is that the complexity of decision problems in ideal resource games is higher than for their counterparts in Electric Boolean Games. (Except for our result of triviality in Prop. 4.) In Boolean games, goals of players are expressed as classical propositional formulas. Moreover, game outcomes or profiles are in fact models of classical propositional logic, i.e., valuations. Checking whether the goal of a player is satisfied in a game profile is an easy problem in Boolean games. This is also true in Electric Boolean Games. In contrast in resource games, checking whether the goal of a player is satisfied in a game profile is as hard as proof search in Log.

We looked at individual games. The setting however allows one to rather easily build classes of coalition games. Some inspiration can surely be taken from the literature, e.g., [Wooldridge and Dunne, 2006; Dunne et al., 2010; Bachrach et al., 2013]. Finally, with the decision problems of rational elimination, there is a dimension of social choice theory and mechanism design. Formal frameworks investigating redistribution schemes and economic policies can be found for instance in [Harrenstein et al., 2015] again, or [Endriss et al., 2011; Levit et al., 2013; Naumov and Tao, 2015] and might be adapted here.