The normal form of FP: every problem of FP is digit-definable

DescriptiveComplexity.FPDefinable.digitDefinable: a counting problem defined in QFO(LFP) – a quantitative term, with sums and products over the universe, read at a least fixed point (DescriptiveComplexity.FPDefinable) – has its binary digits defined by a least fixed point (DescriptiveComplexity.DigitDefinable). This is the half of the theorem that QFO(LFP) captures FP (Arenas, Muñoz, Riveros 2020, Theorem 4.4) saying that a term is evaluated in polynomial time, read through the Immerman–Vardi theorem; it is proved here inside the logic, with no machine.

The construction

• The least fixed point of the definition is an inflationary induction (DescriptiveComplexity.LFPDef.toStepDef); above it, a tower of strata computes the digits of the term modulo 2 ^ (n ^ ℓ), for any ℓ (DescriptiveComplexity.Digits.dig_term).
• On a structure with n ≥ 2 elements the value is below 2 ^ (n ^ ℓ) for a suitable ℓ (DescriptiveComplexity.QTerm.exists_bound), so these are its digits. On a one-element structure the tuples are too few, and the digits are given directly by formulas (DescriptiveComplexity.QTerm.exists_formulas). One last first-order stratum puts the two cases together, in M + 1 groups of digits (DescriptiveComplexity.Digits.finalF).
• The tower is one inflationary induction, whose limit is a least fixed point of rules (DescriptiveComplexity.IFPLfp.homAssign_lfpAssign_trRules).

noncomputable def DescriptiveComplexity.Digits.baseStep {L : FirstOrder.Language} (d : QLFPDef L) : StepDef (L.sum FirstOrder.Language.order)

The least fixed point of a definition in QFO(LFP), as an inflationary induction: the base of the tower.

Equations

• DescriptiveComplexity.Digits.baseStep d = { B := d.B, k := d.k, rules := d.rules, out := ⊤ }.toStepDef

def DescriptiveComplexity.Digits.baseOut {L : FirstOrder.Language} (d : QLFPDef L) : QTerm ((L.sum FirstOrder.Language.order).sum (baseStep d).B.lang) Empty

The output term of a definition, over the base of the tower.

Equations

• DescriptiveComplexity.Digits.baseOut d = d.out

noncomputable def DescriptiveComplexity.Digits.singleF {L : FirstOrder.Language} {e : StepDef (L.sum FirstOrder.Language.order)} {ℓ : ℕ} : ((L.sum FirstOrder.Language.order).sum e.B.lang).Formula (Fin ℓ)

“The structure has one element.”

Equations

• DescriptiveComplexity.Digits.singleF = FirstOrder.Language.Formula.iAlls (Fin 2) ((FirstOrder.Language.var (Sum.inr 0)).equal (FirstOrder.Language.var (Sum.inr 1)))

noncomputable def DescriptiveComplexity.Digits.finalF {L : FirstOrder.Language} {d : QLFPDef L} {e : StepDef (L.sum FirstOrder.Language.order)} {ℓ M : ℕ} (x : (baseStep d).Ext e) (jD : e.B.lang.Relations (0 + ℓ)) (χ : ℕ → ((L.sum FirstOrder.Language.order).sum (baseStep d).B.lang).Formula Empty) (τ : Fin (M + 1)) : ((L.sum FirstOrder.Language.order).sum e.B.lang).Formula (Fin ℓ)

The digits of one group: on a one-element structure, the digit of the value whose rank is the number of the group; otherwise the digits computed by the tower, all in the first group.

Equations

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

theorem DescriptiveComplexity.FPDefinable.digitDefinable {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : FPDefinable C) : DigitDefinable C

Every problem of FP is digit-definable: the normal form of the capture theorem for QFO(LFP), proved inside the logic.