FO(LFP) reductions are strictly stronger than first-order ones

DescriptiveComplexity.FOReduction.toLFP embeds every first-order reduction into the FO(LFP) ones. This file shows the embedding is strict, and unconditionally: there is a problem to which EVEN reduces in FO(LFP) and to which it reduces by no first-order reduction at all (DescriptiveComplexity.exists_lfpReduction_not_orderedReduction).

The witness is as small as it can be. Let NONEMPTYMARK be “the marked subset is nonempty”, over the vocabulary of a marked set (DescriptiveComplexity.Problems.Parity). It is first-order definable – one existential quantifier – so nothing that first-order reduces to it is harder than a first-order sentence, and EVEN is not (DescriptiveComplexity.even_not_foDefinable, DescriptiveComplexity.even_not_le_of_foDefinable). Yet EVEN does FO(LFP) reduce to it: mark every element if the universe is even, none if it is odd. Deciding which is a polynomial-time question, so an induction settles it – the one already at hand, since EVEN is in PTIME – and the reduction's marking formula is that induction's output sentence, read with a free variable it ignores.

Two things to read off this.

• The gap is not about hardness: EVEN is in LOGSPACE, NONEMPTYMARK is first-order, and neither is hard for anything. It is about what a reduction may compute on its way, which is exactly the difference between AC⁰ and polynomial time.
• A reduction notion that can decide its source problem outright trivializes every problem it can decide: NONEMPTYMARK is a target only because the interpretation may answer the question itself. That is why the classical theory measures classes above the reductions' own power, and why the library's own hardness results stay stated with ≤ᶠᵒ[≤], where no such collapse happens.

A first-order target: the marked subset is nonempty

def DescriptiveComplexity.NONEMPTYMARK : DecisionProblem FirstOrder.Language.markedSet

NONEMPTYMARK: some element of the universe is marked. As simple a problem as the vocabulary of a marked set supports, and first-order definable (DescriptiveComplexity.nonemptyMark_foDefinable).

Equations

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

noncomputable def DescriptiveComplexity.nonemptyMarkS : (FirstOrder.Language.markedSet.sum FirstOrder.Language.order).Sentence

The defining sentence of DescriptiveComplexity.NONEMPTYMARK.

Equations

• DescriptiveComplexity.nonemptyMarkS = FirstOrder.Language.Formula.iExs (Fin 1) (FirstOrder.Language.markedSetMarkO.formula₁ (FirstOrder.Language.var (Sum.inr 0)))

theorem DescriptiveComplexity.nonemptyMark_foDefinable : FODefinable NONEMPTYMARK

NONEMPTYMARK is first-order definable: one existential quantifier.

EVEN reduces to it, in FO(LFP)

noncomputable def DescriptiveComplexity.evenMarkInterp (d : StepDef (FirstOrder.Language.empty.sum FirstOrder.Language.order)) : LFPInterpretation (FirstOrder.Language.empty.sum FirstOrder.Language.order) FirstOrder.Language.markedSet Unit 1

The interpretation of the reduction: the universe unchanged, every element marked exactly when the induction d – which will be one defining EVEN – answers yes. Its marking formula is the output sentence of d, read with a free variable it does not use.

Equations

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

theorem DescriptiveComplexity.relMap_evenMarkInterp {d : StepDef (FirstOrder.Language.empty.sum FirstOrder.Language.order)} (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] (xs : Fin 1 → (evenMarkInterp d).Map A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.markedSetMark xs ↔ d.IFPHolds A

Every point of the interpreted universe is marked exactly when the induction answers yes.

theorem DescriptiveComplexity.evenMarkInterp_nonempty {d : StepDef (FirstOrder.Language.empty.sum FirstOrder.Language.order)} (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] [Nonempty A] : Nonempty ((evenMarkInterp d).Map A)

Every element of the base universe is a point of the interpreted one: the domain formula is ⊤.

theorem DescriptiveComplexity.even_lfpReduction_nonemptyMark : Nonempty (LFPReduction EVEN NONEMPTYMARK)

EVEN FO(LFP)-reduces to NONEMPTYMARK: the reduction marks everything when the universe is even and nothing when it is odd, the decision being made by the induction that puts EVEN in PTIME.

The separation

theorem DescriptiveComplexity.even_not_orderedReduction_nonemptyMark : IsEmpty (OrderedFOReduction EVEN NONEMPTYMARK)

EVEN does not first-order reduce to NONEMPTYMARK: the target is first-order definable and EVEN is not, and definability travels backward along first-order reductions.

theorem DescriptiveComplexity.exists_lfpReduction_not_orderedReduction : ∃ (L : FirstOrder.Language) (x : L.IsRelational) (Q : DecisionProblem L), Nonempty (LFPReduction EVEN Q) ∧ IsEmpty (OrderedFOReduction EVEN Q)

FO(LFP) reductions are strictly stronger than first-order ones, with EVEN as the witness: it reduces to DescriptiveComplexity.NONEMPTYMARK in FO(LFP) and by no first-order reduction. No complexity-theoretic assumption enters either half.