1 Introduction
A query on finite relational structures is a property unchanged by isomorphism. It belongs to polynomial time if a deterministic algorithm decides it in time polynomial in the size of an ordinary encoding of the structure. The algorithm may use the order of that encoding; its answer must be independent of the order. An unordered structure, in contrast, does not supply such an order as one of its relations. Descriptive complexity asks which formalisms can express every polynomial-time query without first choosing an order.
Choiceless polynomial time with counting, denoted \CPT throughout this paper, operates on the hereditarily finite sets built from the input elements as atoms. These are finite sets whose members are atoms or further such sets, with no infinite descending membership chain. The formalism permits set operations, comprehension and the cardinality operation \mathsf{Card}, which returns a finite von Neumann ordinal. Each fixed program has polynomial bounds on its computation and on the number of recursively occurring objects. Its operations commute with input automorphisms and do not provide an arbitrary choice of an ordering. We use the established equivalent formulation by interpretation programs; its exact syntax, counting operation and quotient semantics are stated in Section 6. In particular, \CPT here always includes counting and has no imposed bound on the rank of its sets.
To say that this formalism captures polynomial time on unordered finite structures means that every isomorphism-invariant polynomial-time query, in every fixed finite relational vocabulary, is definable by a program of the formalism. We first specify a query on all inputs in a fixed vocabulary.
1.1 The separating query
Throughout, let \mathbb F=\mathbb F_3. Fix the binary relational vocabulary
The subscripts on the last three relation symbols denote elements of \mathbb F. For a finite \tau-structure A, set
No disjointness or equivalence-relation assumption is imposed here. In particular, X and Y may overlap. Define, in \mathbb F,
If several of the relations \mathsf Z_\delta(y,x) hold, all their contributions are included.
Introduce two separate families of unknowns, (\lambda_a)_{a\in X} and (\mu_y)_{y\in Y}. Thus even when a=y, \lambda_a and \mu_y are different unknowns. The system defining our query has the equations
and, for every (t,y)\in X\times Y for which
the equation
Let Q(A) mean that this system is consistent over \mathbb F. Repeated identical equations are harmless; they remain equations and are not added together. An empty sum is zero, and a system with no equations is consistent. These conventions make Q a query on all finite \tau-structures.
1.2 Main result
Theorem 1. The query Q on all finite structures in the fixed vocabulary \tau of eight binary relations is isomorphism-invariant and decidable in deterministic polynomial time, but is not definable in full choiceless polynomial time with counting.
Theorem 1 confirms the noncapture conjecture of Blass, Gurevich and Shelah for the full counting formalism; its historical formulation is discussed below. We first record the ordinary algorithmic upper bound. The rest of the paper proves the choiceless lower bound.
Proposition 2. The query Q is isomorphism-invariant and decidable in deterministic polynomial time from an ordered encoding of its input structure.
Proof. An isomorphism carries X,Y,X_t to their counterparts, preserves the coefficient in (1), and carries the test (3) to the corresponding test. Consequently it permutes the two families of unknowns and the equations compatibly. Consistency is therefore invariant.
If the input has n elements, there are at most 2n unknowns and n+n^2 equations. All coefficients and tests can be computed by polynomially many loops over the input universe; for example, a direct implementation uses O(n^4) operations over the fixed field. Gaussian elimination then decides consistency in polynomial time [24, Sections 14.4â14.5]. Any input order may be used to list the rows and columns: changing it does not change consistency.
The same query is expressible in two standard linear-algebraic logics. Following Grädel and Pakusa [10, Section 2], write \mathrm{FPS}_3 for fixed-point logic with counting (FPC) extended by the solvability operator over \mathbb F_3, and \mathrm{FPR}_3 for FPC extended by the rank operator over \mathbb F_3. Their two-sorted syntax allows bounded number variables alongside the unordered input elements. We state the consequence for nonempty structures, so that the matrix index sets in its proof are nonempty.
Corollary 3. On nonempty finite \tau-structures, Q is definable in both \mathrm{FPS}_3 and \mathrm{FPR}_3. Consequently neither of these logics is contained in \CPT.
FPC defines the coefficient predicates and the row test for Q. Section 8 gives the resulting solvability formula and compares the ranks of the coefficient and augmented matrices. The nonempty witnesses constructed below give both noncontainments.
1.3 Background and the obstruction to rank-dependent arguments
The ordered case provides the starting point. Immerman and Vardi showed that first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries on finite structures supplied with a linear order [15, 25]. For unordered structures, Chandra and Harel asked whether polynomial-time queries admit an effective enumeration [6, Section 5, p. 118]. Gurevich formulated the question in terms of a logic capturing polynomial time and conjectured that no such logic exists [14, Section 7]. Excluding CPT with counting as a candidate leaves this broader question open.
Blass, Gurevich and Shelah introduced choiceless polynomial time to study computation on unordered structures using hereditarily finite sets rather than arbitrary choices of an ordering [2]. Their original 1997 preprint explicitly conjectured that the extension by counting is still a proper fragment of polynomial time [2, 1997 version, Introduction, p. 3]. Their later study of unordered computation examined CFI instances and finite-field linear algebra as possible sources of separation, carefully distinguishing representations with common and independent row and column index sets [3, Sections 4 and 6]. The query here is a particular linear-consistency problem over \mathbb F_3, defined without a promise on the input structure.
Shelahâs early work claimed noncapture for counting extensions of choiceless computation [23, Introduction and Section 4]. Later accounts continued to state the capture problem as open, from Blass, Gurevich and Shelah [3, Section 7] through the 2025 work of Dawar, Grädel, Kullmann and Pago [8, Section 2.2]. We give a separate proof for the explicit query above; Shelahâs claim is not a theorem input to this argument.
The construction of Cai, Fßrer and Immerman established the central example of a polynomial-time graph query beyond fixed-point logic with counting [4]. Its local gadgets conceal a global parity obstruction from bounded-variable counting formulas. This is an antecedent of our charge-based witnesses, not an identification of those witnesses with the original CFI graphs. The passage from counting logic to choiceless computation is substantial: Dawar, Richerby and Rossman showed that the preordered CFI query obtained from ordered base graphs is definable without counting, while even counting does not suffice if set rank is restricted to o(\log n/\log\log n), where n is the input size [9, Theorems 17 and 40, 2007 author version]. In particular, their lower bound for every fixed rank cannot by itself yield a separation for the full formalism. Pakusa, SchalthÜfer and Selman extended the positive result to connected preordered base graphs whose colour classes have logarithmic size in the number of base vertices [21, Theorem 1]. The preorder orders classes of base vertices, rather than all vertices of the resulting CFI structure.
Positive algebraic results also go beyond the original CFI family. Abu Zaid, Grädel, Grohe and Pakusa obtained choiceless canonization, that is, construction of canonical ordered copies, when a supplied preorder has bounded classes whose induced substructures have Abelian automorphism groups [1, Corollary 19]. Their procedure uses specially structured cyclic systems of equations, not arbitrary unordered linear systems [1, Definition 6 and Theorem 14]. Lichter and Schweitzer obtained analogous canonization for graphs when these induced groups are dihedral or cyclic [17, Theorem 1]. These results show why the lower-bound argument must exploit the particular action of its nonabelian group, rather than noncommutativity alone.
Functional lower bounds expose different limits. Rossman proved that CPT with counting cannot construct the set of hyperplanes of an input finite vector space over a fixed finite field [22, Theorem 6.1, author version]. Pago proved that no such program constructs, on every hypercube with N vertices, a total preorder with classes of size O(\log N) [19, Theorem 2 and Corollary 3, full version]. The latter statement also excludes encodings from which the preorder can be recovered in CPT. It obstructs the route of first constructing a fine preorder and then applying the preordered CFI algorithm. These are functional obstructions, not nondefinability of a Boolean query.
Pagoâs symmetric-XOR-circuit approach relates restricted classes of choiceless CFI algorithms to circuit families [20, Theorems 2, 31 and 33, full version]. The translation permits polynomially many circuit images under automorphisms of the base graph; the circuit lower bound assumes an invariant circuit and different bounds on connections between gates. These hypotheses differ, so that argument does not establish nondefinability for the entire restricted algorithm class.
The support-and-transfer architecture has older roots. Blass, Gurevich and Shelah developed supports and representations by forms evaluated at supporting tuples, called molecules [2, Sections 8â9, published version]. Dawar, Richerby and Rossman developed rank-sensitive support bounds and a counting transfer for hereditarily supported objects [9, Sections 7â8, 2007 author version]. Using the group-relative homogeneity from Section 4, we adapt that representation method in Section 5 and prove the required exact counting statements. The support estimate in Section 3 instead uses a larger nonabelian group to obtain small supports for its central subgroup, independently of HF rank. Its standard class-two group and alternating-form ingredients, as well as the projection and counting-game methods used for the atom comparison, are credited at their respective proofs. The grid-specific estimate and the quantitative transfer are proved here.
Finally, the connection to arbitrary programs uses the interpretation characterization of Grädel, Pakusa, SchalthÜfer and Kaiser [11, Theorem 1]. We use the binary, two-dimensional formulation of Grohe, Schweitzer and Wiebking [12, Section 6, Theorem 18, arXiv version 1], including its generated-equivalence and existential-representative quotient convention. This characterization is an external input. Section 6 proves the further facts needed here: a polynomial bound on the complete hereditary encoding of a run, and exact formulas for its states whose variable bound is independent of the number of stages. Thus neither a bound on HF rank nor a restriction to a particular algorithmic construction is imposed on the programs excluded by the theorem.
1.4 Proof overview
For each side length L, we build two structures from the three-dimensional box grid. Each edge carries states consisting of a bounded collection of \mathbb F_3^2 face coordinates and one scalar. A vertex configuration chooses incident edge states that agree on their shared face coordinates and whose scalars have a prescribed signed sum, called its charge. Both kinds of states become input atoms, linked only by the fixed binary relations. The two structures have all charges zero, or one charge equal to one. Their size is N=\Theta(L^3). The queryâs normalization equations assign field-valued weights summing to one to the configurations at each vertex. Its consistency equations make the weighted scalar value of an edge agree at its two endpoints. Summing the vertex divergence equations then forces the total charge to be zero, since each edge enters one vertex and leaves another. This argument allows arbitrary field-valued weights; it does not assume that a solution selects one configuration per vertex. The all-zero configurations give a solution in the zero-charge structure, so the query has opposite answers on the pair.
The challenge is to show that every fixed full \CPT program eventually gives the same answer on this pair. Three steps connect the symmetries of these atoms to the complete computation.
Rank-independent supports. The structures have an automorphism group H containing a central subgroup K of divergence-free scalar flows on the edges. A tuple of atoms is a K-support of an object if every element of K fixing that tuple also fixes the object. For any fixed q, every hereditarily finite object with H-orbit of size at most N^q has a support of size O_q(L(1+\log L)^2). The bound does not depend on the objectâs rank. Commutators in H force the linear functionals detecting a stabilizer to have nonzero curl on few faces. Subtracting explicitly constructed gradients then concentrates those functionals on few edges. This is the role of the nonabelian group; central flows alone do not supply this argument.
Counting equivalence for all supported objects. For analysis only, we add a preorder identifying certain classes of atoms and relations comparing scalar differences. These relations are not given to the program. With M=\lfloor L^{7/4}\rfloor, the two expanded structures agree on all first-order counting sentences using at most M variable names. A charge discrepancy can be moved along paths in the large component that remains after the edges touched by the assigned atoms are removed. Within either expansion, equality of sufficiently wide counting types also determines the K-orbit of a short tuple.
Fix a support length s=O_q(L(1+\log L)^2). Consider all hereditarily finite objects for which the object and every recursive member have a K-support of length at most s. This is a countably infinite domain of finite objects, containing objects of every finite rank. We represent its objects by finite forms evaluated at supporting atom tuples, then prove equality, membership and exact counting transfer. For each fixed m, the two domains agree on all counting sentences with at most m variable names when L is sufficiently large. The key width cost is O_{q,m}(L^{3/2}(1+\log L)^3)=o(M).
The entire computation fits the comparison. The interpretation characterization supplies a fixed program whose successive states are quotients of definable pairs from the preceding state. We encode every quotient vertex by a tagged set of ordered pairs of preceding vertex codes. A polynomial run has only polynomially many such codes and recursive constituents; this transitive family is H-invariant. The support theorem therefore places the entire encoded trace in the domains just compared.
Finally, each state, halting test and output test has an exact counting-formula definition over its supported domain. Its length may grow with the input, but the number of variable names needed is bounded by a constant depending only on the program. We prove this by a capture-avoiding substitution lemma, including the generated quotient relation and the cardinality comparisons. Choose the program and its constants q,m first, and then take L large. Counting equivalence forces the same halt stage and output on the two structures, contradicting their opposite query answers.
Figure 1: The two routes from the input pair. The charge equations give opposite query answers. The symmetry, logic and computation arguments force every fixed choiceless program to give equal answers for sufficiently large grids. The atom expansions are used only for analysis. If the program decided Q, its equal outputs would contradict the left-hand route.
Section 1.1 defines the query on all inputs, and Section 2 constructs its two test structures. Section 3 proves the support theorem. Sections 4 and 5 establish the counting comparison on atoms and then on supported sets. Section 6 encodes full interpretation computations, and Section 7 fixes the parameters and proves Theorem 1. Section 8 proves the definability of Q in solvability and rank logic.
2 The grid structures
The instances used in the lower bound attach finite groups to the edges of a three-dimensional box. At each vertex we retain the tuples of edge states satisfying a prescribed divergence equation. The group law will supply the nonabelian automorphisms used in the support argument; the query just defined will detect an obstruction to the divergence equations.
2.1 Grid orientations and edge groups
For an integer L\ge2, let G=(V,E) be the box grid with
Each edge is oriented in its positive coordinate direction. Put \epsilon_{ve}=1 if v is the head of e, \epsilon_{ve}=-1 if it is the tail, and \epsilon_{ve}=0 otherwise. The incidence map is
Let F be the set of unit square faces. A face parallel to coordinate directions i<j is traversed first in direction +i, then +j, then -i, then -j. Its edge vector c^f\in\mathbb F^E has coefficient 1 when this traversal follows an edge orientation, -1 when it opposes that orientation, and zero off the face. At each vertex of the face one traversed edge enters and one leaves, so
Write F(e)=\{f\in F:c^f_e\ne0\}, and let F(v) be the set of faces containing v. We shall use
In particular, d(v)\ge1.
For vectors in \mathbb F^2, define the alternating form
The edge groups use the standard finite Heisenberg multiplication [13, Section 2.1], with the face-boundary signs specifying its alternating form. The group P_e attached to an edge e has underlying set (\mathbb F^2)^{F(e)}\times\mathbb F. Its elements are written (u,z), where u=(u_f)_{f\in F(e)}, and its product is
Here 1/2=2 in \mathbb F_3. To verify the group law, denote the bilinear correction term by B_e(u,u'). Bilinearity gives
which is exactly associativity. Alternation gives B_e(u,u)=0; hence (0,0) is the identity and (u,z)^{-1}=(-u,-z). In particular, the last coordinate of (u,z)^{-1}(u',z') is
2.2 Atoms and binary relations
Fix b=(b_v)_{v\in V}\in\mathbb F^V. The universe of A_b is the disjoint union of two kinds of atoms. There is an edge atom (e,u,z) for each edge e and each (u,z)\in P_e. At each vertex v there is a configuration atom for every tuple
satisfying
The coordinates in these descriptions label atoms; they are not members of the atoms as sets. The two kinds of atoms are tagged so they are disjoint.
Figure 2 illustrates the signed face boundary in (5) and the shared-coordinate condition in (8).
Figure 2: A geometric grid face f in directions i<j. Arrows follow the global positive-coordinate orientations; the labels +1,+1,-1,-1 are the coefficients of c^f, so their signed divergence is zero at each corner. At the marked vertex v, the two incident states of one configuration satisfy u_{e,f}=u_{e',f}. The drawing shows the geometric cell underlying these coordinates; the atoms are the states and configurations defined in the text.
Lemma 4. For each L\ge2, the size of A_b is independent of b and equals
In particular,
Every vertex has at least one configuration atom.
Proof. There are 3^{2|F(e)|+1} states on e. At a vertex v, each face f\in F(v) meets precisely two incident edges. Their face coordinates are identified by (8), independently of all other faces. The choices of u therefore contribute 3^{2f(v)} possibilities. The divergence condition is a single linear equation in d(v) variables with a nonzero coefficient, so it has 3^{d(v)-1} solutions for every b_v. This proves (9) and positivity. There are L^3 vertices and 3L^2(L-1)\le3L^3 edges. The displayed bounds follow from |F(e)|\le4, f(v)\le12, and d(v)\le6.
The vocabulary \tau is interpreted as follows; each relation is false on all pairs not specified below.
- â˘
\mathsf{Ed} and \mathsf{Cf} are the diagonals of the edge atoms and configuration atoms, respectively.
- â˘
\mathsf{EB} relates edge atoms on the same edge. The relation \mathsf{VB} relates configuration atoms at the same vertex.
- â˘
\mathsf I(a,x) holds when a is a configuration at a vertex v and x=(e,u_e,z_e) is the state selected by a on an incident edge e.
- â˘
For \delta\in\mathbb F, the relation \mathsf Z_\delta((e,u,z),(e,u',z')) holds precisely when (7) equals \delta.
Thus \mathsf I goes from configurations to edge atoms; it is not made symmetric. The coordinate labels used to construct A_b are not extra symbols in its input vocabulary. In particular, no ordering of the grid or of its blocks is supplied to a program.
2.3 Opposite answers
Fix any vertex v_*\in V, and put
These two charge vectors give structures of the same size by Lemma 4.
Proposition 5. For every L\ge2, the structure A_{b^0} satisfies Q and A_{b^1} does not. More generally, Q(A_b) implies \sum_{v\in V}b_v=0 in \mathbb F.
Proof. For clarity, let X(v) denote the configuration block at a grid vertex v. For any t\in X(v), the set X_t in the definition of the query is exactly X(v). For an edge atom y on e, the test (3) holds precisely when e\ni v: every configuration at v selects one atom on each incident edge, and \mathsf{EB} identifies exactly the edge blocks. If e\ni v, the coefficient C(y,a) has exactly one contributing selected edge atom, and exactly one of its three \mathsf Z_\delta relations holds.
On A_{b^0}, each vertex has a configuration with all coordinates zero. Give it weight \lambda_a=1 and give all other configurations weight zero. For y=(e,u,z) set \mu_y=-z. The normalization equations hold. The selected neighbor of every nonzero-weight configuration on e is (e,0,0), whose group difference from y has last coordinate -z by (7). Thus all equations (4) also hold.
Now suppose the query system on A_b has any solution. The weights \lambda_a are arbitrary field elements; we do not assume that they select a configuration. For each edge choose, only for this proof, its zero atom y_e=(e,0,0). By (7), for e\ni v and a\in X(v) we have C(y_e,a)=z_e(a). The equations of the query give
Multiply the first identity by \epsilon_{ve}, sum over the edges at v, and use (8):
Summing this identity over all vertices cancels each edge contribution, because an oriented edge has one head and one tail. Hence \sum_v b_v=0. For b=b^1 that sum is 1, which is impossible.
The remainder of the argument shows that a fixed choiceless computation cannot distinguish these two structures when L is sufficiently large. The equality of their universe sizes and the fixed binary vocabulary will be used throughout that argument.
3 Small orbits have sparse supports
The automorphisms used in this section have two parts. Face translations form an abelian quotient, but their commutators produce central flows on edges. This interaction constrains the stabilizer of an object with a small orbit. We will turn that constraint into a short tuple of atoms whose pointwise stabilizer in the central flow subgroup fixes the object.
Throughout this section, \mathbb F=\mathbb F_3, L\ge2, and G=(V,E) is the positively oriented grid on \{0,\ldots,L-1\}^3. Its incidence map is \partial:\mathbb F^E\to\mathbb F^V. For a unit square face f, write c^f\in\mathbb F^E for its oriented boundary, so that \partial c^f=0. Let F denote the set of faces and put
We use the alternating form \omega((a,b),(a',b'))=ab'-ba' on \mathbb F^2.
3.1 A central extension acting on the structures
For a,a'\in C_F, define an edge vector
On the set H=C_F\times K, define
Bilinearity gives B(a,a')+B(a+a',a'')=B(a',a'')+B(a,a'+a''), proving associativity. The identity is (0,0); since B(a,a)=0, the inverse of (a,k) is (-a,-k). Thus H is a finite group. The subgroup \{0\}\times K, identified with K, is central, and the projection H\to C_F is a surjective homomorphism with kernel K. With the convention [h,h']=hh'h^{-1}(h')^{-1}, its commutator is
Recall that an edge atom on e has a state (u,z) in P_e, with u=(u_f)_{f\in F(e)}. The element (a,k)\in H sends that state to
It acts on a configuration by applying this map to every incident edge state. This is an action because restricting (a,k) to an edge is a homomorphism from H to P_e, and the edge action is left multiplication.
Lemma 6. For every b\in\mathbb F^V, the action just defined is by automorphisms of A_b. On its central subgroup K, the action adds k_e to each edge coordinate z_e and leaves all face coordinates unchanged.
Proof. At a vertex v, the two incident coordinates belonging to a face f are equal before the action and both receive the same addition a_f. Hence the face compatibility equations remain true. The change in the divergence of a configuration is
Here u_f is the common face coordinate in that configuration. Both terms vanish: k\in K and \partial c^f=0. Configurations therefore remain in the same vertex block and still have divergence b_v. Applying the inverse group element proves bijectivity.
The relations \mathsf{Ed},\mathsf{Cf},\mathsf{EB},\mathsf{VB} are preserved because types and blocks are preserved. The incidence relation \mathsf I is preserved because configurations and their specified edge neighbors are transformed by the same map. Finally, for edge states g,g'\in P_e and h\in P_e, one has (hg)^{-1}(hg')=g^{-1}g'. Consequently every \mathsf Z_\delta is preserved. The formula for the central action follows from (12) with a=0.
Every permutation of the atoms extends to hereditarily finite objects by h\cdot x=\{h\cdot y:y\in x\} for sets x, recursively in their rank. Atoms remain distinct from sets. We always use this extension of the H-action. A tuple \alpha of atoms is a K-support of an object x if every element of the pointwise stabilizer
fixes x. The empty tuple is permitted and has stabilizer K.
3.2 A sparse representative for an edge functional
A central element k\in K fixes an edge atom on e exactly when k_e=0. To obtain a short support for an object x, it suffices to find a small edge set T such that every k\in K vanishing on T fixes x. The stabilizer of x in K is a vector subspace, so it can be described by linear equations on K. We will represent these equations using few edge coordinates.
An edge cochain is a vector \ell\in\mathbb F^E. Its face curl is
A vertex function \varphi\in\mathbb F^V has gradient \partial^{\mathsf T}\varphi, whose value on an edge from v to w is \varphi(w)-\varphi(v). Adding a gradient does not change the curl, because \partial c^f=0. It also does not change the linear functional k\mapsto\sum_e\ell_e k_e on K. The next lemma shows that a cochain with few nonzero face curls can be replaced by one using few edges, without changing its functional on K. In the support proof, commutators will supply the bound on the number of these faces.
Lemma 7 (Sparse cochains). Let \ell\in\mathbb F^E have nonzero curl on exactly t faces of the L\times L\times L box. There is a vertex function \varphi such that r=\ell-\partial^{\mathsf T}\varphi is supported on at most 2Lt edges. In particular, if t=0, then \ell is a gradient.
Proof. We construct the subtracted gradient by successive prefix sums. Write a vertex as (i,j,k). The cochain coordinate \ell_1(i,j,k) is on the edge from (i,j,k) to (i+1,j,k), and similarly for directions 2 and 3. Define
with an empty sum interpreted as zero. Subtracting its gradient produces a cochain r^{(1)} whose direction-1 coordinates vanish. Thus
Here a subscript ab denotes a face in coordinate directions a<b, and the lower corner ranges over the indices for which the face exists.
Let t_{ab} be the number of nonzero ab curls. The L slices of fixed first coordinate partition the 23 faces, so choose i_0 for which the number t_0 of nonzero 23 curls satisfies t_0\le t_{23}/L. Put
The function \varphi_2 is independent of i. Consequently r^{(2)}_1=0, and r^{(2)}_2(i_0,j,k)=0. Next put
This last function is independent of i,j. We have
On the slice i=i_0, the 23 curl identity now reads
It follows that a nonzero value of r_3 on this slice must lie after a nonzero curl on its j-line. Each nonzero curl accounts for at most L positions. The slice therefore contains at most Lt_0 nonzero edge coordinates; its direction-2 coordinates are all zero. Extending these slice values constantly across all L slices uses at most L^2t_0\le Lt_{23} supported coordinates.
The difference between r_2(i,j,k) and r_2(i_0,j,k) is a signed sum of the 12 curls between i_0 and i. Each nonzero 12 curl can occur in at most L of these sums. Thus at most Lt_{12} direction-2 coordinates differ from their copied slice values. The identical argument in direction 3 gives at most Lt_{13} differing coordinates. Since direction 1 is zero, the support of r has size at most
The total subtracted function is \varphi=\varphi_1+\varphi_2+\varphi_3. This construction also covers t=0, when the resulting support is empty.
3.3 The support bound
Proposition 8 (Small-orbit support bound). Let N=|A_b|, let q\ge0, and let x be a hereditarily finite object over the atoms of A_b. If its H-orbit has size at most N^q, then x has a K-support consisting of at most
edge atoms. The support may be empty.
Proof. Let S=\{h\in H:h\cdot x=x\}, let U\le C_F be the image of S under the projection, and put K_0=S\cap K. Since C_F and K are additive groups over the prime field \mathbb F_3, both U and K_0 are vector subspaces. We use the group exact sequence with kernel K_0 to obtain |S|=|U|\,|K_0|. Therefore, with a=\operatorname{codim}_{C_F}U and d=\operatorname{codim}_K K_0,
Let W\le K^* be the annihilator of K_0, so \dim W=d. Every \lambda\in K^* extends to a functional on \mathbb F^E, represented by an edge cochain \ell. Two such cochains differ by an element of K^\perp=\operatorname{im}\partial^{\mathsf T}. Indeed that image is contained in K^\perp, and both have dimension \operatorname{rank}\partial.
Fix \lambda\in W and a representative \ell. For u,u'\in U, choose lifts in S. Their commutator lies in S\cap K=K_0; evaluating \lambda on (11) gives
Thus U is totally isotropic for the alternating form on C_F with one block (D\ell)(f)\omega for each face. If t of these coefficients are nonzero, the form has rank 2t: a nonzero scalar multiple of \omega has rank two, and the blocks have disjoint face coordinates in C_F. This rank calculation does not require the boundary vectors c^f in K to be linearly independent.
We recall the standard dimension argument for alternating forms [5, Sections 3.1 and 3.3]. An alternating form of rank 2t on an n-dimensional vector space has no totally isotropic subspace of codimension less than t. Quotient by the radical, of dimension n-2t. The image of an isotropic subspace in this nondegenerate 2t-dimensional space has dimension at most t, since it is contained in its orthogonal complement. The original isotropic subspace therefore has dimension at most (n-2t)+t=n-t. Applied above, this shows t\le a. By Lemma 7, \lambda consequently has a cochain representative supported on at most 2La edges.
Choose such representatives for a basis of W, and let T\subseteq E be the union of their supports. Then
This includes d=0, when the basis and T are empty. Any k\in K that vanishes on T annihilates every basis member of W, hence all of W. Finite-dimensional duality gives k\in K_0, so k fixes x. For each edge e\in T, choose one edge atom. By the central action, fixing that atom is equivalent to k_e=0. The tuple of chosen atoms is therefore a K-support of x and has the stated length.
The argument used x only through its stabilizer subgroup S\le H. Its rank plays no role in the support bound.
A family \mathcal X is membership-transitive if y\in x\in\mathcal X implies y\in\mathcal X. Thus it contains every recursive constituent of each of its members.
Corollary 9. Let \mathcal X be an H-invariant, membership-transitive finite family of hereditarily finite objects over A_b, and suppose |\mathcal X|\le N^q for some fixed q\ge0. Every object in \mathcal X, including every recursive constituent of each of its members, has a K-support of length at most 2L(q\log_3N)^2. All these supports can be padded to the common positive length
Proof. The orbit of each member is contained in \mathcal X, so the proposition applies to it. Membership transitivity places all its recursive constituents in the same family. Adding atom coordinates to a support can only shrink its pointwise stabilizer, so it remains a support. There are atoms because L\ge2; arbitrary atoms can therefore pad even an empty support. Finally N=\Theta(L^3) gives the asymptotic estimate.
4 Counting equivalence and homogeneity
The central subgroup K=\ker\partial acts by adding a divergence-free edge vector to the last coordinates of the atoms. We now prove two facts about this action. First, a bounded number of variables cannot distinguish the two charge assignments. Second, within either structure, equality of sufficiently wide counting types determines a K-orbit. The second fact will let us transport the supports of hereditarily finite sets.
4.1 An expansion for the analysis
Recall that an edge atom has coordinates (e,u,z), whereas a configuration atom at v specifies the states on all incident edges, subject to the face compatibility equations and the divergence equation with right side b_v. Expand A_b to a structure \bar A_b as follows. Partition its universe into classes indexed by
Here u_f is the common face coordinate on the two edges of f at v. Thus an edge class leaves only z unspecified, and a configuration class leaves all incident z-coordinates unspecified. Choose a linear order of these class labels, the same for all charge assignments, and let \preceq be the resulting total preorder on atoms. Each edge class has size 3, and a configuration class at v has size 3^{d(v)-1}; in particular, corresponding classes are nonempty and have the same size. Finally add, for \delta\in\mathbb F_3, the relation
which is false on every other pair. The vectors u,u' need not agree in this definition. The preorder will let counting formulas identify a block and its face coordinates. The relations \mathsf D_\delta will compare scalar differences on the same edge, including between different face patterns.
Every element of K preserves the expansion. The larger group H need not preserve it. Crucially, the preorder and the relations \mathsf D_\delta are tools for this proof and are not part of the input to a choiceless program.
Write C^h for first-order logic with equality, ordinary quantifiers and exact counting quantifiers \exists^{=a}x, using at most h variable names. Here a may be any nonnegative integer. Formula length and these integer constants need not be uniform in L. The C^h-type of an r-tuple, for r\le h, records all such formulas with free variables among its r designated positions. Coordinates of a tuple may repeat.
4.2 A component that survives edge deletions
Let G be the undirected graph underlying the oriented box grid on V=\{0,\ldots,L-1\}^3. For R\subseteq V, write \delta_G R for its edge boundary; this notation distinguishes the boundary of a vertex set from the incidence operator \partial. The projection estimate below is the three-dimensional discrete LoomisâWhitney inequality [18]. We include its short proof and derive the needed finite-box boundary bound.
Lemma 10 (Boundary of a box subset). Set c=1-2^{-1/3}>0. If \varnothing\ne R\subseteq V and |R|\le L^3/2, then
Proof. Let a_{ij},b_{ik},d_{jk} be the indicators of the three coordinate-pair projections of R. If their sizes are A,B,D, respectively, then
For the last inequality apply CauchyâSchwarz to each inner sum and then sum the product (\sum_k b_{ik}^2)(\sum_k d_{jk}^2) over i,j. Consequently at least one projection has size at least |R|^{2/3}. It indexes that many nonempty coordinate lines meeting R. At most |R|/L of these lines lie wholly in R. Every remaining line is a path meeting both R and its complement, so contains a boundary edge; different lines give different edges. Since
the stated estimate follows.
Set
For all sufficiently large L, deleting any set T of at most 6M edges leaves a unique component containing more than L^3/2 vertices. Call it the giant component. Indeed, summing the preceding lemma over all components R of size at most L^3/2 gives
The middle inequality uses \sum_R|\delta_G R|\le2|T| and \sum_i a_i^{3/2}\le(\sum_i a_i)^{3/2} for nonnegative a_i. If every component had size at most half, the left side would equal L^3, a contradiction. Two components cannot both have more than half the vertices. Moreover, whenever more edges are deleted within this range, the new giant is contained in the old one: each new component is contained in an old component, and its size identifies that old component as the giant.
4.3 Moving the unmatched charge
The counting argument follows the finite-variable counting-game method of Immerman and Lander [16, Counting Quantifiers] and the charge-moving strategy of the CFI construction [4, Lemma 6.2 and proof of Theorem 6.4]. Here we construct the required bijections and prove formula preservation directly; no game characterization is needed as a premise.
Proposition 11 (Base counting equivalence). For all sufficiently large L, the expansions \bar A_{b^0} and \bar A_{b^1}, where b^0=0 and b^1=\mathbf1_{v_*}, satisfy the same C^M sentences.
Proof. An assigned edge atom touches its edge, and an assigned configuration atom at v touches all edges incident with v. At most M assigned positions therefore touch a set T of at most 6M edges. Call a paired assignment compatible if some vector t\in\mathbb F_3^E and some vertex w in the giant of G\setminus T satisfy
and each assigned atom is paired with the atom obtained by adding t_e to its last coordinate on every relevant edge. This operation leaves its block and all face-vector coordinates unchanged. The empty assignment is compatible with t=0 and w=v_*.
A compatible assignment preserves every atomic formula. On a fixed edge, common addition of t_e preserves both raw differences and the corrected differences defining \mathsf Z_\delta. It also preserves whether an edge state is the specified neighbor of a configuration. The block relations, preorder, diagonal predicates and equality are preserved as well. This applies even when assigned coordinates repeat.
Deleting an assigned position preserves compatibility: the set of touched edges shrinks, and the old giant is contained in the new one. Suppose now that at most M-1 positions remain. We construct one bijection of the entire universes that extends them, regardless of which atom is next assigned. Its definition may use a different shift on each block; every such shift will agree with t on the retained touched edges. Partition the universe into whole edge blocks and whole vertex configuration blocks. For such a block J, let T_J be T together with its edge, or with its vertex star, as appropriate. There are at most 6M edges in T_J. Choose w_J in the giant of G\setminus T_J. Both w and w_J lie in the giant of G\setminus T, so they are joined by a path there. A signed path vector p_J, supported outside T, can be chosen with
Put t_J=t+p_J. It agrees with t on every previously touched edge and satisfies (16) with w_J in place of w.
Map every atom in J by its t_J-shift. This gives a bijection on an edge block. For a configuration block at v, deleting the star isolates v, so v\ne w_J. Hence (\partial t_J)_v=b^1_v-b^0_v, exactly the condition for translation to map its configurations bijectively to those in the other structure; the face-vector constraints are unchanged. The union of these block bijections is a bijection of universes. For a new atom in block J, both it and all retained positions are paired by the single shift t_J. Thus adjoining that atom extends the compatible assignment, with witness t_J,w_J.
Induct on formulas. Atomic formulas were handled above, and Boolean operations preserve agreement. At a quantifier, first discard any old assignment of its variable, leaving at most M-1 positions. The bijection just constructed pairs all extensions on which the body has the same truth value by induction. It therefore preserves ordinary quantification and every exact counting quantifier, including count zero. Starting from the empty assignment proves the proposition.
4.4 Recognizing the central-group orbits
For the next step, the two tuples lie in the same expansion. A shift prescribed on their touched edges must extend to a divergence-free vector. The only obstruction is a nonzero net prescribed flow across one of the remaining components.
Lemma 12 (Extending a partial flow). Let T\subseteq E and \sigma\in\mathbb F_3^T. There is k\in\ker\partial with k|_T=\sigma if and only if, for every component U of G\setminus T,
If an extension does not exist, there is a nonempty failing component with
Proof. Extend \sigma by zero outside T. The required values on E\setminus T must have divergence -\partial\sigma. On any connected graph, the image of its incidence operator is exactly the vertex vectors with zero sum. To see sufficiency without a rank calculation, take a spanning tree, set nontree edge values to zero, and eliminate leaves: the divergence at a leaf uniquely determines the value on its tree edge. The prescribed total sum makes the final root equation hold. Apply this separately to each component, allowing an isolated vertex as a one-vertex tree. The necessary zero-sum conditions are precisely (17).
The sum of all R_U is zero, because the two incidence signs of each edge cancel. Thus failure at one component implies failure at at least two, so one failing component has size at most L^3/2. Its boundary is contained in T, and Lemma 10 gives the second estimate.
Proposition 13 (Quantitative homogeneity). Let r\ge1, and suppose
If two r-tuples in the same \bar A_b have equal C^M-types, then some k\in K maps the first tuple to the second. The corresponding statement for empty tuples holds without any width hypothesis.
Proof. Write the tuples as \bar a,\bar a'. Each preorder class is definable using two variable names. If h is the number of atoms in strictly earlier classes, its predicate is
Different classes give different h, since every class is nonempty. Type equality therefore puts corresponding tuple coordinates in the same class. They have the same blocks and face-vector patterns.
Let T be the touched edges, so |T|\le6r. An occurrence of a state on e\in T is either an edge atom appearing in a tuple coordinate or the state on e in a configuration appearing there. In the latter case that state is the unique y satisfying \mathsf I(a_i,y) and its specified edge-class predicate. The corresponding occurrence for \bar a' has the same edge and face-vector coordinates. For any two occurrences on one edge, their raw difference can be tested by \mathsf D_\delta, quantifying their uniquely specified neighbors if necessary. These tests use at most the r tuple names, two neighbor names, and one name reused in class-counting predicates. Condition (18) in particular permits these r+3 names. Type equality shows that every pair of corresponding occurrences has the same raw difference. Hence there is a single well-defined \sigma_e equal to the change in z from \bar a to \bar a' for all occurrences on e.
Suppose \sigma cannot be extended to K. Choose a failing component U from Lemma 12; then
We construct a formula true at \bar a and false at \bar a'. For every v\in U, choose any configuration g_v^0 in the first assignmentâs structure and let h_{v,e}^0 be its neighbor on every incident edge. The chosen configurations need not agree across an internal edge. The formula will preserve their original raw difference, so any new witnesses will have equal scalar changes at its two ends. These changes will cancel when the divergence equations are summed over U. On each boundary edge e\in\delta_GU\subseteq T, choose one occurrence from \bar a, and denote its state by o_e^0. Write o_e for the corresponding tuple variable, or the auxiliary neighbor variable when one is needed. The formula existentially quantifies variables g_v,h_{v,e}, and, if the chosen occurrence comes from a tuple configuration, one neighbor variable y_e. Its conjunction asserts:
- 1.
each g_v,h_{v,e} is in the class of the chosen atom, and \mathsf I(g_v,h_{v,e}) holds;
- 2.
for every edge internal to U, the raw difference between its two variables h_{v,e} equals the difference between the two chosen atoms h_{v,e}^0;
- 3.
for every boundary edge, the raw difference between h_{v,e} and its chosen tuple occurrence equals their original raw difference; if that occurrence requires y_e, also impose its edge-class predicate and its incidence with the relevant tuple configuration.
For definiteness, on an internal edge joining v,w, choose an ordering of its endpoints and use
on a boundary edge incident with v\in U, use
where both atoms in the subscript are the fixed original choices. Thus o_e=y_e in the arguments when the occurrence is supplied by a tuple configuration. An edge in T with both endpoints in U is treated as internal; its contribution to R_U cancels and requires no boundary link. All class predicates are of the form \theta_h above, and all difference conditions use one of the three \mathsf D_\delta. This describes a finite formula in the expansionâs vocabulary; the numerical constants and its length may depend on the chosen assignments. The indicated choices witness its truth at \bar a.
If it were true at \bar a', compare the realized z-coordinates of its witnesses with those of h_{v,e}^0, writing the changes as d_{v,e}. Both configurations at v have divergence b_v, so \sum_{e\ni v}\epsilon_{ve}d_{v,e}=0. On an internal edge the difference constraint gives equal changes at its two ends. On a boundary edge it forces d_{v,e}=\sigma_e. Summing the vertex equations over U therefore gives R_U=0, contrary to the choice of U.
There are r tuple variables, |U| configuration variables, at most 6|U| incident-state variables, and at most |\delta_GU|\le6r extra occurrence variables. One further name can be reused in every class predicate. Thus the formula uses at most
names, contradicting type equality. The partial shift therefore extends to some k\in K, whose action maps every coordinate of \bar a to the corresponding coordinate of \bar a'. For empty tuples take k=0.
For the support scale used below, fix q,m first and put
Uniformly for 1\le r\le\max\{2,m\}s, the left side of (18) is
Consequently Proposition 13 applies throughout that range when L is sufficiently large. The same choice of L ensures \max\{4,m+1\}s\le M, the separate width requirement for extending atom types in the hereditary-set comparison below. The exponent 7/4 simultaneously ensures M^{3/2}=o(L^3) for the giant-component estimate and L^{3/2}(1+\log L)^3=o(M) for homogeneity at the support scale. Any fixed exponent strictly between 3/2 and 2 would meet these asymptotic requirements. All these conclusions hold for fixed q,m, chosen before L.
5 From atom types to hereditarily finite sets
The preceding counting equivalence concerns tuples of input atoms. A choiceless computation also constructs sets of atoms, sets of such sets, and objects of unbounded finite rank. We now show how small supports let us transfer bounded-variable counting formulas on a domain containing all these objects. The domain itself will be countably infinite; every object in it is nevertheless hereditarily finite. The counting argument below respects this distinction. The support, molecule and form method originates in Blass, Gurevich and Shelah [2, Sections 8â9 of the published version] and was developed for counting by Dawar, Richerby and Rossman [9, Section 8 of the author version]. We give the full quantitative argument for the chosen automorphism subgroups and support bound used here, including exact counts of represented values.
We first isolate the precise hypotheses needed from the preceding sections. Write \mathrm{HF}(A) for the atoms of A together with all hereditarily finite sets built from them. For a finite relational structure A, let \operatorname{tp}_M^A(\bar a) be the set of all C^M formulas true at \bar a, with free variables among the indicated tuple positions. Tuples may have repeated entries. Two such types are compared using the same ordered list of variable positions.
Theorem 14 (Transfer through small supports). Let A_0,A_1 be nonempty finite structures in the same binary relational vocabulary, and let K_i\leq\operatorname{Aut}(A_i) for i\in\{0,1\}. Let s,m,M be positive integers satisfying
Assume the following two properties.
- 1.
A_0 and A_1 satisfy the same C^M sentences.
- 2.
In each A_i, any two tuples of length at most \max\{2,m\}s with the same C^M type lie in the same K_i orbit.
For i\in\{0,1\}, let D_i consist of the objects x in \mathrm{HF}(A_i) such that x and every object in its transitive closure have a K_i-support of length at most s. Equip D_i with membership, an atom predicate, and the relations of A_i, interpreted as false on arguments containing a non-atom. Then D_0 and D_1 satisfy the same C^m sentences.
Here atoms are urelements, distinct from all sets. A tuple supports an object if its pointwise stabilizer fixes that object. The action of K_i on atoms extends recursively to sets. We can pad every support to exactly s coordinates, using repetitions or arbitrary atoms, because A_i is nonempty. The resulting domains D_i contain all atoms and all pure hereditarily finite sets. They are transitive under membership, countable, and invariant under K_i: if \alpha supports x, then g\alpha supports gx.
For our application, A_i in Theorem 14 is the analytic expansion \bar A_{b^i}, and K_i is its central flow group K. The base counting-equivalence and homogeneity results provide its two assumptions with the parameter bounds established at the end of Section 4. For the remainder of the paper, write \mathcal D_{b^i} for this supported domain over \bar A_{b^i}, using the support length in (14). The atom predicate is definable in our domain by \mathsf{Ed}(x,x)\lor\mathsf{Cf}(x,x). No analytic expansion is supplied to the program; it is used only to prove the indistinguishability theorem.
The proof has three stages: count extensions of atom types; represent supported objects and transfer equality and membership; then match the whole domains while retaining the assigned parameters.
5.1 Exact extension counts for atom types
All types in the next lemma are realized in A_0 or A_1. Thus there are only finitely many types of any fixed tuple length, even though a type records infinitely many formulas.
Lemma 15 (Extension counts). Suppose P and P' have the same C^M type in two structures chosen, with repetition allowed, from A_0,A_1. If |P|+d\leq M, then for every realized type \rho of length |P|+d, the numbers of tuples \gamma and \gamma' satisfying
are equal. In particular a type realized over one prefix is realized over the other. Equal types also have equal types on every projected or reordered subtuple.
Proof. Projection and reordering follow by renaming the free tuple variables: an injection between the selected position sets extends to a permutation of the M available variable names. Repeated atom values cause no problem; positions remain distinct, and equality formulas record all coincidences of values.
First let d=1 and write a=|P|. A realized type \rho of (a+1)-tuples can be isolated among the tuples of both finite structures by a single C^M formula \theta_\rho. Indeed, choose a representative of \rho. For every tuple in the two structures whose type differs from \rho, choose a formula distinguishing it from the representative, negating the formula if necessary. The conjunction of this finite collection is true exactly on the tuples of type \rho. Its free variables lie among the first a+1 positions, and it still uses only the same M variable names. If all tuples have type \rho, use a tautology.
If exactly h extensions of P realize \rho, the formula
is true at P. Equality of prefix types makes it true at P' as well. This proves the one-coordinate assertion, including h=0 and a=0. For empty prefixes in different structures, the required equality of types is precisely their agreement on C^M sentences.
For d>1, project \rho onto the first a+d-1 positions, obtaining \sigma. By induction the number of extensions of P to type \sigma equals the corresponding number over P'. The one-coordinate argument, used both within a structure and between the two structures, shows that every tuple of type \sigma has the same number of last-coordinate extensions to type \rho. Multiplying these two finite counts proves the assertion.
5.2 A common syntax for supported objects
A molecule is a tuple \alpha\in A_i^s. It records a support, but need not be a minimal support. We describe sets by a common collection of formal expressions, independent of the side i.
There are s atomic forms c_1,\ldots,c_s. A set form is a finite set of pairs (\psi,\rho), where \psi is a previously constructed form and \rho is a realized C^M type of length 2s in A_0 or A_1. These are syntactic constructors: atomic forms are distinct from every set form, including the empty set form. A form has finite depth; set forms have greater depth than their constituent forms.
For a molecule \alpha\in A_i^s, define the value of a form recursively:
This produces a finite set because both the form and the base universe are finite. The empty set form evaluates to the empty set.
Lemma 16 (Representation). Every value \phi*\alpha belongs to D_i and is supported by \alpha. Conversely, every object of D_i has such a representation. Moreover, for every g\in K_i,
Proof. Automorphisms preserve C^M types. Induction on the form therefore gives the displayed equivariance identity: in the set case, change the witness molecule \beta to g\beta in (20). If g fixes \alpha, this identity says that it fixes \phi*\alpha. Induction also puts every member of a set-form value, and all of that memberâs recursive constituents, in D_i. Atomic values have the required support directly.
For the converse, induct on the hereditary rank of the object. An atom has the form c_j*\alpha for a molecule containing it. Let x be a set in D_i, and choose a supporting molecule \alpha. For each y\in x, the induction hypothesis gives y=\psi_y*\beta_y. Form the finite set
Every member of x lies in \phi*\alpha. Conversely, a member of \phi*\alpha has the form \psi_y*\beta, where (\beta,\alpha) and (\beta_y,\alpha) have the same type. Homogeneity for tuples of length 2s supplies an element g\in K_i mapping the second tuple to the first. In particular g fixes \alpha, so it fixes x. Equivariance gives \psi_y*\beta=gy\in x. Thus x=\phi*\alpha. For x=\varnothing, the construction gives the empty set form and the same conclusion.
Representation reduces arbitrary finite rank to finite syntax. We next show that the syntax can be evaluated on either base structure without changing equality or membership, provided the supporting molecules have the same joint type.
Lemma 17 (Transfer of atomic facts). Let \phi,\psi be forms. Suppose (\alpha,\beta) and (\alpha',\beta') have the same C^M type, where the two tuples may be in the same base structure or in different base structures. Then
The atom predicate and all base relations also agree on corresponding form values.
Proof. For equality, induct on the sum of the depths of the two forms. For two atomic forms, equality is an equality of molecule coordinates and is recorded by their joint type. An atomic value never equals a set-form value. It remains to compare two set forms.
Suppose \phi*\alpha=\psi*\beta. Take a member of \phi*\alpha' and a witness for it, say (\theta,\rho)\in\phi and \gamma' with \operatorname{tp}_M(\gamma',\alpha')=\rho. Lemma 15 extends the matching prefix (\alpha,\beta) to a tuple (\alpha,\beta,\gamma) with the type of (\alpha',\beta',\gamma'). Hence \theta*\gamma is a member of \phi*\alpha, and therefore of \psi*\beta. Choose a witness (\xi,\sigma)\in\psi and a molecule \zeta such that
Apply the extension lemma once more, this time to the primed prefix of length 3s, to obtain \zeta' such that
This is the step requiring 4s\leq M. Projection preserves the two member-witness types. The induction hypothesis applies to \theta,\xi, whose depths are strictly smaller than those of \phi,\psi, and gives \theta*\gamma'=\xi*\zeta'. Thus the chosen member belongs to \psi*\beta'. Interchanging \phi and \psi proves the reverse inclusion. Finally interchange primed and unprimed data to prove both directions of equality transfer. The argument includes empty set forms: when there is no member to choose, the relevant inclusion is vacuous.
For membership, the right-hand value is either an atom, in which case membership is false on both sides, or the value of a set form. In the latter case, a member witness \theta*\gamma equal to \phi*\alpha can be transferred over the prefix (\alpha,\beta) using 3s positions. Equality transfer, already established for all forms, then transfers the witness. Interchanging sides proves the converse.
A form is atomic on both sides or a set form on both sides. Consequently the atom predicate transfers. A base relation is false if any argument is a set; otherwise it is a relation on selected molecule coordinates, and its truth is part of their joint base type. Repeated arguments are allowed throughout.
5.3 Matching entire domains while retaining parameters
An object may have several representations \phi*\alpha. Thus equal counts of molecules do not by themselves give equal counts of objects. We will group represented values into stabilizer orbits and account for the number of molecules representing each value. This will give a bijection between the two domains after fixing the values of at most m-1 variables. The construction is a mathematical comparison; it is not required to be definable or executable by a choiceless program.
Call paired assignments represented alike if their values have representations
using common forms, and the concatenated tuples P=(\alpha_1,\ldots,\alpha_r) and P'=(\alpha'_1,\ldots,\alpha'_r) have the same C^M type. Dropping a position preserves this condition by projection. Empty assignments are represented alike by the sentence-equivalence assumption.
Lemma 18 (A bijection extending retained assignments). For any represented-alike assignments with r\leq m-1, there is a bijection f:D_0\longrightarrow D_1 such that adjoining any pair x,f(x) gives represented-alike assignments. In particular f(x_j)=x'_j for every retained position.
Proof. Fix representing tuples P,P'. A label is a pair (\phi,\tau), where \phi is a form and \tau is a realized base type of length (r+1)s. Associate to it the finite value sets
and X_{\phi,\tau}(P') on the other side. The extension-count lemma shows that the two sets are either both empty or both nonempty.
Every nonempty value set is a single orbit of the stabilizer K_{0,P}. Indeed, any two molecules with the specified type over P are carried to one another by an element fixing P, using homogeneity for (r+1)s\leq ms positions. Equivariance carries their values along with them. Conversely, an element fixing P preserves the specified joint type, and thus preserves the value set. The same assertion holds on the other side. It follows that two nonempty label sets on one side either coincide or are disjoint.
Whether two labels overlap is the same on both sides. If an overlap has witnesses \gamma,\zeta on the first side, extend P' to match the type of (P,\gamma,\zeta). This uses
Projection preserves the two label conditions, and Lemma 17 preserves equality of the two values. Hence the label sets overlap on the second side. The converse is symmetric.
We also need equality of the sizes of corresponding label sets. Fix a nonempty label. The number n of molecules of its type over P equals the number over P', by Lemma 15. The map \gamma\mapsto\phi*\gamma from these molecules onto the label set has fibres of a common positive size: the stabilizer acts transitively on the molecules, and equivariance maps one fibre bijectively to another. Choose molecules \gamma,\gamma' whose joint types with the two prefixes match. The fibre at \phi*\gamma has size
Partition the possible \zeta by the finitely many realized types of (P,\gamma,\zeta). On each such type the two displayed conditions are constant, both within either structure and between structures: use projection for the first condition and equality transfer for the second. Each type has the same number of extensions over (P,\gamma) and (P',\gamma'), again using (r+2)s\leq M. Summing these finite counts shows that the fibre size h agrees on the two sides. Both value sets therefore have size n/h.
Representation shows that the label sets cover the domains. Their nonempty labels have the same equivalence relation on both sides, where two labels are equivalent when their value sets overlap. For each class, the common value set on the first side and the common value set on the second side are finite and have equal size. Choose a bijection between them. These bijections combine to a bijection f:D_0\to D_1, because different classes give disjoint value sets.
There are only countably many labels: the base type sets are finite and the forms are finite expressions over them. No effective choice is being assumed here. For example, fix external enumerations of the two countable HF universes and of the labels; take the first label of each class and match its finite value sets in their external enumeration orders. These orders belong only to the proof.
If f pairs x with x', a representative label (\phi,\tau) of their class gives molecules \gamma,\gamma' with x=\phi*\gamma, x'=\phi*\gamma' and common joint type \tau over P,P'. Thus the extended assignments are represented alike. If x=x_j for a retained position, equality transfer forces x'=x'_j. This proves the last assertion as well.
Proof of Theorem 14. We prove by induction on C^m formulas that represented-alike assignments agree on their truth values. Equality, membership, the atom predicate, and the input relations agree by Lemma 17; for atomic formulas using two distinct variables, project onto their two representing molecule blocks. With one repeated variable, equality is true and self-membership is false in \mathrm{HF}; a diagonal base relation is false on a set and otherwise is determined by the corresponding atom coordinate in its molecule type. Boolean connectives preserve agreement.
Consider a quantifier binding a variable x. Retain the assigned values of the other variable names, dropping the old value of x if there is one. At most m-1 positions remain. Lemma 18 gives a bijection of the domains under which every extension by x is again represented alike. The induction hypothesis therefore makes this a bijection between the sets of values satisfying the quantified body. Existential truth agrees, and for every natural number h the statement that this set has exactly h elements agrees. This proves the counting step even if that set is infinite: a bijection preserves finiteness and every finite cardinality. Universal quantifiers follow in the same way or by negation. Empty assignments are represented alike, so all C^m sentences have the same truth value.
Theorem 14 imposes no bound on the rank of an object or the depth of its representing form. The type-extension arguments require 4s\leq M for equality transfer and (m+1)s\leq M for the domain bijections. Orbit homogeneity is used at length 2s for representation and at length at most ms when extending a retained assignment. These requirements are independent of rank. In the next section, the support theorem places every code and recursive constituent of a polynomial computation inside D_i. We then construct bounded-variable halt and output sentences evaluated on D_i, to which the transfer theorem applies.
6 Encoding complete choiceless computations
The preceding transfer theorem concerns hereditarily finite sets with small supports. We now bring an arbitrary fixed choiceless computation into that setting. There are two separate points to prove: all constituents of its encoding lie in a polynomial-size invariant family, and its states can be defined by counting formulas whose number of variable names stays bounded throughout the computation. For our two inputs, which have the same size, this will give one common C^m sentence for each stageâs halt test and output test, exact on their supported domains through the respective halt stages, with m depending only on the program.
6.1 The interpretation characterization
We use the binary-vocabulary formulation of the interpretation characterization of choiceless polynomial time with counting, due to Grohe, Schweitzer and Wiebking [12, Section 6 and Theorem 18, arXiv version 1], building on Grädel, Pakusa, SchalthÜfer and Kaiser [11, Theorem 1]. Here counting includes the cardinality operation on hereditarily finite sets. We spell out the exact direction and interpretation convention used below.
An interpretation from one fixed binary relational vocabulary to another consists of fixed, parameter-free formulas
in first-order logic with the Härtig quantifier. This quantifier compares the cardinalities of two sets of elements defined by formulas; the two formulas may have free variables in addition to their respective counted variables. On a finite structure with universe V, the interpretation first forms
Let \sim be the least equivalence relation on D containing every pair (\bar a,\bar b) satisfying \eta(\bar a,\bar b). The new universe is D/{\sim}, and
Thus the interpretation is defined even when \eta itself is not an equivalence relation or \rho_R is not constant on classes. This is the convention in [12].
An interpretation program has one such initialization interpretation, one step interpretation, and fixed halt and output sentences in first-order logic with the Härtig quantifier. Write A_0=A for the input, A_1=I_{\rm init}(A_0), and A_{j+1}=I_{\rm step}(A_j) for j\ge1. The halt sentence is first tested at A_1. A deciding program halts at a stage h\ge1, outputs the truth value of its output sentence there, and has
bounded by a fixed polynomial in |V(A)|. The characterization says, in the direction needed here, that every property of finite binary relational structures definable in full choiceless polynomial time with counting is decided by such a program. The absence of parameters means that the fixed interpretations have no additional input-dependent distinguished tuple; it does not prohibit free tuple variables in their defining formulas.
Fix a deciding interpretation program P. On our two inputs of the same size N, choose a common integer B\ge2 bounding N, both halt stages, and every state size up to halt. We may take B to be a fixed polynomial bound depending only on P.
6.2 A polynomial hereditary encoding
For objects a,b in the universe of hereditarily finite sets over the input atoms, use the Kuratowski pair
This coding is injective in the ordered pair, including when a or b is an atom. Indeed the intersection of its members is \{a\}, while their union is \{a,b\}; after recovering a, the latter set determines b, also when a=b.
Encode the vertices of A_0 by the input atoms themselves. Suppose the vertices of A_{j-1} have already been encoded injectively. A vertex C of A_j is an equivalence class of domain pairs from A_{j-1}. Define its payload and code by
where [j]=\{[0],\ldots,[j-1]\} is the von Neumann ordinal. Distinct classes have disjoint, nonempty sets of representing pairs, so their payloads, and hence their codes, are distinct. The payload records the whole class, so its construction does not choose a representative. The ordinal tag distinguishes vertices created at different stages, and stage-zero codes are atoms rather than sets.
Lemma 19. For either input, the input atoms, all vertex codes up to halt, and all objects recursively occurring as members of those codes belong to an H-invariant transitive family of at most 9B^3 objects.
Proof. At a single stage there are at most B^2 domain pairs. For each pair, its Kuratowski code and its two inner sets add at most three objects. There are at most B classes; their payloads add at most B objects, and the tagged vertex pairs add at most 3B further objects. Previous vertex codes and their constituents have already been counted. Across all stages, the ordinal tags and their constituents add at most B+1 objects. Including the at most B input atoms, the total is at most
for B\ge2. Taking the recursive membership closure therefore gives the stated transitive family.
Every input automorphism preserves truth of the fixed interpretation formulas, including the Härtig quantifier. It therefore permutes the domain pairs, their generated equivalence classes, and all output relations. Inductively it permutes the vertex codes: it acts on a pair or set by acting on its constituents, and fixes every pure ordinal. It consequently preserves the family and its membership closure. In particular the input action of H preserves this family.
Since B is polynomial in N, fix an integer q\ge1, depending only on P, such that 9B^3\le N^q for all sufficiently large N. Every H-orbit in the transitive trace family has at most N^q objects. Corollary 9 therefore gives K-supports of the common length s for every code and every recursive constituent. Thus the entire family lies in the corresponding supported domain \mathcal D_b, including the payloads, all pair wrappers, and the ordinal tags. No bound on the rank of a code has been imposed: its nesting depth may grow throughout the computation.
6.3 Exact formulas for the encoded states
All formulas in this subsection are evaluated in \mathcal D_b with its membership relation and its atomic input relations. Its domain is transitive, contains all input atoms and all pure hereditarily finite sets, and consists of atoms and sets. Consequently
distinguish these two kinds of objects.
Let U_0(x)=\mathsf{Atom}(x) and let the stage-zero relation formulas be the input relations. Suppose that the formulas for the preceding stage are exact: U(x) selects precisely its vertex codes, and its relation formulas describe exactly the state on those codes. Translate a fixed first-order formula with Härtig quantifiers by replacing state relation atoms by their defining formulas, retaining equality, and restricting ordinary quantifiers to U. In particular, equality is equality of the injective vertex codes, including for repeated variable arguments. Replace a Härtig comparison of \chi_1(x) and \chi_2(y) by
Both counted sets have size at most B, so induction on formulas proves this translation exact, also when the state is empty. The superscript * will denote this translation.
For the initialization or step interpretation appropriate to the new stage, put
On two domain pairs define
where tuple equality abbreviates the two coordinate equalities. Define finite formulas recursively by
This expresses paths of length at most t+1 in the reflexive symmetric link graph. There are at most B^2 domain pairs, so \mathsf{Reach}_{B^2} is exactly the generated equivalence relation, and is false if either endpoint is outside the domain.
The generated quotient is now defined. We next recognize its hereditary codes; transitivity will ensure that membership tests identify the actual sets, not merely their visible members. Write
and
Then
expresses z=\langle a,b\rangle whenever that pair and its wrappers are present. Conversely every satisfying assignment gives the actual Kuratowski pair: transitivity ensures that the universally quantified membership tests cannot overlook a member outside the domain. Define the ordinal formulas by
The empty disjunction for i=0 is false. All pure ordinals belong to \mathcal D_b, and induction using transitivity shows that this formula selects precisely [i].
For stage j\ge1, define
The stage subscripts on the formulas and on their auxiliary definitions are syntactic indices, not additional free variables.
Lemma 20. At every stage through halt, U_j selects exactly the vertex codes of A_j, and each R_j defines exactly its corresponding binary state relation. The translated halt and output sentences are exact at every stage j\ge1 through halt.
Proof. The assertion at stage zero follows from the definition of the atomic input relations. Assume it for the preceding stage. Formula induction, including (21), makes \mathsf{Dom} and the interpretation formulas exact. The link graph and its bounded path formula therefore give exactly the required classes of domain pairs.
For a domain pair \bar a representing a class C, every pair code belonging to S_C and all its wrappers are in \mathcal D_b, by Lemma 19 and the support theorem. Hence the right side of the payload biconditional selects exactly the elements of S_C. The true payload exists in the domain, while any satisfying payload has exactly those members, since the domain is transitive. Extensionality for sets gives S=S_C. The ordinal and ordered-pair formulas then force x=e_j(C), with all required witnesses present. This proves the exactness of \mathsf{Rep}_j and U_j. If there are no domain pairs, both formulas are false for every candidate vertex, as required.
Finally, R_j holds precisely when some representatives of the two coded classes satisfy the defining relation formula. This is the chosen quotient semantics, so all relations are exact. Applying the same formula translation to the fixed halt and output sentences proves the last assertion.
6.4 A variable bound independent of the number of stages
The formulas just constructed may be extremely long. What matters for the transfer theorem is a different syntactic bound. For a formula \theta, define
Here free variables are counted relative to the subformula \xi itself. Thus a variable bound outside \xi is counted if it occurs freely inside \xi.
Lemma 21. Suppose predicates in a relational formula T are replaced by formulas whose free variables are among their displayed argument variables and whose free-variable measure is at most w. Capture-avoiding substitution produces a formula of free-variable measure at most \max\{\operatorname{fw}(T),w\}. This allows repeated arguments and unused displayed argument variables. Moreover a formula of measure at most w can be renamed to use at most w+1 variable names.
Proof. Before each insertion, rename its bound variables to avoid the argument variables and all possible capture. A subformula inside the inserted copy has the same free variables as its original counterpart, except that displayed argument variables are replaced by their actual variable arguments. This replacement can identify variables but cannot increase their number. A subformula inherited from the template gains no new free variables: the inserted formula has free variables only among the arguments of the atom it replaces. The claimed maximum bound follows. The argument also covers equality atoms, which are retained as equality, and atomic occurrences with repeated arguments.
For the renaming claim, fix a palette of w+1 names. Recursively process a formula node with an injective assignment of palette names to that nodeâs free variables. At a Boolean connective, restrict this assignment to each childâs free variables. At a binder Qx\,\xi, keep the assigned names of the free variables of the parent and choose a name for x outside those names. There is a spare name because there are at most w parent free variables. If x is free in \xi, extend the assignment by this name; otherwise the binder is vacuous and the child keeps the parent assignment. Recursively rename the child. Its free-variable assignment is injective, and its size is at most w. Names may be reused in subtrees where the corresponding variable is not free. This preserves all bindings and truth, and applies equally to ordinary and exact-count quantifiers.
Apply the lemma first to the fixed formulas of P. Replacing a Härtig quantifier by (21) may repeat a subformula B+1 times but does not increase its free-variable sets with B; the finitely many program formulas therefore give a uniform bound for the translation templates. Pair coding, payloads, representatives, and domain and relation definitions also have fixed templates, with all free variables among their displayed arguments.
For example, the template for \mathsf{Reach}_{t+1}(\bar a,\bar b) uses only the endpoint pairs \bar a,\bar b and the quantified pair \bar d. The inserted copy \mathsf{Reach}_t(\bar a,\bar d) exposes only its four endpoint arguments; \bar b occurs in the other conjunct, \mathsf{Link}(\bar d,\bar b), and is not a free parameter of that copy. Thus expansion takes the maximum of the previous width and the fixed template width, rather than adding the widths at successive levels. The same argument applies when a stage formula is inserted into the next stageâs template. The ordinal recursion has the simpler unary interface. Taking the maximum over these finitely many template widths and the bounds for the fixed formulas of P gives a constant w=w(P) for every fully expanded formula above. Unused or identified arguments can only reduce the number of free variables.
Set m=\max\{2,w+1\}. Lemma 21 puts all the expanded state, halt, and output formulas in C^m, independently of N, B, and the stage number. The numerical constants in the counting quantifiers and the lengths of these formulas may depend on B and the stage. These are formulas used to compare two runs; they are not an additional nonuniform program.
7 Proof of the separation
We now combine the invariant query, support bound, counting transfer and exact computation formulas. The constants controlling supports and formula width are fixed by the program before the grid is chosen.
Proof of Theorem 1. The fixed eight-symbol vocabulary and the query Q are given in Section 1.1. Proposition 2 proves that Q is isomorphism-invariant and belongs to deterministic polynomial time. Suppose it were definable in full \CPT with counting. The interpretation characterization in Section 6 would give a fixed deciding interpretation program P.
Choose its polynomial bound B=B(N) and the constant q from the trace bound, and choose the constant m from the syntax. Take L sufficiently large that the trace bound 9B^3\le N^q and the width estimates below hold, and put M=\lfloor L^{7/4}\rfloor. Corollary 9 places both encoded traces in their supported domains with
Proposition 11 gives base C^M equivalence, and Proposition 13 gives homogeneity for tuples of length at most \max\{2,m\}s: its width bound is O_{q,m}(L^{3/2}(1+\log L)^3)=o(L^{7/4}). We also have \max\{4,m+1\}s\le M. These are exactly the hypotheses of Theorem 14, so the two supported domains agree on all C^m sentences.
Use the same B, ordinal indices, and syntactic definitions on both sides. Up to the earlier halt stage both sets of state definitions are exact. At that stage the common translated halt sentence is true on one side, hence also on the other; thus both computations halt there. Their common translated output sentence has the same truth value on both sides. No deciding interpretation program can therefore give opposite answers on the two structures.
This contradicts Proposition 5, which gives Q(A_{b^0}) and \neg Q(A_{b^1}) for every L\ge2. Therefore no such program exists, proving the theorem.
8 Solvability and rank logic
We now prove the linear-algebraic consequence stated in the introduction. The query Q is defined on all finite structures. For Corollary 3 we take a nonempty input, so the matrix index sets below are nonempty. We use the two-sorted syntax of \mathrm{FPS}_3 and \mathrm{FPR}_3 in [10, Section 2]. We first define its matrix without ordering the input, then encode consistency using the respective operators.
Proof of Corollary 3. Write X(a) and Y(a) for the predicates defining X and Y, and put n=\#x(x=x), a closed numeric term. For \delta=1,2, the counting terms
give, for each fixed r\in\{0,1,2\}, the FPC predicate
Here \eta is a number variable. Since d_1+2d_2\leq3n, this says exactly that C(y,a)=r in \mathbb F_3. It includes both contributions when \mathsf Z_1 and \mathsf Z_2 both hold, while \mathsf Z_0 contributes zero. The row test is the first-order predicate
For nonempty A, use the full tuple domain D=A^2\times\{0,1\} for both rows and columns, with the last coordinate in the number sort. For i=(t,y,\rho) and j=(a,z,\kappa), define
Set b_i=\mathbf{1}_{N(i)} and, over \mathbb F_3, set
The tags make these cases disjoint. The diagonal payloads give one column for each \lambda_a and one separately tagged column for each \mu_y, even when X and Y overlap. They also give one normalization row for each t\in X, while the E rows retain every selected pair (t,y). All remaining rows and columns are zero, with right-hand side zero on those rows. Thus Mx=b is exactly the system defining Q, with harmless zero padding. In particular an empty X_t still gives 0=1. The predicates B_r(i,j)\equiv(M_{ij}=r) for r=1,2 are FPC-definable from these cases and C_1,C_2.
The solvability operator uses a Boolean matrix and an all-ones right-hand side; compare the general fixed-ring normal form in [7, Lemma 4.1]. For an explicit encoding here, use full row and column domains D\times\{0,1,2,3\}, with column tags denoting x^1_j,x^2_j,z_j,v_j. For every i\in D, the four row tags encode
All coefficients are zero or one: the two summands for B_2 use distinct columns. Their incidence is one FPC formula using B_1,B_2,N, equality of tuples in D, and the fixed numeric tags. Every row in the full product has one of the four stated types. The last two equations force x^1=x^2; together with v=1, the first equations then say Mx^1=b. Conversely, a solution x of Mx=b extends by x^1=x^2=x, z=1-x, and v=1. Hence one characteristic-three solvability operator defines Q.
For rank, let \mathbf{1}_\psi denote the numeric counting term \#\zeta\leq0.\psi, where \zeta is a number variable, and put m(i,j)=\mathbf{1}_{B_1(i,j)}+2\mathbf{1}_{B_2(i,j)}. On rows D and columns D\times\{0,1\}, with numeric tag h, use the entry terms
The first matrix is M with zero columns; the second adjoins one copy of b for each j\in D. Since D is nonempty, those identical copies span the same space as one augmented column. The rank operator reduces numeric entries modulo three, so
All domains used above are permitted Cartesian products with fixed numeric bounds; none chooses or orders an input element.
Finally, the proof of Theorem 1 uses only the nonempty witnesses with L\geq2, so these definitions prove both noncontainments. The empty input remains a true instance of Q under its definition in Section 1.1.
References
- [1]Faried Abu Zaid, Erich Grädel, Martin Grohe, and Wied Pakusa. Choiceless Polynomial Time on Structures with Small Abelian Colour Classes. In Mathematical Foundations of Computer Science 2014, pages 50â62, Springer, 2014. doi:10.1007/978-3-662-44522-8_5.
- [2]Andreas Blass, Yuri Gurevich, and Saharon Shelah. Choiceless Polynomial Time. Annals of Pure and Applied Logic, 100(1â3):141â187, 1999. Published text: https://shelah.logic.at/files/95758/533.pdf. Original preprint: arXiv:math/9705225v1 (1997), https://arxiv.org/abs/math/9705225v1. doi:10.1016/S0168-0072(99)00005-6.
- [3]Andreas Blass, Yuri Gurevich, and Saharon Shelah. On Polynomial Time Computation Over Unordered Structures. The Journal of Symbolic Logic, 67(3):1093â1125, 2002. https://shelah.logic.at/files/95347/760.pdf. doi:10.2178/jsl/1190150152.
- [4]Jin-Yi Cai, Martin FĂźrer, and Neil Immerman. An Optimal Lower Bound on the Number of Variables for Graph Identification. Combinatorica, 12(4):389â410, 1992. Author manuscript: https://people.cs.umass.edu/~immerman/pub/opt.pdf. doi:10.1007/BF01305232.
- [5]Peter J. Cameron. Notes on Classical Groups. 2000. Course notes, JanuaryâMarch 2000: https://webspace.maths.qmul.ac.uk/p.j.cameron/class_gps/cg.pdf. https://webspace.maths.qmul.ac.uk/p.j.cameron/class_gps/cg.pdf.
- [6]Ashok K. Chandra and David Harel. Structure and Complexity of Relational Queries. Journal of Computer and System Sciences, 25(1):99â128, 1982. Author copy: https://www.weizmann.ac.il/math/harel/sites/math.harel/files/users/user56/RelationalQueries.pdf. doi:10.1016/0022-0000(82)90012-5.
- [7]Anuj Dawar, Erich Grädel, Bjarki Holm, Eryk KopczyĹski, and Wied Pakusa. Definability of Linear Equation Systems over Groups and Rings. Logical Methods in Computer Science, 9(4):1â26, 2013. Article 12. Published text: https://arxiv.org/pdf/1204.3022. doi:10.2168/LMCS-9(4:12)2013.
- [8]Anuj Dawar, Erich Grädel, Leon Kullmann, and Benedikt Pago. Symmetric Proofs in the Ideal Proof System. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025), pages 40:1â40:18, Schloss DagstuhlâLeibniz-Zentrum fĂźr Informatik, 2025. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.40. doi:10.4230/LIPIcs.MFCS.2025.40.
- [9]Anuj Dawar, David Richerby, and Benjamin Rossman. Choiceless Polynomial Time, Counting and the CaiâFĂźrerâImmerman Graphs. Annals of Pure and Applied Logic, 152(1â3):31â50, 2008. Theorem locators refer to the author preprint dated 13 August 2007: https://www.cl.cam.ac.uk/~ad260/papers/CPT-CFI.pdf. doi:10.1016/j.apal.2007.11.011.
- [10]Erich Grädel and Wied Pakusa. Rank Logic is Dead, Long Live Rank Logic!. The Journal of Symbolic Logic, 84(1):54â87, 2019. Published text: https://wpakusa.de/assets/pdf/GraedelP19.pdf. doi:10.1017/jsl.2018.33.
- [11]Erich Grädel, Wied Pakusa, Svenja SchalthĂśfer, and Ĺukasz Kaiser. Characterising Choiceless Polynomial Time with First-Order Interpretations. In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 677â688, IEEE, 2015. Author copy: https://www.logic.rwth-aachen.de/pub/schalthoefer/GKPS15.pdf. doi:10.1109/LICS.2015.68.
- [12]Martin Grohe, Pascal Schweitzer, and Daniel Wiebking. Deep Weisfeiler Leman. In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, pages 2600â2614, SIAM, 2021. Technical locators refer to the full version arXiv:2003.10935v1, 24 March 2020: https://arxiv.org/abs/2003.10935v1. doi:10.1137/1.9781611976465.154, arXiv:2003.10935v1.
- [13]Shamgar Gurevich and Ronny Hadani. Notes on Canonical Quantization of Symplectic Vector Spaces over Finite Fields. 2009. Version 3, 20 April 2009: https://arxiv.org/abs/0708.0669v3. arXiv:0708.0669v3, https://arxiv.org/abs/0708.0669v3.
- [14]Yuri Gurevich. Logic and the Challenge of Computer Science. In Egon BĂśrger, editor, Current Trends in Theoretical Computer Science, pages 1â57, Computer Science Press, 1988. Author copy: https://web.eecs.umich.edu/~gurevich/Opera/74.pdf.
- [15]Neil Immerman. Relational Queries Computable in Polynomial Time (Extended Abstract). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pages 147â152, ACM, 1982. Author copy: https://people.cs.umass.edu/~immerman/pub/RelationalQueriesSTOC82.pdf. doi:10.1145/800070.802187.
- [16]Neil Immerman and Eric Lander. Describing Graphs: A First-Order Approach to Graph Canonization. In Alan L. Selman, editor, Complexity Theory Retrospective, pages 59â81, Springer, 1990. Author manuscript: https://people.cs.umass.edu/~immerman/pub/canon.pdf. doi:10.1007/978-1-4612-4478-3_5.
- [17]Moritz Lichter and Pascal Schweitzer. Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 31:1â31:18, Schloss DagstuhlâLeibniz-Zentrum fĂźr Informatik, 2021. doi:10.4230/LIPIcs.CSL.2021.31.
- [18]L. H. Loomis and H. Whitney. An Inequality Related to the Isoperimetric Inequality. Bulletin of the American Mathematical Society, 55(10):961â962, 1949. https://doi.org/10.1090/S0002-9904-1949-09320-5. doi:10.1090/S0002-9904-1949-09320-5.
- [19]Benedikt Pago. Choiceless Computation and Symmetry: Limitations of Definability. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 33:1â33:21, Schloss DagstuhlâLeibniz-Zentrum fĂźr Informatik, 2021. Full version arXiv:2401.07147v1, 13 January 2024: https://arxiv.org/abs/2401.07147v1. doi:10.4230/LIPIcs.CSL.2021.33.
- [20]Benedikt Pago. Lower Bounds for Choiceless Polynomial Time via Symmetric XOR-Circuits. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), pages 73:1â73:15, Schloss DagstuhlâLeibniz-Zentrum fĂźr Informatik, 2023. Full version arXiv:2302.05426v1, 8 February 2023: https://arxiv.org/abs/2302.05426v1. doi:10.4230/LIPIcs.MFCS.2023.73.
- [21]Wied Pakusa, Svenja SchalthĂśfer, and Erkal Selman. Definability of CaiâFĂźrerâImmerman Problems in Choiceless Polynomial Time. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), pages 19:1â19:17, Schloss DagstuhlâLeibniz-Zentrum fĂźr Informatik, 2016. doi:10.4230/LIPIcs.CSL.2016.19.
- [22]Benjamin Rossman. Choiceless Computation and Symmetry. In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, pages 565â580, Springer, 2010. Theorem locator refers to the author version dated 6 June 2010: https://www.math.toronto.edu/rossman/yg70.pdf. doi:10.1007/978-3-642-15025-8_28.
- [23]Saharon Shelah. Choiceless Polynomial Time Logic: Inability to Express. In Computer Science Logic, pages 72â125, Springer, 2000. Author version dated 12 May 2000: https://shelah.logic.at/files/199083/634.pdf. https://shelah.logic.at/files/199083/634.pdf.
- [24]Victor Shoup. A Computational Introduction to Number Theory and Algebra. Cambridge University Press, 2 edition, 2009. Section locators refer to author PDF version 2, 16 June 2008: https://shoup.net/ntb/ntb-v2.pdf. https://shoup.net/ntb/ntb-v2.pdf.
- [25]Moshe Y. Vardi. The Complexity of Relational Query Languages (Extended Abstract). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pages 137â146, ACM, 1982. Author copy: https://www.cs.rice.edu/~vardi/papers/stoc82.pdf. doi:10.1145/800070.802186.