Eliminating an induction under a quantifier prefix

DescriptiveComplexity.sigmaSODefinable_of_ifpExpand removes an inflationary induction from a Σ₁ definition. This file does it under a prefix of any length and either polarity (DescriptiveComplexity.exists_expand_sorealize), which is what closes every level of the polynomial hierarchy – and PH itself – under FO(LFP) reductions (DescriptiveComplexity.FixedPointReductionHierarchy).

Why the prefix is peeled from outside in

The blocks of a second-order prefix quantify relations on the same universe as the induction runs on, so each of them commutes with the expansion: the outermost quantifier can be pulled out, its block joined to the base vocabulary, and the rest treated by the same theorem one block shorter. Two constructions of DescriptiveComplexity.FixedPointExpand are what make the step legal – expanding by the induction's block and by the prefix's block in either order is the same structure (DescriptiveComplexity.swapExpand), and an induction read over the larger vocabulary computes the same value (DescriptiveComplexity.StepDef.inflLimit_liftLang).

The recursion therefore stops at one block, not at none, and that is where the polarity enters. With one block left the whole formula is “some (or every) assignment makes an induction-expanded kernel true”; the kernel's problem is in PTIME, so it is Σ₁ and Π₁ definable, and the block that replaces the induction is quantified the same way as the block already there – so the two merge (DescriptiveComplexity.SOBlock.cons) and the level does not rise. Existentially that is DescriptiveComplexity.PTIME_subset_NP, universally DescriptiveComplexity.PTIME_subset_coNP; the parity of the prefix decides which is used, and nothing else in the argument changes.

Merging the last block with the one that replaces the induction

theorem DescriptiveComplexity.sorealize_cons_merge {L : FirstOrder.Language} {B C : SOBlock} {A : Type} (instA : L.Structure A) (ψ : ((L.sum B.lang).sum C.lang).Sentence) (pol : Bool) : SORealize L A [B.cons C] ((mergeStep L B C).onSentence ψ) pol ↔ quantB pol fun (ρ : B.Assignment A) => quantB pol fun (μ : C.Assignment A) => A ⊨ ψ

Two consecutive quantifiers of the same polarity, over two blocks, are one quantifier over the merged block.

Peeling the prefix

theorem DescriptiveComplexity.exists_expand_sorealize {L : FirstOrder.Language} [L.IsRelational] (d : StepDef L) (Bs : List SOBlock) (hBs : Bs ≠ []) (φ : (soLang (L.sum d.B.lang) Bs).Sentence) (pol : Bool) : ∃ (Bs' : List SOBlock) (φ' : (soLang L Bs').Sentence), Bs'.length = Bs.length ∧ ∀ (A : Type) (instA : L.Structure A), Finite A → Nonempty A → (SORealize (L.sum d.B.lang) A Bs φ pol ↔ SORealize L A Bs' φ' pol)

A Σ- or Π-definition read over the value of an induction is one over the base structure, at the same level and the same polarity.