pith. sign in

arxiv: 2605.21170 · v1 · pith:OM3DJP2Snew · submitted 2026-05-20 · 🧮 math.LO

Model Comparison Games for Generalized Quantifiers

Antti Kuusisto , Miguel Moreno , Matias Selin This is my paper

Pith reviewed 2026-05-21 01:39 UTC · model grok-4.3

classification 🧮 math.LO
keywords model comparison gamesgeneralized quantifiersEhrenfeucht-Fraïssé gamesformula-size gamesfirst-order logicseparabilityexpressive powerlogical characterization
0
0 comments X

The pith

Two new model comparison games characterize when structures can be separated by first-order formulas with generalized quantifiers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces two games that determine whether two models can be told apart using first-order logic extended by generalized quantifiers. One game adapts the standard Ehrenfeucht-Fraïssé comparison method by adding moves that handle the extra quantifiers. The other is a formula-size game that tracks the resources needed to build distinguishing formulas. These tools matter because they give a direct, playable way to test the limits of what such extended logics can express about structures.

Core claim

The two new model comparison games characterize separability by first-order formulas with generalized quantifiers. One is built on the Ehrenfeucht-Fraïssé game and the other is a formula-size game.

What carries the argument

Two model comparison games whose move rules and winning conditions are defined to match exactly the distinguishing power of first-order formulas with generalized quantifiers.

If this is right

  • The games supply a method to establish inexpressibility results for first-order logic with generalized quantifiers.
  • The Ehrenfeucht-Fraïssé variant extends classical model comparison directly to the richer logic.
  • The formula-size variant links the length of distinguishing formulas to the length of winning strategies in the game.
  • Both games apply to arbitrary structures, not only finite ones.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The games could simplify proofs that certain properties of databases or graphs lie outside the reach of generalized-quantifier queries.
  • They open the possibility of automated tools that search for short distinguishing formulas by playing the formula-size game.
  • The approach may connect to resource-bounded versions of other logical games studied in finite model theory.

Load-bearing premise

The specific move rules and winning conditions of the two games are defined so that they exactly correspond to the distinguishing power of first-order formulas with generalized quantifiers, without missing cases or overcounting.

What would settle it

A pair of models that one game declares indistinguishable yet a generalized-quantifier formula separates them, or vice versa.

Figures

Figures reproduced from arXiv: 2605.21170 by Antti Kuusisto, Matias Selin, Miguel Moreno.

Figure 1
Figure 1. Figure 1: Suppose the quantifier ∃=3, meaning “there exist exactly three”, is in 𝒬, and suppose 𝜏 = {𝑅, 𝐵} where 𝑅 and 𝐵 are both unary. The model A is separated from both B1 and B2 by the formula ∃=3𝑥 (𝐵(𝑥)∨𝑅(𝑥)), where nodes in the interpretation of 𝐵 are coloured in blue and nodes in the interpretation of 𝑅 in red. Player I thus has a winning strategy in the respective EF{𝒬}-games by choosing the witness set 𝑋 an… view at source ↗
read the original abstract

We introduce two new model comparison games that characterize separability by first-order formulas with generalized quantifiers. One is built on the Ehrenfeucht-Fra\"iss\'e game and the other is a formula-size game.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces two new model comparison games for first-order logic extended with generalized quantifiers: an Ehrenfeucht-Fraïssé-style game and a formula-size game. It defines the move rules and winning conditions for each game and proves that they characterize separability of structures by formulas in this logic, i.e., Duplicator has a winning strategy in the game on a pair of structures if and only if no formula of the logic distinguishes them.

Significance. If the claimed equivalences hold, the results extend the classical Ehrenfeucht-Fraïssé theorem to logics with generalized quantifiers, supplying concrete tools for proving inexpressibility and analyzing expressive power. The dual presentation of an EF-style game together with a formula-size game is a strength, as the two formats often support different proof strategies. The manuscript supplies explicit definitions and equivalence proofs that appear internally consistent with no evident gaps, hidden parameters, or reduction to prior self-citations.

minor comments (2)
  1. [Abstract] The abstract states the main claim but supplies no indication of the game definitions or the structure of the equivalence proofs; a slightly expanded abstract would allow readers to assess the contribution more rapidly.
  2. [Game definitions] In the game definitions (presumably §3), the precise interaction between the generalized-quantifier moves and the standard quantifier moves could be illustrated with one concrete example using a familiar generalized quantifier such as 'most' or 'there exist infinitely many'.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and significance assessment of our work on model comparison games characterizing separability in first-order logic with generalized quantifiers. The recommendation for minor revision is noted, but no specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained via explicit definitions and proofs

full rationale

The paper defines two new model comparison games (an EF-style game and a formula-size game) with explicit move rules and winning conditions tailored to first-order logic extended by generalized quantifiers. It then proves that these games characterize separability exactly as the logic does. This is a standard constructive equivalence result in model theory: the definitions are chosen to match the semantics, and the proofs verify the correspondence in both directions without reducing to self-citations, fitted parameters, or imported uniqueness theorems. No load-bearing step collapses by construction to prior inputs or author-overlapping citations; the central contribution is the game definitions themselves plus the verification, which stands independently.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities are mentioned in the abstract. The claim rests on the existence and correctness of the game definitions and their equivalence proofs.

pith-pipeline@v0.9.0 · 5544 in / 1032 out tokens · 33831 ms · 2026-05-21T01:39:23.598222+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages · 1 internal anchor

  1. [1]

    Springer Science & Business Media, 2005

    Heinz-Dieter Ebbinghaus and J¨ org Flum.Finite Model Theory. Springer Science & Business Media, 2005. 1, 2

    work page 2005

  2. [2]

    An extension of the Ehrenfeucht-Fra¨ ıss´ e game for first order logics augmented with Lindstr¨ om quantifiers

    Simi Haber and Saharon Shelah. An extension of the Ehrenfeucht-Fra¨ ıss´ e game for first order logics augmented with Lindstr¨ om quantifiers. InFields of logic and computation. II, volume 9300 ofLecture Notes in Comput. Sci., pages 226–236. Springer, Cham, 2015. 1

    work page 2015

  3. [3]

    The size of a formula as a measure of complexity

    Lauri Hella and Jouko V¨ a¨ an¨ anen. The size of a formula as a measure of complexity. InLogic without Borders: Essays on Set Theory, Model Theory, 15 Philosophical Logic and Philosophy of Mathematics, pages 193–214. Walter De Gruyter, 2015. 1, 9

    work page 2015

  4. [4]

    Graph Learning via Logic-Based Weisfeiler- Leman Variants and Tabularization.arXiv preprint arXiv:2508.10651, 2025

    Reijo Jaakkola, Tomi Janhunen, Antti Kuusisto, Magdalena Ortiz, Matias Selin, and Mantas ˇSimkus. Graph Learning via Logic-Based Weisfeiler- Leman Variants and Tabularization.arXiv preprint arXiv:2508.10651, 2025. 2

    work page internal anchor Pith review arXiv 2025

  5. [5]

    Kolaitis and Jouko A

    Phokion G. Kolaitis and Jouko A. V¨ a¨ an¨ anen. Generalized quantifiers and pebble games on finite structures.Ann. Pure Appl. Logic, 74(1):23–75, 1995. 1

    work page 1995

  6. [6]

    Some Turing-Complete Extensions of First-Order Logic

    Antti Kuusisto. Some Turing-Complete Extensions of First-Order Logic. In Adriano Peron and Carla Piazza, editors,Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, Gan- dALF 2014, Verona, Italy, September 10-12, 2014, volume 161 ofEPTCS, pages 4–17, 2014.doi:10.4204/EPTCS.161.4. 2

    work page doi:10.4204/eptcs.161.4 2014

  7. [7]

    A double team semantics for generalized quantifiers.Journal of Logic, Language and Information, 24(2):149–191, 2015

    Antti Kuusisto. A double team semantics for generalized quantifiers.Journal of Logic, Language and Information, 24(2):149–191, 2015. 2

    work page 2015

  8. [8]

    First order predicate logic with generalized quantifiers.Theo- ria, 32(3), 1966

    Per Lindstr¨ om. First order predicate logic with generalized quantifiers.Theo- ria, 32(3), 1966. 1, 2 16 A Quantifiers of Arbitrary Width and Type In this section, we consider generalized quantifiers of arbitrary, finite width and type, which can quantify multiple formulas that bind multiple variables. Now that we deal with tuples of variables, we might ...

    work page 1966

  9. [9]

    Suppose it has width𝑘∈Z + and typen∈Z 𝑘 +

    The attacker chooses a quantifier𝑄∈ 𝒬. Suppose it has width𝑘∈Z + and typen∈Z 𝑘 +. The attacker also chooses𝑘tuples of variable symbols x1, . . . ,x𝑘, wherex 𝑗 ∈VAR n(𝑗) for each 1≤𝑗≤𝑘

    work page

  10. [10]

    , 𝑋𝑘 from the domain of either model (without loss of generality, suppose they are chosen from𝑀), where each𝑋 𝑗 ⊆𝑀 n(𝑗) respectsx 𝑗-repetitions, such that (𝑀, 𝑋 1,

    The attacker chooses𝑘witness sets𝑋 1, . . . , 𝑋𝑘 from the domain of either model (without loss of generality, suppose they are chosen from𝑀), where each𝑋 𝑗 ⊆𝑀 n(𝑗) respectsx 𝑗-repetitions, such that (𝑀, 𝑋 1, . . . , 𝑋𝑘)∈𝑄. The attacker also chooses𝑘spillover sets𝑃 1, . . . , 𝑃𝑘, where each𝑃 𝑗 ⊆ 𝑁 n(𝑗) respectsx 𝑗-repetitions

    work page

  11. [11]

    , 𝑋′ 𝑘, where each 𝑋 ′ 𝑗 ⊆𝑁 n(𝑗) respectsx 𝑗-repetitions, such that (𝑁, 𝑋 ′ 1,

    The defender chooses corresponding witness sets𝑋 ′ 1, . . . , 𝑋′ 𝑘, where each 𝑋 ′ 𝑗 ⊆𝑁 n(𝑗) respectsx 𝑗-repetitions, such that (𝑁, 𝑋 ′ 1, . . . , 𝑋′ 𝑘)∈𝑄and 𝑃𝑗 ⊆𝑋 ′ 𝑗 for all 1≤𝑗≤𝑘

    work page

  12. [12]

    , 𝑘}and one of the following: (a) Chooses aw ′ ∈𝑁 n(𝑗) ∖𝑋 ′ 𝑗 that respectsx 𝑗-repetitions andw∈𝑋 𝑗

    The attacker chooses𝑗∈ {1, . . . , 𝑘}and one of the following: (a) Chooses aw ′ ∈𝑁 n(𝑗) ∖𝑋 ′ 𝑗 that respectsx 𝑗-repetitions andw∈𝑋 𝑗. The players swap roles. The next position is (M,N, ℎ w x𝑗 , ℎ′ w′ x𝑗 ). (b) Choosesw ′ ∈𝑋 ′ 𝑗. The defender now either: •choosesw∈𝑋 𝑗, after which the next position is (M,N, ℎw x𝑗 , ℎ′ w′ x𝑗 ), or •choosesw∈𝑃 𝑗, after which...

    work page

  13. [13]

    If the pair (ℎ *, ℎ′ *) does not induce a partial isomorphism betweenM ′ andN ′, then the game ends and the attacker wins

    Let (M ′,N ′, ℎ*, ℎ′ *) be the position determined in the previous step. If the pair (ℎ *, ℎ′ *) does not induce a partial isomorphism betweenM ′ andN ′, then the game ends and the attacker wins. Otherwise a new round begins from this position. At any point during steps 2–3, immediately after a set is chosen, the opposing player maycontestthat choice inst...

    work page

  14. [14]

    If there is an atomic FO(𝒬)-formula𝜙that separates𝒜 𝑖 andℬ 𝑖, then the game ends and PlayerIwins

    work page

  15. [15]

    Otherwise, if𝑠 𝑖 = 1, then the game ends and PlayerIIwins

    work page

  16. [16]

    (b)Right splitting move (conjunction).PlayerIchooses𝑢, 𝑣∈Z + such that𝑢+𝑣=𝑠 𝑖, and chooses (possibly overlapping) sets𝒞,𝒟 ⊆ ℬ 𝑖 such that𝒞 ∪ 𝒟=ℬ 𝑖

    If neither of the above conditions holds, then PlayerIchooses one of the following three options: (a)Swap classes (negation).A new round begins from the position (𝑠𝑖 −1,ℬ 𝑖,𝒜 𝑖). (b)Right splitting move (conjunction).PlayerIchooses𝑢, 𝑣∈Z + such that𝑢+𝑣=𝑠 𝑖, and chooses (possibly overlapping) sets𝒞,𝒟 ⊆ ℬ 𝑖 such that𝒞 ∪ 𝒟=ℬ 𝑖. PlayerIIthen responds by choos...

    work page