Discovering Theorems in Game Theory: Two-Person Games with Unique Pure Nash Equilibrium Payoffs

1 Introduction

Given that both modern computer science and modern game theory were John von Neumann in 1950s [Shoham, 2008], it is only fitting that there has been enormous intersections between the two subjects. While the applications of game theory concepts, models as well as theorems to computer science domains have been ubiquitous these days, the opposite direction remains limited on topics such as computational complexities of various solution concepts in games [Halpern, 2007]. In this paper, however, we explore a new application of computer science to game theory. We will show how AI search and knowledge representation techniques can be used to discover some interesting theorems about pure Nash equilibria.

Traditional equilibrium analysis has been mostly focused on mixed strategy equilibria. Part of the reasons for this bias is that such an equilibrium always exists and algorithms such as the one by Lemke-Howson are guaranteed to find one. Moreover, best response functions in games with mixed strategies are continuous and differentiable, allowing for standard calculus techniques to be applied.

However, pure Nash equilibria (PNEs) are also of interest, and there is already much work about them. Examples here include the existence of PNEs in (ordinal) potential games [Monderer and Shapley, 1996], (quasi-)supermodular games

∗Supported in part by HK RGC CERG616707.

[Topkis, 1998] as well as games with dominant strategies, and uniqueness of PNE payoffs 1 in two-person strictly competitive games [Moulin, 1976].

In this paper, as part of our project on using computers to discover theorems in game theory, we consider the possibility of using computers to discover new classes of two-person games that have unique PNE payoffs. Our starting point is the class of two-person strictly competitive games. We first formulate the notions of games, strictly competitive games and PNEs in first-order logic. Under our formulation, a class of games corresponds to a first-order sentence. In particular, the sentence that corresponds to the class of strictly competitive games is a conjunction of two binary clauses with all variables universally quantified. So we implemented a program that examines all these universally quantified conjunctions of binary clauses to see if there is another such condition that also captures a class of games with unique PNE payoffs. We did not expect much as these conditions are rather simple, but to our surprise, our program returned a condition that is more general than the strict competitiveness condition. As it turned out, it exactly corresponds to Kats and Thisse's [1992] class of weakly unilaterally competitive two-person games. Our program also returned some other conditions. Two of them capture a class of "unfair" games where one player has advantage over the other. The remaining ones capture games where everyone gets what he wants - each receives his maximum payoff in every equilibrium state, thus there is no real competition among the players. Thus one conclusion that we can draw from this experiment is that among all classes of games that can be expressed by a conjunction of two binary clauses, the class of weakly unilaterally competitive games is the most general class of "competitive" and "fair" games that have unique PNE payoffs. Of course, this does not mean that the other conditions are not worth investigating. For instance, sometimes one may be forced to play an unfair game.

For the same set of conditions, we also consider strict twoperson games where different profiles have different payoffs for each player. Among the results returned by our program, two of them are exactly the two conjuncts in Kats and Thisse's weakly unilaterally competitive condition, but the others all turn out to be special cases of games with dominant strategies. Motivated by these results, we consider certain equivalent classes of games, and show that a strict game has a unique PNE iff it is best-response equivalent [Rosenthal, 1974] to a strictly competitive game.

1 Note that the uniqueness of PNE payoffs is also an ordinal property, which means all the PNEs in a game are equally preferred to all players. In particular, the notion of unique PNE payoffs degenerates to unique PNEs in strict games.

The rest of the paper is organized as follows. We first review some basic concepts in two-person games in strategic form, and then reformulate them in first-order logic. We then show that for a class of conditions, whether any of them entails the uniqueness of PNE payoff needs only to be checked on games up to certain size. We then describe a computer program based on this result, and report our experimental results.

2 Two-person games

A (two-person) game (in strategic form) is a tuple (A,B,≤1 , ≤2), where A and B are sets of strategies of players 1 and 2, respectively, and ≤1 and ≤2 are total orders on A×B called preference relations for players 1 and 2, respectively.

Instead of two preference relations, a two-person game can also be specified by two payoff functions, one for each player, which map profiles to numbers. The relationship between these two formulations are as follows: for any profiles s and s′ , s ≤i s′ iff ui(s) ≤ ui(s′ ), where ui is the payoff function for player i. In the following, we shall use these two formulations interchangeably.

In the following, two profiles (a, b) and (a′ , b′ ) are said to be equivalent if their payoff profiles are the same: (u1(a), u2(b)) = (u1(a′ ), u2(b′ )). In terms of preference relations, (a, b) and (a′ , b′ ) are equivalent iff

for i = 1, 2.

For each b ∈ B, we define B1(b) to be the set of best responses by player 1 to the strategy b by player 2:

Similarly, for each a ∈ A, the set of best responses by player 2 is:

A profile (a, b) ∈ A×B is a Pure Nash Equilibrium (PNE) if both a ∈ B1(b) and b ∈ B2(a). A game can have exactly one, more than one, or no PNEs. We say that a game has a unique PNE payoff if all the PNEs are equivalent.

One interesting class of two-person games is that of strictly competitive games. A game is strictly competitive [Moulin, 1976] if for every pair of profiles s1 and s2 in A × B, we have that s1 ≤1 s2 iff s2 ≤2 s1. Thus in strictly competitive games, the two players' preferences are exactly opposite.

Strictly competitive games have many nice properties. If (a, b) and (a′ , b′ ) are both PNEs of a strictly competitive game, then (1) they are equivalent; (2) they are interchangeable in the sense that (a′ , b) and (a, b′ ) are also PNEs. Thus if a strictly competitive game has PNEs, then their payoffs must be the same. Furthermore the unique PNE payoff can be computed using the minmax procedure.

Another class of games that we shall consider in this paper is that of strict games. A game is strict if for both players, different profiles have different payoffs, that is, (a, b) = (a′ , b′ ) whenever (a, b) ≤i (a′ , b′ ) and (a′ , b′ ) ≤i (a, b), where i = 1, 2. As we shall see, strict games have some nice properties that general games do not have.

3 Formulating two-person games in first-order logic

We consider a first-order language with two sorts α and β, equality, and two predicates ≤1 and ≤2. We use "∧" for conjunction, "∨" for disjunction, "¬" for negation, "⊃" for implication, and "≡" for equivalence. Negation has the highest precedence, followed by conjunction and disjunction, implication, and then equivalence. The rule of precedence can be overridden by a new line. For instance, the following expression

stands for the sentence (p ⊃ q) ∧ (q ⊃ p).

In our language, sort α is for player 1's strategies, and β for player 2's strategies. In the following, we use variables x, x1, x2, .. to range over α, and y, y1, y2, ... to range over β. The two predicates represent the two players' preference relations. In the following, as we have already done above, we write ≤i (x1, y1, x2, y2) in infix notation as (x1, y1) ≤i (x2, y2), i = 1, 2, and (x1, y1) ≃i (x2, y2) as a shorthand for

where i = 1, 2. We also write (x1, y1) <i (x2, y2) as a short-

The two relations need to be total orders (in the rest of the paper, unless otherwise stated, all free variables in a displayed formula are assumed to be universally quantified from outside):

where i = 1, 2. In the following, we denote by Σ the set of the above sentences. Thus two-person games correspond to firstorder models of Σ, and two-person finite games correspond to first-order finite models of Σ. This correspondence extends to other type of games as well. For instance, let Σs be the union of Σ with the following two axioms:

Then strict games and models of Σs are isomorphic.

We now show how some other notions in game theory can be formulated in first-order logic. The condition for a profile (ξ, ζ) to be a PNE is captured by the following formula:

In the following, we shall denote the above formula by NE(ξ, ζ).

The following sentence expresses the uniqueness of PNE payoff in a game:

A game is strictly competitive if it satisfies the following property:

Thus it should follow that

Notice that we have assumed that all free variables in a displayed formula are universally quantified from outside. Thus (6) is a sentence of the form ∀x1, x2, y1, y2ϕ. Similarly for (5).

Theorems like (7) can actually be generated automatically using the following theorem.

Theorem 1 Suppose Q is a formula without quantifiers, ⃗x1 and ⃗x2 tuples of variables of sort α, and ⃗y1 and ⃗y2 tuples of variables of sort β. We have that

1. Σ |= ∃⃗x1∃⃗y1∀⃗x2∀⃗y2Q ⊃ (5) iff for all model G of Σ such that |A| ≤ |⃗x1| + 2 and |B| ≤ |⃗y1| + 2, we have that G |= ∃⃗x1∃⃗y1∀⃗x2∀⃗y2Q ⊃ (5), where A is the domain of G for sort α, and B the domain of G for sort β.
2. Σ |= ∃⃗x1∃⃗y1∀⃗x2∀⃗y2Q ⊃ ¬∃x, y.NE(x, y) iff for all model G of Σ such that |A| ≤ |⃗x1| + 1 and |B| ≤ |⃗y1| + 1 we have that G |= ∃⃗x1∃⃗y1∀⃗x2∀⃗y2Q ⊃ ¬∃x, y.NE(x, y), where A is the domain of G for sort α, and B the domain

of G for sort β.

Proof: "Only if" is trivial. To show "if", suppose there is a game G (model of Σ) such that it satisfies the condition ∃⃗x1∃⃗y1∀⃗x2∀⃗y2Q but has two non-equivalent PNEs, (a, b) and (a′ , b′ ): either (a, b) ̸≃1 (a′ , b′ ) or (a, b) ̸≃2 (a′ , b′ ). Thus there is a tuple ⃗a1 of elements from A and a tuple ⃗b1 of elements from B such that |⃗a1| = |⃗x1|, |⃗b1| = |⃗y1|, and G satisfies

which is obtained from (∀⃗x2∀⃗y2Q) by replacing in it every free occurrence of each variable in ⃗x1 by its corresponding element in ⃗a1, and every free occurrence of each variable in ⃗y1 by its corresponding element in ⃗b1. Now construct a new game G′ = (A′ , B′ ,≤′1 ,≤′2 ) as follows:

• A′ = {a, a′ } ∪ ⃗a1 and B′ = {b, b′ } ∪ ⃗b1.
• ≤′1 is the restriction of ≤1 on A′ , and ≤′2 is the restriction of ≤2 on B′ .

Notice that this game is well-defined as ≤′1 and ≤′2 are both total orders, i.e. G′ |= Σ. Clearly, the size of G′ is smaller or equal to (|⃗x1| + 2) × (|⃗y1| + 2), both (a, b) and

(a′ , b′ ) are still non-equivalent PNEs of G′ , and the formula ∃⃗x1∃⃗y1∀⃗x2∀⃗y2Q is still true in G′ .

In other words, to prove that a sentence of the form ∃⃗x1∃⃗y1∀⃗x2∀⃗y2Q is a sufficient condition for the uniqueness of PNE payoff, it suffices to verify that this is the case for all games of sizes up to (|⃗x1| + 2) × (|⃗y1| + 2), and to prove that it is a sufficient condition for the non-existence of PNE, it suffices to verify this for games of sizes up to (|⃗x1| + 1) × (|⃗y1| + 1).

Theorem 1 holds for many specialized games as well. For instance, it holds for strict games as well.

Theorem 2 Theorem 1 holds when Σ is replaced by Σs.

In fact, Theorem 1 holds when Σ is replaced by any set of universally quantified sentences.

4 Theorem discovering

Since p ≡ q is logically equivalent to (¬p∨q)∧(p∨¬q), the condition (6) for strictly competitive games can be written as a conjunction of two binary clauses:

where each li, 1 ≤ i ≤ 4, is a literal, i.e. either an atom or the negation of an atom. As we mentioned, we want to know if there are other sentences of the form (8) that also capture classes of games with unique PNE payoffs. In the following, we say that a condition ϕ is a uniqueness condition if whenever a game satisfies this condition, it has unique PNE payoff, that is, if Σ |= ϕ ⊃ (5).

Based on Theorem 1, a straightforward way of discovering uniqueness conditions of the form (8) is as follows: For each condition of the form (8), check that if a 2 × 2 game does not have unique PNE payoff, then it does not satisfy this condition. There are 810,000 such conditions, 1950 non-isomorphic 2 × 2 two-person games, and among them 709 games that do not have unique PNE payoffs. Thus this strategy can be implemented on a modern computer even by brute-force search.

The search space can also be pruned by noticing that the conditions of the form (8) are not independent. For instance, condition

entails (is stronger than) condition

Once we know that a condition C is a uniqueness condition, those that entail C are no longer interesting as they become special cases of C, thus can be pruned.

However, checking logical entailment is in general not decidable for first-order logic. But as a strategy for pruning search space, we can use a weaker notion called subsumption on conditions of the form (8): C subsumes C′ if there is a substitution σ such that Cσ = C′ . For our language, subsumption can be checked efficiently, and the search tree can be designed in such a way that the condition associated with a node always subsumes the conditions associated with the ancestors of the node. Thus once a condition is found to be a uniqueness condition, the entire sub-tree under this condition can be pruned.

However, we still need a way to check for complete logical entailment under Σ for conditions of the form (8). This is because we want every condition returned by our program to be a most general, "weakest" uniqueness condition in the sense that it does not entail any other uniqueness condition of the form (8). Fortunately, this can be done using the following proposition.

Proposition 1 To check whether condition ∀⃗x1⃗y1Q1 entails condition ∀⃗x2⃗y2Q2 for all two-person games, it suffices to check this for all games up to max{|⃗x2|, 1} ×max{|⃗y2|, 1}, where Q1 and Q2 are formulas without quantifiers. This result holds for strict games as well.

Notice that what we have described applies to the task of discovering uniqueness conditions of the form (8) for strict two-person games as well.

We now report our experimental results, first for general two-person games, and then for strict two-person games.

5 General games

For two-person general games, our program returns the following seven uniqueness conditions for 2x2 games.

By Theorem 1, these are also uniqueness conditions for all two-person games. Furthermore, since these are the only conditions returned by our program, for any sentence C of the form (8), if it is a uniqueness condition, then it must entail one of the above conditions under Σ. In other words, the above seven conditions are the weakest (most general) uniqueness conditions of the form (8).

Notice that condition (10) and condition (11) are symmetric in the sense that one can be obtained from the other by swapping the roles of the two players. So are (12) and (13), and (14) and (15). On the other hand, (9) is symmetric to itself. It is easy to see that if two conditions are symmetric, then one is a uniqueness condition iff the other is.

Condition (9) looks like condition (6) for strictly competitive games, except that the strategy of one of the players is fixed in each implication. As it turned out, it captures exactly the class of two-person games that are weakly unilaterally competitive [Kats and Thisse, 1992]:

"a game belongs to this class if a unilateral move by one player which results in an increase in that player's payoff also causes a (weak) decline in the payoffs of all other players. Furthermore, if that move causes no change in the mover's payoff then all other players' payoffs remain unchanged."

Clearly, if a game is strictly competitive, then it is also weakly unilaterally competitive, but the converse is not true in general. Kats and Thisse [1992] showed that if a game is weakly unilaterally competitive, then it has unique PNE payoff. For us, for two-person games, this follows directly from our computer output and Theorem 1.

Condition (10) can be given a similar interpretation:

A two-person game satisfies this condition if a unilateral move by player 1 which results in a (weak) increase in his payoff also causes a (weak) increase in the payoff of player 2, but a unilateral move by player 2 which results in a (weak) increase in his payoff will causes a (weak) decline in the payoff of player 1.

Thus in this class of games, the two players are not equal, and it clearly favors player 2. The game may be competitive for player 1, but not for player 2.

Proposition 2 Given a game that satisfies (10), if player 2's payoff is maximal at (a, b), i.e. (a′ , b′ ) ≤2 (a, b) for all a′ , b′ , then there is a strategy a∗ such that (a∗ , b) is a PNE and (a∗ , b) ≃2 (a, b).

Thus for the class of games that satisfy condition (10), the optimal strategy for player 2 is to do the strategy for which there is a strategy by the other player that will give him the maximum payoff. The following is an example of such games (as usual, player 1 is the row player, and player 2 the column player; the first number in a cell is the payoff of the row player, the second the column player):

It has a unique equilibrium (3, 6).

As we mentioned, condition (11) is symmetric to condition (10), with the roles of the two players swapped. For the classes of games corresponding to the other conditions, (12) - (15), both players can obtain their maximal payoffs.

Proposition 3 Given a game that satisfies one of the conditions (12) - (15), if player 1's (player 2's) payoff at (a, b) maximal, then there is a strategy b∗ (a∗ ) such that (a, b∗ ) ((a∗ , b)) is a PNE where both players receive the maximum payoffs.

Thus, from these two propositions, we see that the classes of games represented by the conditions (10) - (15) are not really "competitive" games. We can then conclude that among the classes of games that can be represented by a conjunction (8) of two binary clauses, the class of weakly unilaterally competitive games is the most general class of "competitive"

and "fair" games that have unique PNE. As we mentioned above, by this we do not mean that other types of games are not interesting. In real life, unfair games like those described by (10) may well arise.

6 Strict games

We now describe our experimental results for strict games. Recall that these are games where for each player, different profiles have different payoffs. Thus uniqueness of PNE payoff simply means uniqueness of PNE in strict games.

6.1 Games with dominant strategies

We first consider conditions that mention only ≤1:

For this class of conditions, our program outputs the following six uniqueness conditions on 2x2 strict games:

By Theorem 2, these are also uniqueness conditions for all strict two-person games. Notice that these conditions do not mention ≤2. This means that if player 1's preference relation satisfies any of the above conditions, then the game has a unique PNE, no matter what the other player's preference relation is.

For instance, the first condition can be written as

For strict games, this is equivalent to

as ¬(x1, y1) ≤1 (x2, y1) iff (x2, y1) <1 (x1, y1). It is not hard to see that the above condition implies the following condition:

meaning that no matter what player 2 does, the best response for player 1 is always the same. For strict games, this means that player 1 has a strictly dominant strategy: a strategy x is a strictly dominant strategy if for all other strategy x′ of player 1, and any strategy y of player 2, (x′ , y) <1 (x, y). As it turned out, this is also the case for the other five conditions above, as the following proposition shows.

Proposition 4 A strict game G = (A,B,≤1,≤2) has a strictly dominant strategy for player 1 if and only if for any preference relation ≤′2 for player 2, the game G′ = (A, B, ≤1, ≤′2 ) has exactly one PNE.

Given this result, there is no need to consider any condition of the form (8) that mentions only one player's preference.

It is interesting to note that for the prisoner's dilemma each player has a strictly dominant strategy, thus should play this strategy. The dilemma is that each player can get a higher payoff by a unilateral move away from his dominant strategy.

6.2 Weakly unilaterally competitive games for individual players

For other conditions of the form (8), our program returns 16 uniqueness conditions for strict games. However, each of them has a symmetric one when the roles of the two players are swapped. Thus there are really only eight such conditions, given below:

In particular, we found that for strict games, a conjunction C1 ∧ C2 of two binary clauses is a uniqueness condition iff either C1 or C2 is a uniqueness condition.

The first condition is equivalent to

as in strict games, s1 ≤1 s2 iff s1 <1 s2 ∨ s1 = s2. This is exactly one of the two conjuncts in the condition (9) for weakly unilaterally competitive games.

Now swap the roles of the two players in (24), we get the following condition

which is exactly the other conjunct in the condition (9).

In the following, we call a game that satisfies (24) a weakly unilaterally competitive for player 1, and a game that satisfies (25) a weakly unilaterally competitive for player 2. Thus a game is weakly unilaterally competitive if it is weakly unilaterally competitive for both players. The following example shows that a game can be weakly unilaterally competitive for player 1 but not for player 2.

This example also shows that a weakly unilaterally competitive game for player 1 may not be almost strictly competitive [Aumann, 1962]: a game is almost strictly competitive if

1. the set of payoff vectors of the PNEs is the same as the set of payoff vectors of the twisted equilibria; and
2. there is a PNE that is also a twisted equilibrium,

where (a, b) is a twisted equilibrium if no player can decrease the payoff of the other player by a unilateral change of his strategy: for every a′ ∈ A (b′ ∈ B), (a, b) ≤2 (a′ , b) ((a, b) ≤1 (a, b′ )). For this example, it is easy to see that the only equilibrium of the game, (4, 3), is not a twisted equilibrium.

As it turns out, (24) and (25) are the only non-trivial conditions. The last two conditions (22) and (23) can never be satisfied by games larger or equal to 3x3. The remaining five conditions (17) - (21) are games with dominant strategies.

Proposition 5 If G is a strict game and satisfies one of the conditions (17) - (21), then one of the players has a strictly dominant strategy in G.

6.3 Strictly competitive game classes

To summarize, for strict games, the only interesting uniqueness conditions that can be expressed by a conjunction of two binary clauses and include games that do not have dominant strategies are weakly unilaterally competitive conditions for individual players, (24) and (25). This led us to wonder if these two conditions are also necessary conditions for a strict game to have a unique PNE. However, it is easy to see that this is not the case. In fact, a universal condition like (8) can never be both a necessary and a sufficient condition for a game to have unique PNE. This is because for any given game, no matter how many PNEs it has, we can always extend it by one more strategy for each player, and make it into a game with a unique PNE by assigning payoffs large enough to a profile made of the two new strategies. However, if a universal condition is satisfied by a game, it is also satisfied by any of its sub-games.

This led us to consider not individual games, but classes of games under certain equivalence relation.

Two games G1 = (A,B,≤1,≤2) and G2 = (A′ , B′ , ≤′1 ,≤′2 ) are unilaterally order equivalent 2 if

• A = A′ , and B = B′ .
• For every a ∈ A, b, b′ ∈ B, (a, b) ≤2 (a, b′ ) iff (a, b) ≤′2 (a, b′ ).
• For every b ∈ B, a, a′ ∈ A, (a, b) ≤1 (a′ , b) iff (a, b) ≤′1 (a′ , b).

They are best-response equivalent [Rosenthal, 1974] if for all a ∈ A, B2(a) in G1 and G2 are the same, and for all b ∈ B, B1(b) in G1 and G2 are the same. Clearly, if G1 and G2 are unilaterally order equivalent, then they are also bestresponse equivalent, but the converse is not true in general. Both notions of equivalence preserve PNEs.

We have the following result.

Theorem 3 A strict game has at most one PNE iff it is bestresponse equivalent to a strictly competitive game.

Theorem 3 does not hold for general two-person games. For instance, the following game

has a unique equilibrium (2, 2) but is not best-response equivalent to any strictly competitive games.

2 We call it unilaterally order equivalence to distinguish it from order equivalence [Rosenthal, 1974] that requires both the row and column orders in the two games to be the same for both players.

7 Concluding remarks

We have provided a logical framework for computer-aided theorem discovery in two-person game theory, and applied it successfully to the task of discovering classes of two-person games with unique PNE payoffs. The general methodology used here is similar to the ones used by Lin [2004] for discovering state invariants in planning, by Lin and chen [2007] for discovering strongly equivalent logic programs and by Tang and Lin [2009] for proving and discovering theorems in social choice theory.

There are many directions for future work. An obvious one is to see how interesting theorems can be discovered using Theorem 1 on classes of games that do not have any PNE and games whose PNEs are Pareto optimal.