Solution (source code)

= Solution

The definition in this part uses a single <Boolean valuation>, so the relevant <Nash equilibria> are <pure strategy> equilibria of a <Boolean game>. Use its standard convention that the players' control sets form a <set partition> of the variables.

Membership follows from an existential choice of a <strategy profile> and a universal check of all <unilateral deviations>. Assign <payoff> one to satisfying a player's goal and zero otherwise. A <strategy profile> $\sigma$ is a <Nash equilibrium> precisely when, for every player $i$ and every alternative <Boolean valuation> $\tau_i$ of that player's variables,
$$
\gamma_i(\sigma)\ \lor\ \neg\gamma_i(\tau_i,\sigma_{-i})
$$
is true: either the goal is already satisfied or no deviation can satisfy it. Thus the requested property is
$$
\exists\sigma\ \forall(i,\tau_i)\quad
\left[
\phi(\sigma)\land
\bigl(\gamma_i(\sigma)\lor
\neg\gamma_i(\tau_i,\sigma_{-i})\bigr)
\right].
$$
The strings encoding $\sigma$, $i$ and $\tau_i$ have polynomial length, and evaluating the bracketed <propositional formulas> takes <polynomial time>. Invalid encodings of a player index can simply be ignored by the test. This is the existential <second level of the polynomial hierarchy>, $\Sigma_2^{\mathrm P}$.

For hardness, reduce the canonical complete problem of deciding a <two-block quantified Boolean formula>
$$
\exists X\ \forall Y\ \psi(X,Y).
$$
Make a two-player <Boolean game>: player 1 controls $X$ and has goal $\gamma_1=\top$; player 2 controls $Y$ and has goal $\gamma_2=\neg\psi$. Set the query formula to $\phi=\psi$. The construction has size linear in the input formula.

If an assignment $x$ satisfies $\forall Y\,\psi(x,Y)$, combine it with any assignment $y$. Player 1 already satisfies its goal, and player 2 cannot satisfy $\neg\psi$ by any <unilateral deviation>. Thus $(x,y)$ is a <Nash equilibrium> satisfying the query.

Conversely, let $(x,y)$ be a <Nash equilibrium> satisfying $\psi$. Player 2 currently has <payoff> zero. If some alternative $y'$ made $\psi(x,y')$ false, that deviation would satisfy player 2's goal and increase its <payoff> to one. The <Nash equilibrium> condition therefore implies $\forall Y\,\psi(x,Y)$. This proves the required equivalence and the <polynomial-time reduction>.

Together, membership and hardness prove \b[$\Sigma_2^{\mathrm P}$-completeness] of <existential equilibrium checking in a Boolean game>. The reduction works with only two players and one constant goal.