🔢 mathematics

A New Ehrenfeucht-Fraïssé Game for Dependence Logic

This paper introduces a new Ehrenfeucht-Fraïssé game for dependence logic that utilizes single-element moves and independence declarations to characterize elementary equivalence, thereby overcoming the complexity of previous team-based formulations.

Original authors: Joni Puljujärvi, Jouko Väänänen

Published 2026-06-02

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Joni Puljujärvi, Jouko Väänänen

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Big Picture: Comparing Two Worlds

Imagine you have two different worlds (let's call them World A and World B). These worlds are made of objects and rules. In the world of logic, we want to know: Are these two worlds essentially the same?

Specifically, we are looking at a special kind of logic called Dependence Logic. In this logic, we care about "dependence." For example, in World A, maybe the color of a house is completely determined by its address (if two houses have the same address, they must have the same color). In World B, maybe the color is random, even if the addresses match.

The paper introduces a new game to test if World A and World B are indistinguishable regarding these rules of dependence.

The Old Way: The "Team" Game (Too Complicated)

Previously, there was a game used to compare these worlds, but it was very heavy and complicated.

The Players: Two players, Player I (the challenger) and Player II (the defender).
The Moves: In the old game, Player I didn't just pick one object; they had to pick a whole team (a massive list) of objects at once.
The Problem: Imagine trying to compare two cities by picking out a whole neighborhood of houses in one move. It's messy, hard to track, and computationally heavy. It felt like a "second-order" game (dealing with groups) rather than a simple "first-order" game (dealing with individuals).

The New Way: The "Single Element" Game

The authors, Joni Puljujärvi and Jouko Väänänen, created a new, lighter game that works more like the classic games we use for simple logic.

The Setup:
Instead of picking whole teams, the players now pick single elements (one house, one person, one number) at a time, just like in a standard board game.

The Twist: The "Commitment Card"
Here is the unique feature of this new game. When Player I picks an element, they can also play a Commitment Card.

The Card says: "I am picking this new element based only on the previous moves I made in this specific sequence. I am ignoring everything else."
The Meaning: This is a promise of independence. Player I is saying, "My choice here is determined only by these specific past choices, not by any other hidden factors."

How the Game Plays Out:

Player I picks an item in World A (or B) and plays a card declaring which past moves determined this choice.
Player II must respond by picking an item in the other world.
The Goal: Player II wins if they can keep matching Player I's moves perfectly, while respecting the commitments.

The "Uniform Winning Strategy"
This is the most important concept. Player II doesn't just need to win one single game. They need a Uniform Winning Strategy.

Imagine Player II is a robot programmed with a strategy.
If Player I plays the game twice, making the exact same commitments (saying "I chose this based on move #1 and #3" both times), Player II's robot must produce the exact same response both times.
If Player II can do this consistently across many different scenarios, it proves that World A and World B share the exact same rules of dependence.

The "Coloring" Example (From the Paper)

The paper uses a graph coloring example to explain why this matters.

World A is a map that can be colored with only 2 colors (Red and Blue) so that no touching houses share a color.
World B is a map that cannot be colored with 2 colors.

In the old game, you might try to pick a whole coloring scheme at once. In the new game:

Player I picks a house in World B and says, "I'm picking this house based only on the fact that it's the first one."
Player II picks a house in World A.
Player I picks another house in World B and says, "I'm picking this one based only on the first house."
If Player II is forced to pick a color for the second house in World A that matches the logic of World B, they will eventually get stuck. Because World B has no valid 2-coloring, Player II cannot make a consistent "commitment" that works for all scenarios.

The paper proves that if Player II has a uniform winning strategy, then World A and World B are logically identical regarding dependence. If Player I can force a win, the worlds are different.

Why This Matters

Simplicity: It replaces the messy "team" moves with simple "single element" moves, making the game much easier to understand and use.
Precision: It captures the exact same power as the old, complicated game. It proves that you don't need to look at massive groups to understand dependence; you just need to look at how single choices relate to each other.
The "First-Order" Feel: It brings the logic of dependence down to the same level as standard logic, where we compare individual items rather than complex sets.

Summary

Think of this paper as inventing a new, simpler way to play "Spot the Difference" between two complex worlds. Instead of comparing entire neighborhoods at once, you compare house by house. But you add a special rule: you must declare which past houses influenced your current choice. If the defender can always match the challenger's moves while respecting these declarations, the two worlds are fundamentally the same. If they can't, the worlds are different.

Technical Summary: A New Ehrenfeucht–Fraïssé Game for Dependence Logic

Problem Statement
Dependence logic ( $D$ ) extends first-order logic by adding dependence atoms $=(\vec{x}, y)$ , which assert that the value of $y$ is functionally determined by the values of $\vec{x}$ . The semantics of $D$ are typically defined via team semantics, where formulas are evaluated over sets of assignments (teams) rather than single assignments. Consequently, previous attempts to define an Ehrenfeucht–Fraïssé (EF) game for dependence logic, such as the one in [15], relied on "second-order" moves where players select entire teams or sets of assignments. The authors argue that because teams can be massive, these moves are computationally and conceptually complicated. The paper seeks to define a "first-order" EF game for dependence logic where moves consist of single elements, analogous to the classical EF game for first-order logic, while still capturing the expressive power of dependence logic.

Methodology
The authors introduce a new game, denoted $EF^{dep}_n(A, B)$ , played between two structures $A$ and $B$ . The methodology involves three primary components:

The Game Mechanics:
The game proceeds for $n$ rounds. In each round $k$ , Player I (the spoiler) selects an element $x_k$ from either $A$ or $B$ . Crucially, Player I must also declare a set of "dependence commitments" $W_k \subseteq \mathcal{P}(n)$ and sets of atomic formulas $U^+_k, U^-_k$ .
- If a set of indices $\{i_0, \dots, i_{k-1}\} \in W_k$ , Player I declares that the current move $x_k$ is determined solely by the previous moves made in the same model (i.e., $x_k$ depends only on $\{x_{i_0}, \dots, x_{i_{k-1}}\}$ if $x_k \in A$ , or the corresponding elements in $B$ ).
- Player II (the duplicator) responds with an element $y_k$ from the opposite structure.
- The winning condition for Player II in a single play is not based on the commitments; rather, the commitments are only evaluated when considering multiple plays simultaneously.
Uniform Winning Strategies:
The core innovation is the definition of a uniform winning strategy for Player II. A strategy is uniformly winning if, whenever Player I plays consistently (i.e., makes the same commitments and satisfies the same atomic formulas across multiple plays), Player II's responses respect the declared dependencies. Specifically, if Player I's moves in two different plays are identical on the indices declared in $W_k$ , Player II's responses must also be identical. This mechanism allows the game to capture the functional nature of dependence atoms without requiring players to select entire teams.
Auxiliary Game and Equivalence:
To prove the characterization result, the authors introduce an auxiliary game, $EFD_n((A, X), (B, Y))$ , based on indexed teams. This game is a modification of the game in [15] but uses supplement functions (which define how teams are expanded) as moves rather than teams themselves. The authors establish a bridge between the two games:
- They show that if Player II has a winning strategy in the auxiliary game $EFD_n$ , she possesses a uniform winning strategy in the new game $EF^{dep}_n$ .
- They prove that the existence of a uniform winning strategy in $EF^{dep}_n(A, B)$ is equivalent to the preservation of truth from $A$ to $B$ for all dependence logic sentences of quantifier rank $\le n$ .

Key Contributions and Results

Definition of $EF^{dep}_n(A, B)$ : The paper defines a novel EF game where moves are single elements, not teams. This resolves the complexity of "second-order" moves found in previous formulations.
Uniformity Condition: The paper introduces the concept of a "uniform winning strategy," which enforces that Player II's responses must respect the functional dependencies declared by Player I across multiple plays.
Characterization Theorem: The main result (Theorem 6.1) establishes that for any two structures $A$ and $B$ , Player II has a uniform winning strategy in $EF^{dep}_n(A, B)$ for all $n$ if and only if $A$ and $B$ are elementarily equivalent in dependence logic ( $A \equiv_D B$ ).
Reduction to First-Order Moves: The authors demonstrate that despite the "second-order" nature of dependence logic semantics, the game can be played with first-order moves, provided the strategy satisfies the uniformity condition.

Significance and Claims
The paper claims to provide a "first-order" characterization of elementary equivalence in dependence logic, mirroring the classical result for first-order logic. The significance lies in simplifying the game-theoretic analysis of dependence logic by avoiding the manipulation of large teams during gameplay.

The authors are modest regarding the scope of their results. They note that:

The proof of the main result relies on a specific normal form for dependence logic sentences (Theorem 2.5), which they acknowledge is somewhat unsatisfactory as it disconnects the game length directly from the quantifier rank of arbitrary formulas.
The results rely heavily on the downward closedness of dependence logic (Fact 2.3). Consequently, the authors state that these results cannot be immediately lifted to other team logics that lack this property, such as inclusion logic or independence logic.
Future work is suggested to explore whether similar games can be constructed for inclusion logic and independence logic, and to investigate whether the game length can be more tightly connected to the quantifier rank without relying on normal forms.

The paper does not propose new applications or experimental proposals but focuses strictly on the theoretical characterization of dependence logic via game semantics.