Separating choiceless counting from polynomial time and witnessed choice

Confirms the Blass–Gurevich–Shelah noncapture conjecture: consistency of a linear system over 𝔽₃ 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. (Lean)

Manuscripts (2)

Choiceless polynomial time with counting does not capture polynomial time

September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026}

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 𝔽₃ in a fixed binary vocabulary is decidable in polynomial time but not in the full counting formalism.

Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting

September 24, 2026 · source · cite as \cite{OAI:Witnessed-symmetric-choice-is-strictly-stronger-than-choiceless-polynomial-time-with-counting-September-24-2026}

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.

Result 243 · Mathematical logic. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.