Prover-Adversary games for systems over (non-deterministic) branching programs

Anupam Das; Avgerinos Delkos

arxiv: 2508.16014 · v4 · pith:SFVFFYWNnew · submitted 2025-08-22 · 💻 cs.CC · cs.LO· math.LO

Prover-Adversary games for systems over (non-deterministic) branching programs

Anupam Das , Avgerinos Delkos This is my paper

Pith reviewed 2026-05-21 23:16 UTC · model grok-4.3

classification 💻 cs.CC cs.LOmath.LO

keywords proof complexitybranching programsprover-adversary gamesImmerman-Szelepcsenyi theoremnon-deterministic branching programsalternating branching programsNL equals coNL

0 comments

The pith

Prover-adversary games polynomially characterize the proof systems eLDT and eLNDT for deterministic and non-deterministic branching programs.

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

The paper introduces Pudlak-Buss style Prover-Adversary games that characterize proof systems reasoning over deterministic branching programs and non-deterministic branching programs. It proves that these games are polynomially equivalent to the existing systems eLDT and eLNDT respectively. The non-deterministic case requires defining a negation operation on NBPs, which rests on a non-uniform version of the Immerman-Szelepcsenyi theorem establishing coNL equals NL. Using the same techniques, the paper shows a proof-complexity version of that theorem in which eLNDT becomes polynomially equivalent to proof systems over boundedly alternating branching programs. A reader would care because the equivalences supply direct game-based views of established proof systems and link them to classical results on nondeterminism.

Core claim

Pudlak-Buss style Prover-Adversary games are polynomially equivalent to eLDT for deterministic branching programs and to eLNDT for non-deterministic branching programs; the latter equivalence requires a workable negation for NBPs obtained via a non-uniform formalization of the Immerman-Szelepcsenyi theorem that coNL equals NL, and the same methods yield that eLNDT is polynomially equivalent to systems over boundedly alternating branching programs.

What carries the argument

Pudlak-Buss style Prover-Adversary games defined over branching programs, together with a polynomial negation operation on non-deterministic branching programs.

If this is right

eLDT is polynomially equivalent to the Prover-Adversary game played on deterministic branching programs.
eLNDT is polynomially equivalent to the Prover-Adversary game played on non-deterministic branching programs.
eLNDT is polynomially equivalent to any proof system whose lines are boundedly alternating branching programs.
The equivalences translate directly into polynomial-size translations between proofs and winning strategies.

Where Pith is reading between the lines

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

The game view may supply new combinatorial arguments for proving lower bounds on eLNDT by analyzing the existence of winning strategies.
If the non-uniform negation construction extends to other models, similar game characterizations could apply to additional classes such as NL and coNL.
The results suggest that bounded alternation in branching programs can be simulated inside eLNDT without superpolynomial blowup.

Load-bearing premise

A polynomial-size negation for non-deterministic branching programs can be constructed from a non-uniform version of the Immerman-Szelepcsenyi theorem.

What would settle it

An explicit family of non-deterministic branching programs with no polynomial-size negated version under the non-uniform coNL=NL construction, or a superpolynomial separation between eLNDT proofs and the corresponding game strategies.

read the original abstract

We introduce Pudlak-Buss style Prover-Adversary games to characterise proof systems reasoning over deterministic branching programs (BPs) and non-deterministic branching programs (NBPs). Our starting points are the proof systems eLDT and eLNDT, for BPs and NBPs respectively, previously introduced by Buss, Das and Knop. We prove polynomial equivalences between these proof systems and the corresponding games we introduce. This crucially requires access to a form of negation of branching programs which, for NBPs, requires us to formalise a non-uniform version of the Immerman-Szelepcsenyi theorem that coNL = NL. Thanks to the techniques developed, we further obtain a proof complexity theoretic version of Immerman-Szelepcsenyi, showing that eLNDT is polynomially equivalent to systems over boundedly alternating branching programs.

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.

Desk Editor's Note private letter to a colleague

This paper adds prover-adversary games for eLDT and eLNDT with polynomial equivalences and derives a proof-complexity version of Immerman-Szelepcsenyi via non-uniform coNL=NL for NBP negation.

read the letter

The main thing here is that the authors define Pudlak-Buss style prover-adversary games for the existing eLDT and eLNDT systems over deterministic and non-deterministic branching programs. They prove the games are polynomially equivalent to the proof systems and then use the same machinery to show eLNDT is polynomially equivalent to systems over boundedly alternating branching programs. That last step is their proof-complexity analogue of Immerman-Szelepcsenyi. The non-uniform formalization of coNL=NL is needed to get a workable negation for NBPs so the games can be defined in the first place. What is new is the concrete games themselves and the non-uniform construction. The paper does a clean job laying out the game rules and deriving the equivalences step by step from the definitions, with clear links back to the earlier Buss-Das-Knop systems. The citation pattern is standard and appropriate for this corner of proof complexity. The soft spot is the size and overhead of the non-uniform negation construction for NBPs. The polynomial claims for eLNDT and the game equivalence rest on producing a co-NBP of size poly(s) from an NBP of size s and keeping the eLNDT proof overhead polynomial. The paper gives a construction in section 4 and the appendix, but the bounds have to be checked tightly. If any hidden super-polynomial factor appears in the simulation or the proof, both the game equivalence and the bounded-alternation result would fail at the polynomial level. This is worth a careful read rather than a fatal problem, but it is load-bearing. The work is aimed at people already working on space-bounded proof complexity and branching-program systems. A reader who knows the prior game characterizations and Immerman-Szelepcsenyi will get the most from the new games and the IS analogue. It deserves a serious referee because the results are new in the subfield and the technical development is direct and grounded.

Referee Report

1 major / 2 minor

Summary. The manuscript introduces Pudlak-Buss style prover-adversary games to characterize the proof systems eLDT (over deterministic branching programs) and eLNDT (over non-deterministic branching programs). It proves polynomial equivalences between these systems and the introduced games. For NBPs this requires a non-uniform formalization of the Immerman-Szelepcsenyi theorem (coNL = NL) to obtain a workable negation operation. As a further consequence the paper derives a proof-complexity analogue of IS, establishing that eLNDT is polynomially equivalent to systems over boundedly alternating branching programs.

Significance. If the polynomial-size equivalences hold, the work supplies game characterizations for branching-program proof systems that may facilitate lower-bound arguments and clarifies the role of negation in non-deterministic settings. The non-uniform IS formalization and the resulting proof-complexity version of the theorem are notable contributions that extend earlier results of Buss, Das and Knop.

major comments (1)

[§4 and Appendix] §4 (and the appendix construction): the central polynomial equivalence between eLNDT and the corresponding prover-adversary game rests on producing, from an NBP of size s, a co-NBP of size poly(s) whose correctness is provable inside eLNDT with only polynomial overhead. The manuscript must explicitly state and verify these size and proof-size bounds; if either is super-polynomial the claimed equivalences for eLNDT and the bounded-alternation systems collapse.

minor comments (2)

[§2] Notation for the non-uniform IS formalization and the precise definition of 'negation' for NBPs should be introduced earlier (ideally in §2 or §3) to improve readability for readers unfamiliar with the non-uniform setting.
[Abstract] The abstract states that 'polynomial equivalences' are proved; a brief parenthetical remark on the degree of the polynomials or the precise systems involved would help readers assess the strength of the result at a glance.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their positive summary of the paper's contributions and for the constructive major comment. We address it point-by-point below and will revise the manuscript to incorporate the requested clarifications.

read point-by-point responses

Referee: [§4 and Appendix] §4 (and the appendix construction): the central polynomial equivalence between eLNDT and the corresponding prover-adversary game rests on producing, from an NBP of size s, a co-NBP of size poly(s) whose correctness is provable inside eLNDT with only polynomial overhead. The manuscript must explicitly state and verify these size and proof-size bounds; if either is super-polynomial the claimed equivalences for eLNDT and the bounded-alternation systems collapse.

Authors: We agree that the polynomial equivalence between eLNDT and the prover-adversary game for NBPs depends on the co-NBP construction having polynomial size and admitting a polynomial-size eLNDT proof of correctness. The appendix already contains the non-uniform Immerman-Szelepcsenyi formalization that yields such a construction, and the overall polynomial overhead follows directly from the size of the NL machine simulation and the inductive definition of the eLNDT proofs. Nevertheless, we accept the referee's observation that these bounds are not stated with sufficient explicitness. In the revised version we will add, in §4 and the appendix, a dedicated paragraph that (i) states the concrete polynomial size bound on the produced co-NBP, (ii) states the polynomial bound on the eLNDT proof size, and (iii) sketches the verification that both remain polynomial, thereby confirming that the claimed equivalences are preserved. This change strengthens the exposition without altering any theorems. revision: yes

Circularity Check

0 steps flagged

Minor self-citation to prior eLDT/eLNDT introduction; equivalences and non-uniform IS formalization are independently derived

full rationale

The paper starts from previously introduced systems eLDT and eLNDT (Buss, Das, Knop) and proves new polynomial equivalences to Pudlak-Buss style prover-adversary games. The key technical step is formalizing a non-uniform version of Immerman-Szelepcsenyi to obtain negation for NBPs, which is then used to establish the equivalences and a proof-complexity analogue of IS for boundedly alternating programs. No quoted step reduces a 'prediction' or central result back to a fitted parameter or self-definition by construction. The self-citation is limited to the starting definitions of the systems and is not load-bearing for the new game equivalences or the IS formalization; those rest on explicit constructions and proofs inside the paper. This is a standard, non-circular extension of prior work.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work relies on standard background results in proof complexity and complexity theory rather than new fitted parameters or invented physical entities. The key non-standard element is the formalisation of a non-uniform Immerman-Szelepcsenyi theorem, which functions as a domain assumption.

axioms (2)

domain assumption Standard properties of deterministic and non-deterministic branching programs as models of computation
Invoked throughout the definitions of eLDT, eLNDT and the new games.
domain assumption Existence of a workable negation operation for branching programs that preserves polynomial size
Explicitly required for the equivalences, especially for NBPs.

pith-pipeline@v0.9.0 · 5683 in / 1572 out tokens · 38581 ms · 2026-05-21T23:16:59.575607+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

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

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We prove polynomial equivalences between these proof systems and the corresponding games we introduce. This crucially requires access to a form of negation of branching programs which, for NBPs, requires us to formalise a non-uniform version of the Immerman-Szelepcsényi theorem that coNL = NL.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

the k-decider ABk_i C ... tB_k , ABk_i C → A, Bi, tB_k+1

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.