Separating choiceless counting from polynomial time and witnessed choice. Confirms the Blass–Gurevich–Shelah noncapture conjecture: consistency of a linear system over 𝔽3 defines a polynomial-time query on unordered finite structures that choiceless polynomial time with counting cannot express. A separate result shows that adding witnessed symmetric choice strictly increases expressive power. Both separations hold for the full counting formalism, allowing hereditarily finite sets of arbitrary finite rank.
released 2026-09-23 | 2 theorems · 12 lemmas · 21 proofs · 14,977 words |
PLAY LEVEL 1 »(pdf)
We prove that choiceless polynomial time with counting does not capture polynomial time on unordered finite structures, confirming the noncapture conjecture of Blass, Gurevich and Shelah. A linear-consistency query over 𝔽3 in a fixed binary vocabulary is decidable in polynomial time but not in the full counting formalism.
released 2026-09-24 | 4 theorems · 18 lemmas · 30 proofs · 22,114 words |
PLAY LEVEL 2 »(pdf)
We prove that witnessed symmetric choice strictly increases the expressive power of choiceless polynomial time with counting. A fixed sentence with one witnessed-choice occurrence defines a Boolean query on every finite input that is not definable in the original counting formalism.