ΣQSO(FO) is the logic of #P

#P is defined in the library by witness counts (DescriptiveComplexity.SharpPDefinable): the number of assignments of a block of relation variables satisfying a first-order sentence over the ordered expansion. Arenas, Muñoz, Riveros 2020 read #P as the logic ΣQSO(FO) instead, whose terms add and multiply, sum and take products over elements, and sum over relations (DescriptiveComplexity.SQTerm). The two readings coincide (DescriptiveComplexity.mem_sharpP_iff_sqDefinable):

• a witness count is the term ΣX̄. [φ];
• every term is a witness count with free variables (DescriptiveComplexity.SQTerm.wcount), by induction on the term, each construction of the logic being a closure property of witness counts (DescriptiveComplexity.Counting.QSOWitness, DescriptiveComplexity.Counting.QSOQuantifiers).

So a problem stated as a ΣQSO(FO) term – the permanent as ΣS. [S is a permutation] · Πx. (∃y. S(x, y) ∧ M(x, y)), a probability of a query as a weighted count – is in #P without writing its kernel.

theorem DescriptiveComplexity.SQTerm.wcount {M : FirstOrder.Language} {α : Type} (t : SQTerm M α) : WCount M α fun (A : Type) (x : M.Structure A) (v : α → A) => t.eval A v

Every ΣQSO(FO) term is a witness count, with its free variables.

def DescriptiveComplexity.SQDefinable {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : Prop

A counting problem is ΣQSO(FO)-definable when, on nonempty finite ordered structures, it is the value of a closed term of ΣQSO(FO) over the ordered expansion, whatever the linear order.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.mem_sharpP_iff_sqDefinable {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : SharpP.Mem C ↔ SQDefinable C

ΣQSO(FO) captures #P: a counting problem is in #P iff it is ΣQSO(FO)-definable. Registered in the Lax archive as Lax366625.SharpPAsQuantitativeLogic.mem_sharpP_iff_sqDefinable.