pith. sign in

arxiv: 2606.25276 · v1 · pith:DOKXNFEVnew · submitted 2026-06-24 · 💻 cs.GT

Decidability and Undecidability Results for LIA-Definable Impartial Combinatorial Games

Shiguang Feng , Liangda Fang , Jiahao Luo , Quanlong Guan This is my paper

Pith reviewed 2026-06-25 20:50 UTC · model grok-4.3

classification 💻 cs.GT
keywords impartial combinatorial gamesLIA-definable gamesdecidabilityundecidabilitycombinatorial game theorylinear integer arithmeticwinning positionstermination
0
0 comments X

The pith

Deciding termination and winning states for LIA-definable impartial combinatorial games is undecidable in general.

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

The paper establishes that several decision problems for impartial combinatorial games whose rules are expressed in linear integer arithmetic are undecidable. These include determining if a game terminates or contains cycles, verifying if an LIA formula exactly describes its winning or losing positions, and checking the status of an individual state. The same problems become decidable once termination is assumed, and state-level winning/losing questions further become decidable when the game also has finite depth. This matters because many concrete combinatorial games fit the LIA-definable class, so the results mark the boundary between what can and cannot be automatically determined about their behavior.

Core claim

Deciding whether an LIA-definable ICG is terminating or cyclic is undecidable in general, while the corresponding questions become decidable for terminating LIA-definable ICGs. Deciding whether an LIA formula exactly characterizes the set of winning, losing, or draw states is undecidable in general and decidable for terminating LIA-definable ICGs. Deciding whether a state is winning or losing remains undecidable even for terminating LIA-definable ICGs, but becomes decidable for terminating finite-depth LIA-definable ICGs. Deciding whether a state is a draw is undecidable in general and decidable for terminating LIA-definable ICGs.

What carries the argument

LIA-definable impartial combinatorial games, with the argument carried by reductions from undecidable problems in linear integer arithmetic to the corresponding game decision problems.

If this is right

  • No general algorithm exists to determine whether an LIA-definable ICG terminates or is cyclic.
  • No algorithm exists to check whether a given LIA formula exactly captures the winning, losing, or draw states of an LIA-definable ICG.
  • Even when termination is guaranteed, no algorithm decides whether a given state is winning or losing.
  • When a game is both terminating and of finite depth, algorithms exist for deciding whether a state is winning or losing.

Where Pith is reading between the lines

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

  • The results indicate that additional syntactic restrictions on game definitions, such as explicit depth bounds, are needed before automated verification becomes feasible.
  • Similar undecidability patterns are likely to appear in other classes of games whose move relations can encode arithmetic.
  • Practical tools for analyzing concrete LIA games will need to incorporate termination checks or depth bounds as preprocessing steps.

Load-bearing premise

The reductions from undecidable linear integer arithmetic problems to the game questions preserve the LIA-definable structure of the games.

What would settle it

An algorithm that correctly decides termination for arbitrary LIA-definable ICGs would yield a decision procedure for a known undecidable fragment of linear integer arithmetic.

read the original abstract

Combinatorial game theory is a branch of mathematics and theoretical computer science that studies deterministic games with perfect information and no elements of chance. The majority of combinatorial games are impartial and formalized in linear integer arithmetic, which we call LIA-definable impartial combinatorial games (ICGs). This paper studies decidability and undecidability questions for these games. We prove that deciding whether an LIA-definable ICG is terminating or cyclic is undecidable in general, while the corresponding questions become decidable for terminating LIA-definable ICGs. We also show that deciding whether an LIA formula exactly characterizes the set of winning, losing, or draw states of an LIA-definable ICG is undecidable in general and decidable for terminating LIA-definable ICGs. For state-level questions, deciding whether a state is winning or losing remains undecidable even for terminating LIA-definable ICGs, but becomes decidable for terminating finite-depth LIA-definable ICGs. Finally, deciding whether a state is draw for an LIA-definable ICG is undecidable in general and decidable for terminating LIA-definable ICGs.

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

1 major / 0 minor

Summary. The paper claims that for LIA-definable impartial combinatorial games, deciding termination or cyclicity is undecidable in general but decidable for terminating games; deciding if an LIA formula characterizes the win/lose/draw sets is undecidable in general and decidable for terminating games; deciding if a state is winning or losing is undecidable for terminating games but decidable for terminating finite-depth games; and deciding if a state is a draw is undecidable in general but decidable for terminating games.

Significance. These results are significant as they map out the decidability landscape for key properties of LIA-definable ICGs, offering both undecidability proofs via reductions and decidability results for restricted classes. This helps in understanding the computational boundaries in combinatorial game theory when using linear integer arithmetic for definitions. The distinction between general, terminating, and finite-depth cases is particularly useful.

major comments (1)
  1. The undecidability results are based on reductions from undecidable LIA problems. The manuscript must ensure and demonstrate that the move relations in the constructed games are LIA-definable. The skeptic's concern about whether the reduction preserves the LIA structure is load-bearing; if not addressed explicitly, the negative results may not hold for the intended class.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading, positive evaluation of the significance of the results, and the constructive major comment. We address the point below and will revise the manuscript to strengthen the presentation of the reductions.

read point-by-point responses

  1. Referee: The undecidability results are based on reductions from undecidable LIA problems. The manuscript must ensure and demonstrate that the move relations in the constructed games are LIA-definable. The skeptic's concern about whether the reduction preserves the LIA structure is load-bearing; if not addressed explicitly, the negative results may not hold for the intended class.

    Authors: We agree that the LIA-definability of the constructed move relations must be shown explicitly for the reductions to be valid. In the proofs (e.g., Theorems 3.1 and 4.3), each game is constructed so that positions are tuples of integers and the move relation is defined directly by a quantifier-free LIA formula obtained from the source undecidable LIA instance (such as an encoding of the halting problem or Diophantine equation). The formula is exhibited in the proof text. Nevertheless, to remove any ambiguity for a skeptical reader, we will add a dedicated paragraph immediately after each main construction that isolates the LIA formula for the move relation and verifies it is indeed in LIA. This revision will be made in the next version. revision: yes

Circularity Check

0 steps flagged

No circularity; undecidability via external reductions from LIA.

full rationale

The paper derives its undecidability results for LIA-definable ICGs by reduction from known undecidable problems in linear integer arithmetic. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear in the abstract or described claims. The central results rest on external arithmetic facts rather than internal redefinitions or ansatzes. This is the standard case of a self-contained theoretical paper whose derivation chain does not collapse to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard results from logic (decidability of LIA fragments, undecidability of full LIA) and combinatorial game theory; no free parameters or invented entities are introduced.

axioms (2)
  • standard math Linear integer arithmetic (LIA) is a decidable theory for certain fragments but undecidable in full generality.
    Used as the base for encoding games and for the undecidability reductions.
  • domain assumption Impartial combinatorial games can be faithfully encoded as LIA formulas describing moves and positions.
    Central modeling choice that allows the decision problems to be stated in LIA.

pith-pipeline@v0.9.1-grok · 5758 in / 1368 out tokens · 21831 ms · 2026-06-25T20:50:32.024540+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

271 extracted references

  1. [1]

    1966 , volume =

    Seymour Ginsburg and Edwin Spanier , journal =. 1966 , volume =

    1966

  2. [2]

    Mathematical Systems Theory , year =

    On the base-dependence of sets of numbers recognizable by finite automata , author =. Mathematical Systems Theory , year =

  3. [3]

    Mojz\. \". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves , year =

  4. [4]

    Mathematisch-Physikalische Semesterberichte (G\"

    Hans Hermes , title =. Mathematisch-Physikalische Semesterberichte (G\". 1954 , volume =

    1954

  5. [5]

    Doklady Akademii Nauk SSSR , year =

    Andrey Petrovich Ershov , title =. Doklady Akademii Nauk SSSR , year =

  6. [6]

    Graphschemata und rekursive Funktionen , journal =

    R\'. Graphschemata und rekursive Funktionen , journal =. 1958 , volume =

    1958

  7. [7]

    Canadian Mathematical Bulletin , year =

    Joachim Lambek , title =. Canadian Mathematical Bulletin , year =

  8. [8]

    Minsky , title =

    Marvin L. Minsky , title =. Annals of Mathematics , publisher =

  9. [9]

    Marvin Minsky , title =

  10. [10]

    Nigel John Cutland , title =

  11. [11]

    Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD-2022) , series =

    Andrej Dudenhefner , title =. Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction (FSCD-2022) , series =

    2022

  12. [12]

    Proceedings of the 4th International Workshop on Reachability Problems (RP-2010) , series =

    Philippe Schnoebelen , title =. Proceedings of the 4th International Workshop on Reachability Problems (RP-2010) , series =. 2010 , doi =

    2010

  13. [13]

    Journal of Computer and System Sciences , volume =

    Christopher Hampson , title =. Journal of Computer and System Sciences , volume =. 2021 , doi =

    2021

  14. [14]

    Complex Systems , pages =

    Matthew Cook , title =. Complex Systems , pages =

  15. [15]

    2019 , pages =

    Haniel Barbosa and Andrew Reynolds and Daniel Larraz and Cesare Tinelli , booktitle =. 2019 , pages =

    2019

  16. [16]

    2021 , organization=

    Rutuja Laxmikant Kolhe and Anuya Joshi and Prachi Vikas Mate and Deeksha Satyendra Gupta and Dipti Patil , booktitle =. 2021 , organization=

    2021

  17. [17]

    Wenjun Ma and Xudong Luo and Weiru Liu , booktitle=

  18. [18]

    Kimberly Ferguson-Walter and Sunny Fugate and Justin Mauger and Maxine Major , booktitle=

  19. [19]

    Proceedings of the Eighth International Conference on Human-Agent Interaction (HAI-2020) , pages=

    Martial Razakatiana and Christophe Kolski and Ren. Proceedings of the Eighth International Conference on Human-Agent Interaction (HAI-2020) , pages=

    2020

  20. [20]

    Integers: Electronic Journal of Combinatorial Number Theory , volume =

    Furman Smith and Pantelimon St. Integers: Electronic Journal of Combinatorial Number Theory , volume =

  21. [21]

    Vladimir Gurvich , journal =

  22. [22]

    Schaefer , title =

    Thomas J. Schaefer , title =. Journal of Computer and System Sciences , volume =

  23. [23]

    Fraenkel and Elisheva Goldschmidt , title =

    Aviezri S. Fraenkel and Elisheva Goldschmidt , title =. Journal of Combinatorial Theory, Series A , volume =

  24. [24]

    Journal of Combinatorial Theory, Series A , volume =

    Urban Larsson , title =. Journal of Combinatorial Theory, Series A , volume =

  25. [25]

    Nhan Bao Ho , journal =

  26. [26]

    2015 , publisher =

    Wenan Liu and Meile Zhao , journal =. 2015 , publisher =

    2015

  27. [27]

    Eric Sopena , journal =

  28. [28]

    2016 , publisher =

    Nhan Bao Ho , journal =. 2016 , publisher =

    2016

  29. [29]

    2018 , publisher=

    Vladimir Gurvich and Nhan Bao Ho , journal=. 2018 , publisher=

    2018

  30. [30]

    2019 , publisher=

    Patricia Bouyer , booktitle=. 2019 , publisher=

    2019

  31. [31]

    2018 , publisher=

    Lu-Xing Yang and Pengdeng Li and Yushu Zhang and Xiaofan Yang and Yong Xiang and Wanlei Zhou , journal=. 2018 , publisher=

    2018

  32. [32]

    Armando Solar-Lezama and Liviu Tancau and Rastislav Bodik and Sanjit Seshia and Vijay Saraswat , booktitle=

  33. [33]

    Proceedings of the Fourteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2008) , series =

    Leonardo De Moura and Nikolaj Bj. Proceedings of the Fourteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2008) , series =

    2008

  34. [34]

    Proceedings of the Ninth ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI-2005) , pages=

    Armando Solar-Lezama and Rodric Rabbah and Rastislav Bod. Proceedings of the Ninth ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI-2005) , pages=

    2005

  35. [35]

    2018 , publisher =

    Evidential Supplier Selection Based on DEMATEL and Game Theory , journal =. 2018 , publisher =

    2018

  36. [36]

    International Journal on Interactive Design and Manufacturing , volume =

    Roberto Hern. International Journal on Interactive Design and Manufacturing , volume =. 2018 , publisher =

    2018

  37. [37]

    Brit CA Milvang-Jensen , year =

  38. [38]

    Aviezri Fraenkel , journal =

  39. [39]

    Issah Musah and Douglas Kwasi Boah and Baba Seidu , journal =

  40. [40]

    Stewart , title =

    David Gale and Frank M. Stewart , title =. Contributions to the Theory of Games , volume =

  41. [41]

    Proceedings of the Fifth International Federation of Automatic Control Conference on System Structure and Control (SSC-1998) , pages =

    Eugene Asarin and Oded Maler and Amir Pnueli and Joseph Sifakis , title =. Proceedings of the Fifth International Federation of Automatic Control Conference on System Structure and Control (SSC-1998) , pages =

    1998

  42. [42]

    Proceedings of the Twenty-ninth International Colloquium on Automata, Languages and Programming (ICALP-2002) , series =

    Thierry Cachat , title =. Proceedings of the Twenty-ninth International Colloquium on Automata, Languages and Programming (ICALP-2002) , series =

    2002

  43. [43]

    Electronic Notes in Theoretical Computer Science , volume =

    Thierry Cachat , title =. Electronic Notes in Theoretical Computer Science , volume =. 2003 , publisher=

    2003

  44. [44]

    Journal of Computer and System Sciences , volume =

    Roderick Bloem and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Yaniv Sa'ar , title =. Journal of Computer and System Sciences , volume =

  45. [45]

    Advances in Applied Mathematics , volume =

    Doron Zeilberger , title =. Advances in Applied Mathematics , volume =

  46. [46]

    Proceedings of the Third International Planning Competition Conference (IPC-2002) , pages =

    Maria Fox and Derek Long , title =. Proceedings of the Third International Planning Competition Conference (IPC-2002) , pages =

    2002

  47. [47]

    Journal of Artificial Intelligence Research , volume =

    Maria Fox and Derek Long , title =. Journal of Artificial Intelligence Research , volume =

  48. [48]

    Jendrik Seipp and Malte Helmert , booktitle=

  49. [49]

    Guillem Frances and Blai Bonet and Hector Geffner , booktitle=

  50. [50]

    Journal of Artificial Intelligence Research , volume =

    Javier Segovia-Aguas and Sergio Jim. Journal of Artificial Intelligence Research , volume =

  51. [51]

    Journal of Philosophical Logic , volume =

    Dongmo Zhang and Michael Thielscher , title =. Journal of Philosophical Logic , volume =

  52. [52]

    Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli , title =

    Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli , title =. Proceedings of the Twenety-Third International Conference on Computer Aided Verification (CAV-2011) , pages =

    2011

  53. [53]

    Proceedings of the Nineteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2013) , pages =

    Alessandro Cimatti and Alberto Griggio and Bastiaan Joost Schaafsma and Roberto Sebastiani , title =. Proceedings of the Nineteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2013) , pages =

    2013

  54. [54]

    Proceedings of the Twenty-sixth International Conference on Computer Aided Verification (CAV-2014) , pages =

    Bruno Dutertre , title =. Proceedings of the Twenty-sixth International Conference on Computer Aided Verification (CAV-2014) , pages =

    2014

  55. [55]

    Allen Emerson and Charanjit Jutla , title =

    E. Allen Emerson and Charanjit Jutla , title =. Proceedings of the Thirty-second Annual Symposium of Foundations of Computer Science (FOCS-1991) , pages =

    1991

  56. [56]

    Michael Albert and Richard Nowakowski and David Wolfe , year =

  57. [57]

    Raymond Reiter , year =

  58. [58]

    Nowakowski , year =

    Richard J. Nowakowski , year =

  59. [59]

    Guy , journal =

    Richard K. Guy , journal =

  60. [60]

    Proceedings of the Sixteenth ACM SIGPLAN-SIGACT Symposium Conference on Principles of Programming Languages (POPL-1989) , year =

    Amir Pnueli and Roni Rosner , title =. Proceedings of the Sixteenth ACM SIGPLAN-SIGACT Symposium Conference on Principles of Programming Languages (POPL-1989) , year =

    1989

  61. [61]

    Proceedings of the Twelfth Annual Symposium Conference on Theoretical Aspects of Computer Science (STACS-1995) , year =

    Wolfgang Thomas , title =. Proceedings of the Twelfth Annual Symposium Conference on Theoretical Aspects of Computer Science (STACS-1995) , year =

    1995

  62. [62]

    Theoretical Computer Science , volume =

    Wieslaw Zielonka , title =. Theoretical Computer Science , volume =

  63. [63]

    Proceedings of the Seventeenth Annual Symposium on Theoretical Aspects of Computer Science (STACS-2000) , pages =

    Marcin Jurdzinski , title =. Proceedings of the Seventeenth Annual Symposium on Theoretical Aspects of Computer Science (STACS-2000) , pages =

    2000

  64. [64]

    Henzinger and Rupak Majumdar , title =

    Luca de Alfaro and Thomas A. Henzinger and Rupak Majumdar , title =. Proceedings of the Twelfth International Conference on Computer Aided Verification (CAV-2001) , series =. 2001 , pages =

    2001

  65. [65]

    Proceedings of the Twenty-first Annual IEEE Symposium Conference on Logic in Computer Science (LICS-2006) , pages =

    Thomas Ball and Orna Kupferman , title =. Proceedings of the Twenty-first Annual IEEE Symposium Conference on Logic in Computer Science (LICS-2006) , pages =

    2006

  66. [66]

    Theoretical Computer Science , volume =

    Krishnendu Chatterjee and Laurent Doyen , title =. Theoretical Computer Science , volume =

  67. [67]

    Ferguson , title =

    Thomas S. Ferguson , title =. Theoretical Computer Science , volume =. 1998 , publisher =

    1998

  68. [68]

    Deshmukh and Sela Mador-Haim and Milo M

    Abhishek Udupa and Arun Raghavan and Jyotirmoy V. Deshmukh and Sela Mador-Haim and Milo M. K. Martin and Rajeev Alur , booktitle =

  69. [69]

    Beyene and Corneliu Popeea and Andrey Rybalchenko , title =

    Tewodros A. Beyene and Corneliu Popeea and Andrey Rybalchenko , title =. Proceedings of the Twenty-Fifth International Conference on Computer Aided Verification (CAV-2013) , series =

    2013

  70. [70]

    Proceedings of the Forty-First ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-2014) , year =

    Tewodros Beyene and Swarat Chaudhuri and Corneliu Popeea and Andrey Rybalchenko , title =. Proceedings of the Forty-First ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-2014) , year =

    2014

  71. [71]

    Artificial Intelligence , volume=

    Giuseppe De Giacomo and Yves Lesp. Artificial Intelligence , volume=

  72. [72]

    Xiong, Liping and Liu, Yongmei , booktitle=

  73. [73]

    Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2005) , pages =

    Aidan Harding and Mark Ryan and Pierre-Yves Schobbens , title =. Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2005) , pages =. 2005 , publisher=

    2005

  74. [74]

    Proceedings of the Twenty-second International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2016) , year =

    Daniel Neider and Ufuk Topcu , title =. Proceedings of the Twenty-second International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2016) , year =

    2016

  75. [75]

    Dantam and Swarat Chaudhuri and Lydia E

    Yue Wang and Neil T. Dantam and Swarat Chaudhuri and Lydia E. Kavraki , title =. Proceedings of the Twenty-sixth International Conference on Automated Planning and Scheduling (ICAPS-2016) , pages =

    2016

  76. [76]

    The International Journal of Robotics Research , volume =

    Neil T Dantam and Zachary K Kingston and Swarat Chaudhuri and Lydia E Kavraki , title =. The International Journal of Robotics Research , volume =

  77. [77]

    ACM Transactions on Computational Logic , volume =

    Daniel Neider and Shambwaditya Saha and Parthasarathy Madhusudan , title =. ACM Transactions on Computational Logic , volume =

  78. [78]

    Proceedings of the Twenty-fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2018) , year =

    Tom. Proceedings of the Twenty-fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2018) , year =

    2018

  79. [79]

    Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-2016) , pages =

    Azadeh Farzan and Zachary Kincaid , title =. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-2016) , pages =

    2016

  80. [80]

    Proceedings of the ACM on Programming Languages , volume =

    Azadeh Farzan and Zachary Kincaid , title =. Proceedings of the ACM on Programming Languages , volume =

Showing first 80 references.