Eliminating an induction from a second-order definition

The theorem: a problem defined by a Σ₁ sentence read over a structure expanded by the value of an inflationary induction is Σ₁ definable outright (DescriptiveComplexity.sigmaSODefinable_of_ifpExpand). Since an induction is exactly what an FO(LFP) reduction may consult, this is what closes NP under FO(LFP) reductions (DescriptiveComplexity.FixedPointReductionClosure).

The argument, and why no fixed-point certificate is built

The direct route – guess the value of the induction inside the existential block and have the kernel check it – founders on the check: the inflationary value is not characterized by being a fixed point (the step formulas are not monotone, so a fixed point need not contain it), and pinning it down needs the whole stage sequence, which is the construction of DescriptiveComplexity.FixedPointInflationaryLFP all over again.

The route taken instead pays nothing, by pushing the induction inside the guess:

• the guessed relations are made part of the vocabulary. Over that larger vocabulary, “the induction's value satisfies the kernel” is a problem defined by an induction with a first-order output – order-free FO(IFP) definable, so in PTIME, so (DescriptiveComplexity.PTIME_subset_NP) Σ₁ definable, with no induction left;
• two consecutive existential blocks – the original guess and the one that replaces the induction – merge into one (DescriptiveComplexity.sigmaSODefinable_exBlock), which is what keeps the result at Σ₁ rather than at Σ₂.

The two supporting constructions are of the kind that has to exist once: an induction read over a larger vocabulary computes the same value (DescriptiveComplexity.StepDef.ifpHolds_liftLang), and expanding by two blocks in either order is the same structure (DescriptiveComplexity.swapExpand).

Expanding by two blocks, in either order

def DescriptiveComplexity.swapExpand (L : FirstOrder.Language) (B C : SOBlock) : (L.sum B.lang).sum C.lang →ᴸ (L.sum C.lang).sum B.lang

Swapping two block expansions: the same symbols, read in the other association.

Equations

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

theorem DescriptiveComplexity.swapExpand_isExpansionOn {L : FirstOrder.Language} {B C : SOBlock} {A : Type} (instL : L.Structure A) (ρ : B.Assignment A) (μ : C.Assignment A) : (swapExpand L B C).IsExpansionOn A

The swap is an expansion: expanding by B then by C interprets every symbol as expanding by C then by B does.

theorem DescriptiveComplexity.realize_swapExpand {L : FirstOrder.Language} {B C : SOBlock} {A : Type} (instL : L.Structure A) (ρ : B.Assignment A) (μ : C.Assignment A) (φ : ((L.sum B.lang).sum C.lang).Sentence) : A ⊨ (swapExpand L B C).onSentence φ ↔ A ⊨ φ

Realization across the swap.

An induction read over a larger vocabulary

noncomputable def DescriptiveComplexity.StepDef.liftLang {L L' : FirstOrder.Language} (φ : L →ᴸ L') (d : StepDef L) : StepDef L'

A simultaneous induction read over a larger vocabulary: the step formulas and the output are transported along the vocabulary map, which they use only through the symbols they already mention. This generalizes DescriptiveComplexity.StepDef.liftOrder, the case of the ordered expansion.

Equations

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

theorem DescriptiveComplexity.StepDef.inflLimit_liftLang {L L' : FirstOrder.Language} (φ : L →ᴸ L') (d : StepDef L) {A : Type} (instL : L.Structure A) (instL' : L'.Structure A) (hexp : φ.IsExpansionOn A) : (liftLang φ d).inflLimit A = d.inflLimit A

An induction computes the same value over a larger vocabulary.

theorem DescriptiveComplexity.StepDef.ifpHolds_liftLang {L L' : FirstOrder.Language} (φ : L →ᴸ L') (d : StepDef L) {A : Type} (instL : L.Structure A) (instL' : L'.Structure A) (hexp : φ.IsExpansionOn A) : (liftLang φ d).IFPHolds A ↔ d.IFPHolds A

The inflationary value of the lifted induction is the original one.

Two existential blocks are one

theorem DescriptiveComplexity.sigmaSODefinable_exBlock {L : FirstOrder.Language} [L.IsRelational] {C : SOBlock} {S : DecisionProblem (L.sum C.lang)} (hS : SigmaSODefinable 1 S) {P : DecisionProblem L} (hP : ∀ (A : Type) [_instA : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ ∃ (ρ : C.Assignment A), S.Holds A) : SigmaSODefinable 1 P

An existential guess over an expanded vocabulary stays in Σ₁: if S, a problem over the vocabulary expanded by a block C, is Σ₁ definable, then so is “some assignment of C makes S hold”. The two existential blocks merge into one (DescriptiveComplexity.SOBlock.cons), which is what keeps the level at Σ₁.

Eliminating the induction

theorem DescriptiveComplexity.sigmaSODefinable_of_ifpExpand {L : FirstOrder.Language} [L.IsRelational] (d : StepDef L) {S : DecisionProblem (L.sum d.B.lang)} (hS : SigmaSODefinable 1 S) {P : DecisionProblem L} (hP : ∀ (A : Type) [_instA : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ S.Holds A) : SigmaSODefinable 1 P

A Σ₁ definition read over the value of an induction is a Σ₁ definition. If S – a problem over the vocabulary expanded by the relation variables of a simultaneous induction d – is Σ₁ definable, then so is the problem “S holds of the structure expanded by the value of d”.

This is the substitution property NP needs: the FO(LFP) relations an FO(LFP) reduction consults can be removed from a Σ₁ definition, at no cost in quantifier alternation.