Counting without choices cannot express every polynomial-time query

← All digests

Family 243 · Mathematical logic
Importance 5/5 · Provisional editorial rating
Sources consulted 2026-10-21

1. The question

A graph has no preferred first vertex. An ordinary algorithm receives its vertices in some encoded order and may use that order internally, provided the final answer does not depend on how the vertices were named.

What if the computational language is forbidden from making arbitrary choices among indistinguishable vertices? It can construct sets and count their members, but it cannot simply select one element of an unordered nonempty set. Can such a language still express every polynomial-time property?

Family 243 contains two manuscripts. M1, dated 23 September 2026, claims that full choiceless polynomial time with counting cannot capture polynomial time. M2, dated 24 September, claims that adding witnessed symmetric choice strictly increases its expressive power. Both address Boolean queries, not merely the difficulty of constructing a particular auxiliary object.

2. Background and essential definitions

Queries on unordered structures

A finite relational structure is a finite set equipped with relations, such as the edge relation of a graph. A Boolean query assigns true or false and is unchanged by isomorphism, meaning a renaming of the elements that preserves all relations.

A polynomial-time query has an ordinary deterministic algorithm whose running time is bounded by a polynomial in the input size. The algorithm may use an order in the encoding; only its final answer must be invariant.

Descriptive complexity asks which logical or computational formalisms describe exactly such queries. A formalism captures polynomial time if every polynomial-time invariant query is expressible in it and its expressions can be evaluated in polynomial time.

Choiceless polynomial time with counting

The papers abbreviate the counting version as CPT. Its objects are hereditarily finite sets over the input atoms. Starting from the input elements, it may build finite sets of atoms, sets of those sets, and so on. For example, an unordered pair of vertices can be an object without selecting which vertex comes first.

The rank measures nesting depth. The full formalism imposes no fixed rank bound. It does impose polynomial resource bounds on the computation and on the number of recursively occurring objects. The cardinality operation returns the size of a finite set as a canonical finite ordinal.

Every operation respects input automorphisms. A program can form an entire definable family and count it, but it cannot obtain an arbitrary ordering for free. This is a restriction on representation and choice, not a restriction to shallow sets or to formulas without iteration.

Witnessed symmetric choice

An automorphism is a permutation of the input preserving every relation. A set is an orbit under a group of automorphisms if those automorphisms can move any member to any other.

Witnessed symmetric choice permits selecting from such an orbit, while constructing automorphisms that certify the symmetry. The witnesses must preserve the entire input and fix the parameters and preceding computation states. It is not enough to observe informally that the candidates look interchangeable.

The extension, written CPT+WSC, has explicit failure semantics when witnesses or resource bounds fail. M2 constructs a separating sentence that always returns true or false on every finite input, so its separation does not rely on treating malformed computations as positive answers.

3. Development history and previous partial results

Immerman and Vardi showed that fixed-point logic captures polynomial time on finite structures supplied with a linear order. Without an order, the general question is much harder. Chandra and Harel asked about effective descriptions of polynomial-time queries, and Gurevich formulated the broader logic-capture problem.

Blass, Gurevich and Shelah introduced choiceless polynomial time in the late 1990s and conjectured that adding counting still would not capture all polynomial-time queries. Their later work examined finite-field linear algebra and Cai–Fürer–Immerman, or CFI, constructions as possible sources of separation.

CFI structures hide a global parity obstruction from bounded-variable counting logic. They supplied a foundational lower bound for fixed-point logic with counting. But CPT is stronger than that logic. Dawar, Richerby and Rossman showed that certain preordered CFI queries are definable choicelessly, while proving lower bounds when activated-set rank is restricted. Pakusa, Schalthöfer and Selman extended positive results to further preordered families.

This history makes the unrestricted-rank qualification crucial. A lower bound for every fixed nesting depth does not exclude a polynomial-time program whose nesting depth grows with input size.

Other work established functional limitations. Rossman ruled out constructing all hyperplanes of a finite vector space in CPT; Pago ruled out certain fine preorders of hypercubes and developed circuit approaches for restricted algorithms. These results obstruct particular constructions but do not, by themselves, exhibit an invariant yes/no query outside full CPT.

Symmetry-based choice has a separate development through Gire–Hoang and Dawar–Richerby. Lichter and Schweitzer introduced the witnessed-choice extension used by M2 and related isomorphism testing to canonization under suitable hypotheses. Its additional expressive power over the full counting formalism was a separate question.

The manuscripts acknowledge an earlier noncapture claim by Shelah, while noting that later literature continued to treat the full counting capture question as open. They give separate arguments and do not use that earlier claim as a theorem input.

4. What the new manuscripts claim

M1: a polynomial-time linear query outside full CPT

M1 defines a query $Q$ on all structures in a fixed vocabulary of eight binary relations. From those relations it forms a linear system over

$$\mathbb F_3=\{0,1,2\},$$

with arithmetic modulo three. The answer is whether that system is consistent.

The construction has at most twice as many unknowns as input elements and at most a quadratic number of equations. Coefficients are computed by polynomially many loops, and Gaussian elimination decides consistency in polynomial time. Renaming the input merely permutes equations and unknowns.

M1 asserts that no program of full CPT with counting defines this query. The input is not promised to be a well-formed grid or gadget. Its coefficient and empty-sum conventions define $Q$ on every finite structure, including degenerate cases.

On nonempty structures, the same query is definable in fixed-point logic with counting extended by solvability over $\mathbb F_3$, and also by rank over $\mathbb F_3$. Thus the manuscript also claims that neither of those two extended logics is contained in CPT.

M2: witnessed choice adds expressive power

M2 constructs a fixed CPT+WSC sentence in the same eight-relation vocabulary, with one syntactic occurrence of the witnessed-choice operator, such that its Boolean query is not definable in CPT.

One occurrence does not mean one choice in the entire computation. The operator may make successive choices during iteration and may be evaluated for different parameter tuples.

Its all-input query is defined separately from M1’s linear-consistency query. Both distinguish the same family of charged-grid pairs, but M1’s noncapture theorem alone would not supply a legal witnessed-choice definition.

M2 retains and presents the common support and counting arguments from M1, while adding the witnessed-choice construction and a direct comparison of arbitrary CPT terms. Its final lower bound does not use the interpretation-program characterization employed by M1.

5. Why the advance matters

Importance: 5/5, provisional. The family claims to eliminate a major candidate for capturing polynomial time on unordered structures and to establish a strict expressiveness increase from a carefully controlled form of choice.

The separating problem is linear algebra, a basic polynomial-time task. The obstruction is therefore not lack of a fast conventional algorithm. It is the inability of one invariant formalism to organize enough information while respecting symmetry and its polynomial resources.

The second claim helps locate the obstruction: certified choices can express a query that unrestricted set nesting and counting alone cannot. It gives a concrete role to symmetry witnesses rather than treating arbitrary ordering as an unexplained primitive.

These conclusions do not resolve whether some other logic captures polynomial time. They also have no direct implication for $\mathrm P$ versus $\mathrm{NP}$. The comparison is between ways of expressing already polynomial-time invariant queries.

6. The main idea

Hide one unit of total charge

Both papers construct structures from a three-dimensional box grid of side length $L$. Each edge carries a bounded collection of vector and scalar states over $\mathbb F_3$. Vertex configurations choose compatible incident-edge states and require a prescribed signed scalar sum, called the charge.

The input atoms encode these edge states and configurations. There are two structures of equal size

$$N=\Theta(L^3):$$

one has total charge zero, the other total charge one.

M1’s query permits field-valued weights on the configurations at each vertex, summing to one. It requires the weighted scalar value of an edge to agree at its two endpoints. Summing all vertex equations cancels every edge contribution, because each edge enters one vertex and leaves another.

Consistency therefore forces total charge zero. The zero-charge structure has a solution supplied by the all-zero configurations; the unit-charge structure does not. This argument allows arbitrary field-valued weights, not just weights that select one configuration.

Small orbits force small supports at every rank

A support for a constructed object is a tuple of input atoms such that every relevant automorphism fixing that tuple also fixes the object. If a computation activates only polynomially many objects and the whole activation family is invariant, each object’s orbit is polynomially bounded.

The new support estimate uses a larger nonabelian automorphism group $H$ and its central subgroup $K$ of divergence-free scalar flows. For an object with $H$-orbit size at most $N^q$, the manuscript obtains a $K$-support of size

$$O_q\bigl(L(1+\log L)^2\bigr).$$

The estimate is independent of the object’s set rank. Commutators in $H$ force the linear data detecting a stabilizer to have nonzero curl on only a small number of faces. Subtracting gradients concentrates those data on few edges. The nonabelian action supplies the restriction; central flows alone would not give the same bound.

Transfer indistinguishability to an entire computation

The grid pairs remain indistinguishable by counting formulas of sufficiently bounded variable width. A charge discrepancy can be moved through a large remaining grid component while avoiding the atoms already named by a formula.

The paper transfers this comparison from atoms to all hereditarily supported finite sets, including sets of arbitrary finite rank. Forms evaluated at supporting tuples describe the objects; exact equality, membership and counting must all transfer.

M1 then encodes a complete interpretation-program run as a polynomial-size hereditary family. Its state formulas can grow in length with the input, but use a fixed number of variable names depending only on the program. Choosing the grid sufficiently large after fixing the program forces equal halt stages and outputs on the pair.

M2 instead describes the actual evaluations of CPT terms directly. It carefully distinguishes resource-failure defaults and rejects spurious proposed outputs. In both routes, the lower bound covers the entire formalism rather than a particular style of algorithm.

Certified choices expose the hidden charge

M2 uses a tuple of four vertex blocks to define an order of the underlying grid and a spanning tree. It chooses edge states only outside the tree.

At each step, a local face translation aligns the vector coordinates of two candidate states. A circulation around the new edge and its return path in the tree corrects the scalar difference. These transformations preserve earlier choices.

The program enumerates suitable candidate maps and keeps only automorphisms of the full input fixing the required history. A transitivity guard certifies the choice set; dummy choices keep the sentence legal on arbitrary inputs. Once the non-tree states are chosen, monotone elimination along the tree decides whether compatible vertex configurations exist.

The zero-charge grids always pass and the unit-charge grids always fail. The ordinary CPT comparison says that no fixed CPT sentence can maintain those opposite answers on all sufficiently large pairs, giving the strict separation.

7. Scope, limitations, and open questions

Counting is included throughout, and finite-set rank is unrestricted. The polynomial resource bounds still apply. The proof’s extra preorders and scalar-comparison relations are analytical tools for comparing structures, not extra input relations silently supplied to the program.

The query in M1 is defined on all finite inputs in its fixed binary vocabulary. M2 likewise supplies a Boolean value on every input and requires legal witnessing for every reachable choice history, not merely one favorable path.

Neither result shows that CPT+WSC captures all polynomial-time queries. The effect of nested witnessed-choice operators also remains a separate question. Earlier separations over fixed-point logic with counting use a smaller base formalism and should not be identified with the full-CPT statement here.

The broader search for a logic capturing polynomial time on unordered structures remains open in the scope of these manuscripts. The claimed result rules out one candidate and distinguishes one extension, rather than settling that entire program.

8. Sources and further reading

Blass, Gurevich and Shelah, Choiceless polynomial time, Annals of Pure and Applied Logic 100 (1999), 141–187, introduces the model. Their On polynomial time computation over unordered structures, Journal of Symbolic Logic 67 (2002), 1093–1125, discusses the counting and linear-algebra questions.

Cai, Fürer and Immerman, An optimal lower bound on the number of variables for graph identification, Combinatorica 12 (1992), 389–410, is the counting-logic predecessor. Dawar, Richerby and Rossman, Choiceless polynomial time, counting and the Cai–Fürer–Immerman graphs, Annals of Pure and Applied Logic 152 (2008), 31–50, explains the importance of set rank.

Lichter and Schweitzer, Choiceless polynomial time with witnessed symmetric choice, later published in Journal of the ACM 71 (2024), supplies the precise choice semantics used by M2.

Source manuscripts

• M1. OpenAI, Choiceless polynomial time with counting does not capture polynomial time (September 23, 2026).
• M2. OpenAI, Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting (September 24, 2026).

Sources consulted on 21 October 2026 at repository revision 1581d4c. Download the manuscript citations.