FO(≤, IFP) into FO(LFP): the capture of the inflationary limit

The hard half of the capture theorem FO(≤, IFP) = PTIME (DescriptiveComplexity.ifpDefinable_iff_mem_PTIME): every ordered inflationary definition translates back into FO(LFP) (DescriptiveComplexity.IFPDefinable.lfpDefinable), so with the embedding of DescriptiveComplexity.FixedPointInflationary the two logics are interchangeable (DescriptiveComplexity.ifpDefinable_iff_lfpDefinable) and FO(≤, IFP) captures polynomial time through Grädel's Horn fragment.

The construction

Let d : StepDef (L.sum Language.order). Because inflation adds and never removes, both a stage and its complement advance positively:

• x̄ ∈ stage (s+1) of i iff x̄ ∈ stage s or step i holds at stage s – positive in the stage relations and in the truth relations below;
• x̄ ∉ stage (s+1) of i iff x̄ ∉ stage s and step i fails at stage s – positive in the complements and the falsity relations.

So the translated program (DescriptiveComplexity.IFPLfp.trDef) carries, for each stage index (j, t̄) (the DescriptiveComplexity.FixedPointHorn stage walk: hs static copies of hm-tuples in lexicographic order), the stage S, its complement N, and a dual evaluator deriving truth T and falsity F of every subformula of every step formula at that stage, with an accumulator AC walking the order under universal quantifiers. Base-vocabulary atoms become guards; block atoms read S/N at the current stage – which is what distinguishes this evaluator from the one of DescriptiveComplexity.FixedPointHorn, whose subformula relations read the finished fixed point: here evaluation is per stage, mutually recursive with the stages themselves, stratified as stage s before evaluator at s before stage s + 1. The answer variables R are read off the maximal stage, and the output sentence survives unchanged modulo the block injection DescriptiveComplexity.SOBlock.homLHom – the point of targeting FO(LFP) rather than SO-Horn: no evaluator is ever built for the output.

Correctness

The canonical assignment (DescriptiveComplexity.IFPLfp.canonAssign) gives every translated variable its intended value; soundness (DescriptiveComplexity.IFPLfp.trRules_sound) shows it satisfies every rule, and completeness derives every canonical fact – the dual evaluator by induction on the subformula at a fixed stage (DescriptiveComplexity.IFPLfp.derives_tf, with the stage's own S/N derivability as hypotheses), the stages by induction along the cover walk of the stage order (DescriptiveComplexity.IFPLfp.derives_SN), and the answer variables by reading the top of the walk (DescriptiveComplexity.IFPLfp.derives_r, through DescriptiveComplexity.IFPLfp.inflStage_srank_top: the top rank is beyond the atom count, where the stages have stabilized to the limit).

The step formulas, over Empty

def DescriptiveComplexity.IFPLfp.stepB {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty (d.B.arity i + 0)

A step formula, as a bounded formula over Empty whose binders are the arguments of its variable: the form the subformula machinery of DescriptiveComplexity.FixedPointHorn operates on.

Equations

• DescriptiveComplexity.IFPLfp.stepB d i = FirstOrder.Language.BoundedFormula.relabel Sum.inr (d.step i)

Dimensions

noncomputable def DescriptiveComplexity.IFPLfp.hm {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : ℕ

The width of a stage tuple: the arity bound of the block.

Equations

• DescriptiveComplexity.IFPLfp.hm d = DescriptiveComplexity.blockArityBound d.B

noncomputable def DescriptiveComplexity.IFPLfp.hc {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : ℕ

The number of copies of the stage relations: as in DescriptiveComplexity.LFPHorn.hs, enough for (hc + 1) · n^hm stages to exceed the number of atoms of the block on every nonempty structure.

Equations

• DescriptiveComplexity.IFPLfp.hc d = Nat.card d.B.ι

noncomputable def DescriptiveComplexity.IFPLfp.hs {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : ℕ

The number of copies of the stage relations: as in DescriptiveComplexity.LFPHorn.hs, enough for (hc + 1) · n^hm stages to exceed the number of atoms of the block on every nonempty structure.

Equations

• DescriptiveComplexity.IFPLfp.hs d = DescriptiveComplexity.IFPLfp.hc d + 1

noncomputable def DescriptiveComplexity.IFPLfp.hX {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : ℕ

The number of variables reserved for evaluating the step formulas: a bound on the binder depths of all their subformulas.

Equations

• DescriptiveComplexity.IFPLfp.hX d = Finset.univ.sup fun (i : d.B.ι) => DescriptiveComplexity.ctxB (DescriptiveComplexity.IFPLfp.stepB d i)

theorem DescriptiveComplexity.IFPLfp.ctxB_le_hX {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : ctxB (stepB d i) ≤ hX d

noncomputable def DescriptiveComplexity.IFPLfp.kk {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : ℕ

The universally quantified first-order variables shared by all clauses: two stage-tuple blocks (current and next), the atom tuple, the evaluation block, and one spare for the accumulators.

Equations

• DescriptiveComplexity.IFPLfp.kk d = 3 * DescriptiveComplexity.IFPLfp.hm d + DescriptiveComplexity.IFPLfp.hX d + 1

The block of the translation

def DescriptiveComplexity.IFPLfp.SubIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : Type

Index of the truth, falsity and accumulator relations: a variable of the block together with a subformula of its step formula.

Equations

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

instance DescriptiveComplexity.IFPLfp.instFiniteSubtypeSigmaNatBoundedFormulaSumOrderLangBEmptyMemListSubsStepB {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : Finite { x : (n' : ℕ) × ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n' // x ∈ subs (stepB d i) }

instance DescriptiveComplexity.IFPLfp.instFiniteSubIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : Finite (SubIx d)

theorem DescriptiveComplexity.IFPLfp.subIx_le_hX {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (x : SubIx d) : (↑x.snd).fst ≤ hX d

The binder depth of a subformula index is within the evaluation block.

@[reducible, inline]

abbrev DescriptiveComplexity.IFPLfp.TrIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : Type

The relation variables of the translated program: the answer variables R, the stages S, their complements N, the truth/falsity relations T/F (Bool-tagged), and the ∀-accumulators AC.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.IFPLfp.rIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : TrIx d

The answer variables.

Equations

• DescriptiveComplexity.IFPLfp.rIx d i = Sum.inl i

@[reducible, inline]

abbrev DescriptiveComplexity.IFPLfp.sIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (i : d.B.ι) : TrIx d

S j i (t̄, x̄): at stage (j, t̄), the atom i x̄ is derived.

Equations

• DescriptiveComplexity.IFPLfp.sIx d j i = Sum.inr (Sum.inl (true, j, i))

@[reducible, inline]

abbrev DescriptiveComplexity.IFPLfp.nIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (i : d.B.ι) : TrIx d

N j i (t̄, x̄): at stage (j, t̄), the atom i x̄ is not derived.

Equations

• DescriptiveComplexity.IFPLfp.nIx d j i = Sum.inr (Sum.inl (false, j, i))

@[reducible, inline]

abbrev DescriptiveComplexity.IFPLfp.tfIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (x : SubIx d) (b : Bool) : TrIx d

Truth (true) and falsity (false) of a subformula of a step formula at a stage.

Equations

• DescriptiveComplexity.IFPLfp.tfIx d j x b = Sum.inr (Sum.inr (Sum.inl (j, x, b)))

@[reducible, inline]

abbrev DescriptiveComplexity.IFPLfp.acIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (x : SubIx d) : TrIx d

The accumulator of a universally quantified subformula at a stage.

Equations

• DescriptiveComplexity.IFPLfp.acIx d j x = Sum.inr (Sum.inr (Sum.inr (j, x)))

noncomputable def DescriptiveComplexity.IFPLfp.trArity {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : TrIx d → ℕ

The arities: answer variables keep theirs, stage relations carry a stage tuple in front of theirs, subformula relations a stage tuple in front of their binder depth, accumulators one more.

Equations

• DescriptiveComplexity.IFPLfp.trArity d (Sum.inl i) = d.B.arity i
• DescriptiveComplexity.IFPLfp.trArity d (Sum.inr (Sum.inl (fst, fst_1, i))) = DescriptiveComplexity.IFPLfp.hm d + d.B.arity i
• DescriptiveComplexity.IFPLfp.trArity d (Sum.inr (Sum.inr (Sum.inl (fst, x_1, snd)))) = DescriptiveComplexity.IFPLfp.hm d + (↑x_1.snd).fst
• DescriptiveComplexity.IFPLfp.trArity d (Sum.inr (Sum.inr (Sum.inr (fst, x_1)))) = DescriptiveComplexity.IFPLfp.hm d + (↑x_1.snd).fst + 1

noncomputable def DescriptiveComplexity.IFPLfp.trBlock {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : SOBlock

The block of the translated program.

Equations

• DescriptiveComplexity.IFPLfp.trBlock d = { ι := DescriptiveComplexity.IFPLfp.TrIx d, ιFinite := ⋯, arity := DescriptiveComplexity.IFPLfp.trArity d }

The shared first-order variables and their layout

noncomputable def DescriptiveComplexity.IFPLfp.vT1 {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (q : Fin (hm d)) : Fin (kk d)

The current stage tuple t̄.

Equations

• DescriptiveComplexity.IFPLfp.vT1 d q = ⟨↑q, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.vT2 {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (q : Fin (hm d)) : Fin (kk d)

The next stage tuple t̄'.

Equations

• DescriptiveComplexity.IFPLfp.vT2 d q = ⟨DescriptiveComplexity.IFPLfp.hm d + ↑q, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.vX {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (q : Fin (hm d)) : Fin (kk d)

The atom tuple x̄, the scratch the block-atom evaluation rules equate with the (evaluated) arguments of a block atom.

Equations

• DescriptiveComplexity.IFPLfp.vX d q = ⟨2 * DescriptiveComplexity.IFPLfp.hm d + ↑q, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.vE {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (q : Fin (hX d)) : Fin (kk d)

The evaluation block ē, holding the free variables of a subformula of a step formula.

Equations

• DescriptiveComplexity.IFPLfp.vE d q = ⟨3 * DescriptiveComplexity.IFPLfp.hm d + ↑q, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.vS {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : Fin (kk d)

The spare variable, the accumulator's predecessor.

Equations

• DescriptiveComplexity.IFPLfp.vS d = ⟨3 * DescriptiveComplexity.IFPLfp.hm d + DescriptiveComplexity.IFPLfp.hX d, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.eSel {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {n : ℕ} (hn : n ≤ hX d) (q : Fin n) : Fin (kk d)

The first n variables of the evaluation block.

Equations

• DescriptiveComplexity.IFPLfp.eSel d hn q = DescriptiveComplexity.IFPLfp.vE d ⟨↑q, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.xa {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) (q : Fin (d.B.arity i)) : Fin (kk d)

The atom tuple of a relation variable i, inside the x̄ block.

Equations

• DescriptiveComplexity.IFPLfp.xa d i q = DescriptiveComplexity.IFPLfp.vX d ⟨↑q, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.j0 {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : Fin (hs d)

The first copy.

Equations

• DescriptiveComplexity.IFPLfp.j0 d = ⟨0, ⋯⟩

noncomputable def DescriptiveComplexity.IFPLfp.jTop {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : Fin (hs d)

The last copy.

Equations

• DescriptiveComplexity.IFPLfp.jTop d = ⟨DescriptiveComplexity.IFPLfp.hc d, ⋯⟩

Atom builders

noncomputable def DescriptiveComplexity.IFPLfp.rAt {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) (sel : Fin (d.B.arity i) → Fin (kk d)) : SOAtom (trBlock d) (kk d)

An atom of an answer variable.

Equations

• DescriptiveComplexity.IFPLfp.rAt d i sel = { idx := DescriptiveComplexity.IFPLfp.rIx d i, args := sel }

noncomputable def DescriptiveComplexity.IFPLfp.sAt {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (i : d.B.ι) (ts : Fin (hm d) → Fin (kk d)) (xs : Fin (d.B.arity i) → Fin (kk d)) : SOAtom (trBlock d) (kk d)

An atom S j i (t̄, x̄).

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.nAt {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (i : d.B.ι) (ts : Fin (hm d) → Fin (kk d)) (xs : Fin (d.B.arity i) → Fin (kk d)) : SOAtom (trBlock d) (kk d)

An atom N j i (t̄, x̄).

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.tfAt {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (x : SubIx d) (b : Bool) (ts : Fin (hm d) → Fin (kk d)) (es : Fin (↑x.snd).fst → Fin (kk d)) : SOAtom (trBlock d) (kk d)

A truth or falsity atom of a subformula at a stage.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.acAt {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (x : SubIx d) (ts : Fin (hm d) → Fin (kk d)) (es : Fin ((↑x.snd).fst + 1) → Fin (kk d)) : SOAtom (trBlock d) (kk d)

An accumulator atom of a subformula at a stage.

Equations

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

The rules of the translated program

noncomputable def DescriptiveComplexity.IFPLfp.iotaList {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : List d.B.ι

The relation variables, as a list.

Equations

• DescriptiveComplexity.IFPLfp.iotaList d = Finset.univ.toList

theorem DescriptiveComplexity.IFPLfp.mem_iotaList {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : i ∈ iotaList d

noncomputable def DescriptiveComplexity.IFPLfp.stagePairs {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : List (Fin (hs d) × Fin (hs d))

The stage-successor pairs of copies: within one copy, or crossing to the next (as in DescriptiveComplexity.LFPHorn.stagePairs).

Equations

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

theorem DescriptiveComplexity.IFPLfp.mem_stagePairs {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {j j' : Fin (hs d)} : (j, j') ∈ stagePairs d ↔ j = j' ∨ ↑j + 1 = ↑j'

noncomputable def DescriptiveComplexity.IFPLfp.stageG {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j j' : Fin (hs d)) : (L.sum FirstOrder.Language.order).Formula (Fin (kk d))

The guard stepping from stage (j, t̄) to stage (j', t̄'): the successor tuple within a copy, the wrap-around between consecutive copies.

Equations

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

def DescriptiveComplexity.IFPLfp.rootSub {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : SubIx d

The root subformula of a variable's step formula.

Equations

• DescriptiveComplexity.IFPLfp.rootSub d i = ⟨i, ⟨⟨d.B.arity i + 0, DescriptiveComplexity.IFPLfp.stepB d i⟩, ⋯⟩⟩

noncomputable def DescriptiveComplexity.IFPLfp.rootSel {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : Fin (↑(rootSub d i).snd).fst → Fin (kk d)

The evaluation selector of the root subformula is the atom tuple.

Equations

• DescriptiveComplexity.IFPLfp.rootSel d i = DescriptiveComplexity.IFPLfp.eSel d ⋯

The stage rules

noncomputable def DescriptiveComplexity.IFPLfp.sCarry {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

Carry: a derived atom stays derived at the next stage.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.sDerive {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

Derive: an atom whose step formula is true at a stage is derived at the next stage. This is where inflation is used: the new stage is the old one plus what the step formulas add.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.nBase {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

Base: at the first stage, nothing is derived.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.nStep {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

Complement step: an underived atom whose step formula is false at a stage stays underived at the next stage. This is where inflation pays: non-membership in the next stage is a conjunction of two positive atoms.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.rRules {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

Read-off: the answer variables hold the maximal stage.

Equations

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

The dual evaluator

noncomputable def DescriptiveComplexity.IFPLfp.evTerm {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) {n : ℕ} (hn : n ≤ hX d) (t : ((L.sum FirstOrder.Language.order).sum d.B.lang).Term (Empty ⊕ Fin n)) : (L.sum FirstOrder.Language.order).Term (Fin (kk d))

A term of a subformula, as a term of the guard vocabulary over the evaluation variables.

Equations

• DescriptiveComplexity.IFPLfp.evTerm d hn t = FirstOrder.Language.Term.relabel (Sum.elim (fun (e : Empty) => e.elim) (DescriptiveComplexity.IFPLfp.eSel d hn)) (DescriptiveComplexity.stripTerm t)

noncomputable def DescriptiveComplexity.IFPLfp.evalClauses {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (j : Fin (hs d)) (x : SubIx d) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

The rules evaluating one subformula of a step formula at the stages, by shape: the dual T/F derivation, with base-vocabulary atoms and equalities as guards, block atoms reading S/N at the current stage, and the accumulator walking the order under a universal quantifier.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.evalRules {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

All evaluation rules: every stage copy, every variable, every subformula of its step formula.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.trRules {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

The rules of the translated program.

Equations

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

The translated definition

theorem DescriptiveComplexity.IFPLfp.trArity_rIx {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (i : d.B.ι) : (trBlock d).arity (rIx d i) = d.B.arity i

The arities of the answer variables are those of the original block.

noncomputable def DescriptiveComplexity.IFPLfp.trDef {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) : LFPDef L

The translated FO(LFP) definition: the rules above, with the original output sentence transported along the answer-variable injection (DescriptiveComplexity.SOBlock.homLHom).

Equations

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

The canonical assignment

Over a fixed ordered structure, each relation variable of the translated block has an intended value; the correctness proof (to come) will show that the least model of the rules is exactly this assignment. Every predicate is a named definition, so reduction stops at it (the DescriptiveComplexity.FixedPointHorn discipline).

noncomputable def DescriptiveComplexity.IFPLfp.srank {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (A : Type) [LinearOrder A] (j : Fin (hs d)) (t : Fin (hm d) → A) : ℕ

The rank of a stage: its position in the lexicographic order of the pairs of a copy index and a stage tuple.

Equations

• DescriptiveComplexity.IFPLfp.srank d A j t = DescriptiveComplexity.orank (toLex (j, toLex t))

noncomputable def DescriptiveComplexity.IFPLfp.canonS {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] (j : Fin (hs d)) (i : d.B.ι) (w : Fin (hm d + d.B.arity i) → A) : Prop

A stage of the inflationary iteration, at a stage index.

Equations

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

noncomputable def DescriptiveComplexity.IFPLfp.canonN {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] (j : Fin (hs d)) (i : d.B.ι) (w : Fin (hm d + d.B.arity i) → A) : Prop

The complement of a stage of the inflationary iteration.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.IFPLfp.stageStr {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] (r : ℕ) : ((L.sum FirstOrder.Language.order).sum d.B.lang).Structure A

The structure interpreting the expanded vocabulary at a stage of the iteration – the structure the step formulas are read in there.

Equations

• DescriptiveComplexity.IFPLfp.stageStr d A r = (L.sum FirstOrder.Language.order).sumStructure d.B.lang A

noncomputable def DescriptiveComplexity.IFPLfp.evalT {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] (r : ℕ) {n : ℕ} (ψ : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n) (v : Fin n → A) : Prop

Truth of a subformula of a step formula at a stage of the iteration.

Equations

• DescriptiveComplexity.IFPLfp.evalT d A r ψ v = ψ.Realize default v

noncomputable def DescriptiveComplexity.IFPLfp.canonAc {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] (r : ℕ) (x : SubIx d) : (Fin ((↑x.snd).fst + 1) → A) → Prop

The intended accumulator of a universally quantified subformula at a stage: the quantified subformula holds up to the last argument. Other subformulas have no accumulator; theirs is empty.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.IFPLfp.canonAc d A r x = fun (x : Fin ((↑x.snd).fst + 1) → A) => False

noncomputable def DescriptiveComplexity.IFPLfp.canonAssign {L : FirstOrder.Language} (d : StepDef (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] : (trBlock d).Assignment A

The canonical assignment: the limit on the answer variables, the stages and their complements on S/N, truth and falsity of the step formulas' subformulas at the stages, and the accumulators.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.IFPLfp.canonAssign d A (Sum.inl i) = fun (x : Fin ((DescriptiveComplexity.IFPLfp.trBlock d).arity (Sum.inl i)) → A) => d.inflLimit A i x
• DescriptiveComplexity.IFPLfp.canonAssign d A (Sum.inr (Sum.inl (true, j, i))) = DescriptiveComplexity.IFPLfp.canonS d A j i
• DescriptiveComplexity.IFPLfp.canonAssign d A (Sum.inr (Sum.inl (false, j, i))) = DescriptiveComplexity.IFPLfp.canonN d A j i

Atom characterizations under the canonical assignment

theorem DescriptiveComplexity.IFPLfp.rAt_holds {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {i : d.B.ι} {sel : Fin (d.B.arity i) → Fin (kk d)} {V : Fin (kk d) → A} : (rAt d i sel).Holds (canonAssign d A) V ↔ d.inflLimit A i fun (q : Fin (d.B.arity i)) => V (sel q)

theorem DescriptiveComplexity.IFPLfp.sAt_holds {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {i : d.B.ι} {ts : Fin (hm d) → Fin (kk d)} {xs : Fin (d.B.arity i) → Fin (kk d)} {V : Fin (kk d) → A} : (sAt d j i ts xs).Holds (canonAssign d A) V ↔ d.inflStage A (srank d A j fun (q : Fin (hm d)) => V (ts q)) i fun (q : Fin (d.B.arity i)) => V (xs q)

theorem DescriptiveComplexity.IFPLfp.nAt_holds {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {i : d.B.ι} {ts : Fin (hm d) → Fin (kk d)} {xs : Fin (d.B.arity i) → Fin (kk d)} {V : Fin (kk d) → A} : (nAt d j i ts xs).Holds (canonAssign d A) V ↔ ¬d.inflStage A (srank d A j fun (q : Fin (hm d)) => V (ts q)) i fun (q : Fin (d.B.arity i)) => V (xs q)

theorem DescriptiveComplexity.IFPLfp.tAt_holds {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {x : SubIx d} {ts : Fin (hm d) → Fin (kk d)} {es : Fin (↑x.snd).fst → Fin (kk d)} {V : Fin (kk d) → A} : (tfAt d j x true ts es).Holds (canonAssign d A) V ↔ evalT d A (srank d A j fun (q : Fin (hm d)) => V (ts q)) (↑x.snd).snd fun (q : Fin (↑x.snd).fst) => V (es q)

theorem DescriptiveComplexity.IFPLfp.fAt_holds {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {x : SubIx d} {ts : Fin (hm d) → Fin (kk d)} {es : Fin (↑x.snd).fst → Fin (kk d)} {V : Fin (kk d) → A} : (tfAt d j x false ts es).Holds (canonAssign d A) V ↔ ¬evalT d A (srank d A j fun (q : Fin (hm d)) => V (ts q)) (↑x.snd).snd fun (q : Fin (↑x.snd).fst) => V (es q)

theorem DescriptiveComplexity.IFPLfp.acAt_holds {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {x : SubIx d} {ts : Fin (hm d) → Fin (kk d)} {es : Fin ((↑x.snd).fst + 1) → Fin (kk d)} {V : Fin (kk d) → A} : (acAt d j x ts es).Holds (canonAssign d A) V ↔ canonAc d A (srank d A j fun (q : Fin (hm d)) => V (ts q)) x fun (q : Fin ((↑x.snd).fst + 1)) => V (es q)

theorem DescriptiveComplexity.IFPLfp.canonAc_all_snoc {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r : ℕ} {i : d.B.ι} {n : ℕ} {χ : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty (n + 1)} {hmem : ⟨n, χ.all⟩ ∈ subs (stepB d i)} {v : Fin n → A} {y : A} : canonAc d A r ⟨i, ⟨⟨n, χ.all⟩, hmem⟩⟩ (Fin.snoc v y) ↔ ∀ z ≤ y, evalT d A r χ (Fin.snoc v z)

The accumulator of ∀, at an explicit snoc tuple.

The stage walk, quantitatively

The interface the correctness inductions consume: the first stage has rank 0, a stageG step raises the rank by one, and the last stage's rank is beyond the atom count – so the stage read off by the answer rules is the inflationary limit.

theorem DescriptiveComplexity.IFPLfp.srank_bot {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [LinearOrder A] {t : Fin (hm d) → A} (ht : ∀ (p : Fin (hm d)) (a : A), t p ≤ a) : srank d A (j0 d) t = 0

theorem DescriptiveComplexity.IFPLfp.stageG_covBy {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {j j' : Fin (hs d)} {V : Fin (kk d) → A} (hjj : (j, j') ∈ stagePairs d) (h : (stageG d j j').Realize V) : toLex (j, toLex fun (q : Fin (hm d)) => V (vT1 d q)) ⋖ toLex (j', toLex fun (q : Fin (hm d)) => V (vT2 d q))

theorem DescriptiveComplexity.IFPLfp.stageG_realize {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {j j' : Fin (hs d)} {V : Fin (kk d) → A} (hjj : (j, j') ∈ stagePairs d) (hcov : toLex (j, toLex fun (q : Fin (hm d)) => V (vT1 d q)) ⋖ toLex (j', toLex fun (q : Fin (hm d)) => V (vT2 d q))) : (stageG d j j').Realize V

A cover of stages, as a realized stage guard.

theorem DescriptiveComplexity.IFPLfp.stagePairs_of_covBy {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [LinearOrder A] [Nonempty A] {j j' : Fin (hs d)} {u u' : Lex (Fin (hm d) → A)} (hcov : toLex (j, u) ⋖ toLex (j', u')) : (j, j') ∈ stagePairs d

A cover of stages is a stage pair.

theorem DescriptiveComplexity.IFPLfp.srank_stageG {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {j j' : Fin (hs d)} {V : Fin (kk d) → A} (hjj : (j, j') ∈ stagePairs d) (h : (stageG d j j').Realize V) : (srank d A j' fun (q : Fin (hm d)) => V (vT2 d q)) = (srank d A j fun (q : Fin (hm d)) => V (vT1 d q)) + 1

A stageG step raises the stage rank by one.

theorem DescriptiveComplexity.IFPLfp.card_le_srank_top {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t : Fin (hm d) → A} (ht : ∀ (p : Fin (hm d)) (a : A), a ≤ t p) : Nat.card (BAtom d.B A) ≤ srank d A (jTop d) t

theorem DescriptiveComplexity.IFPLfp.inflStage_srank_top {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {t : Fin (hm d) → A} (ht : ∀ (p : Fin (hm d)) (a : A), a ≤ t p) : d.inflStage A (srank d A (jTop d) t) = d.inflLimit A

The stage at the top rank is the inflationary limit.

Soundness: the canonical assignment satisfies the rules

noncomputable def DescriptiveComplexity.IFPLfp.evTermVal {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] (r : ℕ) {n : ℕ} (v : Fin n → A) (t : ((L.sum FirstOrder.Language.order).sum d.B.lang).Term (Empty ⊕ Fin n)) : A

The value of a term of the expanded vocabulary at a stage.

Equations

• DescriptiveComplexity.IFPLfp.evTermVal r v t = FirstOrder.Language.Term.realize (Sum.elim default v) t

theorem DescriptiveComplexity.IFPLfp.evalT_imp {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r n : ℕ} {a b : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n} {v : Fin n → A} : evalT d A r (a.imp b) v ↔ evalT d A r a v → evalT d A r b v

theorem DescriptiveComplexity.IFPLfp.evalT_all {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r n : ℕ} {a : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty (n + 1)} {v : Fin n → A} : evalT d A r a.all v ↔ ∀ (y : A), evalT d A r a (Fin.snoc v y)

theorem DescriptiveComplexity.IFPLfp.evalT_equal {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r n : ℕ} {t u : ((L.sum FirstOrder.Language.order).sum d.B.lang).Term (Empty ⊕ Fin n)} {v : Fin n → A} : evalT d A r (FirstOrder.Language.BoundedFormula.equal t u) v ↔ evTermVal r v t = evTermVal r v u

theorem DescriptiveComplexity.IFPLfp.evalT_rel_inl {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r n l : ℕ} {rl : (L.sum FirstOrder.Language.order).Relations l} {ts : Fin l → ((L.sum FirstOrder.Language.order).sum d.B.lang).Term (Empty ⊕ Fin n)} {v : Fin n → A} : evalT d A r (FirstOrder.Language.BoundedFormula.rel (Sum.inl rl) ts) v ↔ FirstOrder.Language.Structure.RelMap rl fun (q : Fin l) => evTermVal r v (ts q)

theorem DescriptiveComplexity.IFPLfp.evalT_rel_inr {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r n l : ℕ} {rl : d.B.lang.Relations l} {ts : Fin l → ((L.sum FirstOrder.Language.order).sum d.B.lang).Term (Empty ⊕ Fin n)} {v : Fin n → A} : evalT d A r (FirstOrder.Language.BoundedFormula.rel (Sum.inr rl) ts) v ↔ d.inflStage A r ↑rl fun (q : Fin (d.B.arity ↑rl)) => evTermVal r v (ts (Fin.cast ⋯ q))

theorem DescriptiveComplexity.IFPLfp.evalT_stepB {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r : ℕ} {i : d.B.ι} {v : Fin (d.B.arity i + 0) → A} : evalT d A r (stepB d i) v ↔ d.next (d.inflStage A r) i fun (q : Fin (d.B.arity i)) => v (Fin.castAdd 0 q)

Truth of a step formula at a stage is one application of the step.

theorem DescriptiveComplexity.IFPLfp.realize_evTerm {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {r n : ℕ} (hn : n ≤ hX d) {V : Fin (kk d) → A} (t : ((L.sum FirstOrder.Language.order).sum d.B.lang).Term (Empty ⊕ Fin n)) : FirstOrder.Language.Term.realize V (evTerm d hn t) = evTermVal r (fun (q : Fin n) => V (eSel d hn q)) t

theorem DescriptiveComplexity.IFPLfp.eSel_snoc {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} {n : ℕ} (hn1 : n + 1 ≤ hX d) {V : Fin (kk d) → A} : (fun (q : Fin (n + 1)) => V (eSel d hn1 q)) = Fin.snoc (fun (q : Fin n) => V (eSel d ⋯ q)) (V (eSel d hn1 (Fin.last n)))

The evaluation tuple of a wider context, as a snoc.

The stage rules are sound

theorem DescriptiveComplexity.IFPLfp.sCarry_sound {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} [Finite A] [Nonempty A] {j j' : Fin (hs d)} (hjj : (j, j') ∈ stagePairs d) {i : d.B.ι} : { guard := stageG d j j', body := [sAt d j i (vT1 d) (xa d i)], head := some (sAt d j' i (vT2 d) (xa d i)) }.Holds (canonAssign d A) V

theorem DescriptiveComplexity.IFPLfp.sDerive_sound {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} [Finite A] [Nonempty A] {j j' : Fin (hs d)} (hjj : (j, j') ∈ stagePairs d) {i : d.B.ι} : { guard := stageG d j j', body := [tfAt d j (rootSub d i) true (vT1 d) (rootSel d i)], head := some (sAt d j' i (vT2 d) (rootSel d i)) }.Holds (canonAssign d A) V

theorem DescriptiveComplexity.IFPLfp.nBase_sound {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} {i : d.B.ι} : { guard := minTupF (vT1 d), body := [], head := some (nAt d (j0 d) i (vT1 d) (xa d i)) }.Holds (canonAssign d A) V

theorem DescriptiveComplexity.IFPLfp.nStep_sound {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} [Finite A] [Nonempty A] {j j' : Fin (hs d)} (hjj : (j, j') ∈ stagePairs d) {i : d.B.ι} : { guard := stageG d j j', body := [nAt d j i (vT1 d) (rootSel d i), tfAt d j (rootSub d i) false (vT1 d) (rootSel d i)], head := some (nAt d j' i (vT2 d) (rootSel d i)) }.Holds (canonAssign d A) V

theorem DescriptiveComplexity.IFPLfp.rRules_sound {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} [Finite A] [Nonempty A] {i : d.B.ι} : { guard := maxTupF (vT1 d), body := [sAt d (jTop d) i (vT1 d) (xa d i)], head := some (rAt d i (xa d i)) }.Holds (canonAssign d A) V

The evaluator is sound

theorem DescriptiveComplexity.IFPLfp.evalClauses_sound {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} {j : Fin (hs d)} {x : SubIx d} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (hc : c ∈ evalClauses d j x) : c.Holds (canonAssign d A) V

All rules are sound

theorem DescriptiveComplexity.IFPLfp.trRules_sound {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (V : Fin (kk d) → A) {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (hc : c ∈ trRules d) : c.Holds (canonAssign d A) V

Completeness: every canonical fact is derivable

noncomputable def DescriptiveComplexity.IFPLfp.packV {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} (t1 t2 x : Fin (hm d) → A) (e : Fin (hX d) → A) (sp : A) : Fin (kk d) → A

Assembling a valuation of the shared variables from its blocks.

Equations

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

theorem DescriptiveComplexity.IFPLfp.packV_comp_vT1 {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} {t1 t2 x : Fin (hm d) → A} {e : Fin (hX d) → A} {sp : A} : (fun (q : Fin (hm d)) => packV t1 t2 x e sp (vT1 d q)) = t1

theorem DescriptiveComplexity.IFPLfp.packV_comp_vT2 {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} {t1 t2 x : Fin (hm d) → A} {e : Fin (hX d) → A} {sp : A} : (fun (q : Fin (hm d)) => packV t1 t2 x e sp (vT2 d q)) = t2

theorem DescriptiveComplexity.IFPLfp.packV_comp_eSel {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} {t1 t2 x : Fin (hm d) → A} {e : Fin (hX d) → A} {sp : A} {n : ℕ} (hn : n ≤ hX d) {v : Fin n → A} (hpad : ∀ (q : Fin n), e ⟨↑q, ⋯⟩ = v q) : (fun (q : Fin n) => packV t1 t2 x e sp (eSel d hn q)) = v

theorem DescriptiveComplexity.IFPLfp.packV_vS {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} {t1 t2 x : Fin (hm d) → A} {e : Fin (hX d) → A} {sp : A} : packV t1 t2 x e sp (vS d) = sp

theorem DescriptiveComplexity.IFPLfp.packV_comp_xa {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} {t1 t2 x : Fin (hm d) → A} {e : Fin (hX d) → A} {sp : A} {i : d.B.ι} {xt : Fin (d.B.arity i) → A} (hpad : ∀ (q : Fin (d.B.arity i)), x ⟨↑q, ⋯⟩ = xt q) : (fun (q : Fin (d.B.arity i)) => packV t1 t2 x e sp (xa d i q)) = xt

noncomputable def DescriptiveComplexity.IFPLfp.padF {A : Type} [Nonempty A] {m M : ℕ} (f : Fin m → A) : Fin M → A

Extending a tuple to a wider block, junk-padded.

Equations

• DescriptiveComplexity.IFPLfp.padF f p = if h : ↑p < m then f ⟨↑p, h⟩ else Classical.arbitrary A

theorem DescriptiveComplexity.IFPLfp.packV_comp_eSel_pad {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [Nonempty A] {t1 t2 x : Fin (hm d) → A} {sp : A} {n : ℕ} (hn : n ≤ hX d) {v : Fin n → A} : (fun (q : Fin n) => packV t1 t2 x (padF v) sp (eSel d hn q)) = v

theorem DescriptiveComplexity.IFPLfp.packV_comp_xa_pad {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [Nonempty A] {t1 t2 : Fin (hm d) → A} {e : Fin (hX d) → A} {sp : A} {i : d.B.ι} {xt : Fin (d.B.arity i) → A} : (fun (q : Fin (d.B.arity i)) => packV t1 t2 (padF xt) e sp (xa d i q)) = xt

Membership of the rules in the program

theorem DescriptiveComplexity.IFPLfp.mem_trRules_sCarry {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ sCarry d) : c ∈ trRules d

theorem DescriptiveComplexity.IFPLfp.mem_trRules_sDerive {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ sDerive d) : c ∈ trRules d

theorem DescriptiveComplexity.IFPLfp.mem_trRules_nBase {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ nBase d) : c ∈ trRules d

theorem DescriptiveComplexity.IFPLfp.mem_trRules_nStep {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ nStep d) : c ∈ trRules d

theorem DescriptiveComplexity.IFPLfp.mem_trRules_rRules {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ rRules d) : c ∈ trRules d

theorem DescriptiveComplexity.IFPLfp.mem_trRules_evalClauses {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {j : Fin (hs d)} {x : SubIx d} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ evalClauses d j x) : c ∈ trRules d

The subformula relations are derivable

theorem DescriptiveComplexity.IFPLfp.derives_tf {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {j : Fin (hs d)} {t : Fin (hm d) → A} (hS : ∀ (i : d.B.ι) (xt : Fin (d.B.arity i) → A), d.inflStage A (srank d A j t) i xt → Derives (trRules d) ⟨sIx d j i, fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases t xt i_1⟩) (hN : ∀ (i : d.B.ι) (xt : Fin (d.B.arity i) → A), ¬d.inflStage A (srank d A j t) i xt → Derives (trRules d) ⟨nIx d j i, fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases t xt i_1⟩) {n : ℕ} (ψ : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n) {i : d.B.ι} (hmem : ⟨n, ψ⟩ ∈ subs (stepB d i)) (v : Fin n → A) : (evalT d A (srank d A j t) ψ v → Derives (trRules d) ⟨tfIx d j ⟨i, ⟨⟨n, ψ⟩, hmem⟩⟩ true, fun (i_1 : Fin (hm d + (↑⟨i, ⟨⟨n, ψ⟩, hmem⟩⟩.snd).fst)) => Fin.addCases t v i_1⟩) ∧ (¬evalT d A (srank d A j t) ψ v → Derives (trRules d) ⟨tfIx d j ⟨i, ⟨⟨n, ψ⟩, hmem⟩⟩ false, fun (i_1 : Fin (hm d + (↑⟨i, ⟨⟨n, ψ⟩, hmem⟩⟩.snd).fst)) => Fin.addCases t v i_1⟩)

The dual evaluator is complete at a stage: given that the stage and its complement are derivable there, truth and falsity of every subformula of every step formula are derivable, by induction on the subformula.

The stages and their complements are derivable

theorem DescriptiveComplexity.IFPLfp.derives_SN {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (u : Lex (Fin (hs d) × Lex (Fin (hm d) → A))) : (∀ (i : d.B.ι) (xt : Fin (d.B.arity i) → A), d.inflStage A (orank u) i xt → Derives (trRules d) ⟨sIx d (ofLex u).1 i, fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases (ofLex (ofLex u).2) xt i_1⟩) ∧ ∀ (i : d.B.ι) (xt : Fin (d.B.arity i) → A), ¬d.inflStage A (orank u) i xt → Derives (trRules d) ⟨nIx d (ofLex u).1 i, fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases (ofLex (ofLex u).2) xt i_1⟩

The stage walk is complete: at every stage index, the stage and its complement are derivable – by induction along the cover walk of the stage order, the evaluator supplying the step formulas' values at the predecessor stage.

The answer variables are derivable

theorem DescriptiveComplexity.IFPLfp.derives_r {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {i : d.B.ι} {x : Fin (d.B.arity i) → A} (h : d.inflLimit A i x) : Derives (trRules d) ⟨rIx d i, x⟩

Every atom of the inflationary limit is derivable on the answer variables: read the stage at the top of the walk.

Assembly: the capture of the inflationary limit

theorem DescriptiveComplexity.IFPLfp.homAssign_lfpAssign_trRules {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : SOBlock.homAssign (rIx d) ⋯ (lfpAssign (trRules d)) = d.inflLimit A

The answer variables of the least model are the inflationary limit: soundness bounds the least model by the canonical assignment, and completeness derives every limit atom.

theorem DescriptiveComplexity.IFPLfp.trDef_holds_iff {L : FirstOrder.Language} {d : StepDef (L.sum FirstOrder.Language.order)} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (trDef d).Holds A ↔ d.IFPHolds A

The translated definition means the inflationary definition.

theorem DescriptiveComplexity.IFPDefinable.lfpDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : IFPDefinable P) : LFPDefinable P

Every FO(≤, IFP) definition is an FO(LFP) definition: the hard half of the capture theorem FO(≤, IFP) = PTIME – translate the inflationary iteration into a stage walk with a dual truth/falsity evaluator for the step formulas.

theorem DescriptiveComplexity.ifpDefinable_iff_lfpDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : IFPDefinable P ↔ LFPDefinable P

FO(≤, IFP) = FO(LFP) (Gurevich–Shelah 1986: on ordered structures, and indeed on all structures, the inflationary fixed point adds no power over the least fixed point; here the ordered capture, proved by translation in both directions).

theorem DescriptiveComplexity.ifpDefinable_iff_mem_PTIME {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : IFPDefinable P ↔ PTIME.Mem P

The capture theorem FO(≤, IFP) = PTIME: a problem is FO(≤, IFP) definable exactly when it is in PTIME.