Simultaneous first-order inductions: one skeleton for IFP and PFP

The inflationary (FO(IFP)) and partial (FO(PFP)) fixed-point logics differ in exactly one place – what one application of the step formulas does with the previous stage. Everything else is shared: the data (a block of relation variables, one first-order step formula per variable, an output sentence), the notion of a stage, stabilization on finite structures, transport along isomorphisms, and the pullback along a first-order interpretation. This file provides that shared skeleton; the logics themselves are built on it in DescriptiveComplexity.FixedPointInflationary and DescriptiveComplexity.FixedPointPartial.

The data

A DescriptiveComplexity.StepDef over L bundles a block B of relation variables, one step formula per variable – a first-order formula over L.sum B.lang whose free variables are the arguments of the variable – and an output sentence over the same expanded vocabulary. This is one simultaneous induction with a first-order output; nesting is treated by stratification, in DescriptiveComplexity.FixedPointInflationary.

Unlike DescriptiveComplexity.LFPDef, whose rules are clausal data (the library's Horn-program normal form), the step formulas here are unrestricted: positivity is exactly what the inflationary and partial iterations dispense with. LFPDef keeps its clausal form – the two are bridged in DescriptiveComplexity.FixedPointInflationary (rules give a StepDef) and DescriptiveComplexity.FixedPointInflationaryLFP (the converse translation).

The two iterations

• DescriptiveComplexity.StepDef.inflStage: iterate DescriptiveComplexity.StepDef.inflStep, which accumulates the step formulas into the previous stage. The stages grow, so on a finite structure they reach a fixed point within the atom count (DescriptiveComplexity.StepDef.isFixedPt_inflStep_card – the height of the subset lattice, via DescriptiveComplexity.exists_succ_eq_of_monotone_subset), and their union DescriptiveComplexity.StepDef.inflLimit equals the stage at the atom count (DescriptiveComplexity.StepDef.inflLimit_eq_stage_card).
• DescriptiveComplexity.StepDef.partStage: iterate DescriptiveComplexity.StepDef.next itself, replacing the previous stage. Nothing grows, and the iteration may cycle forever; if some stage is a fixed point, all fixed stages are equal (DescriptiveComplexity.StepDef.partStage_eq_of_isFixedPt) and one is reached within Nat.card of the assignment type – the pigeonhole DescriptiveComplexity.isFixedPt_iterate_card_iff, exposed here as DescriptiveComplexity.StepDef.exists_isFixedPt_partStage_iff.

Transport

Both iterations commute with transporting an assignment along an isomorphism (DescriptiveComplexity.StepDef.inflStage_map, DescriptiveComplexity.StepDef.partStage_map) and with the pullback of the block through a first-order interpretation (DescriptiveComplexity.StepDef.inflStage_pull, DescriptiveComplexity.StepDef.partStage_pull, for the pulled definition DescriptiveComplexity.StepDef.pull). Each is one commuting lemma about DescriptiveComplexity.StepDef.next (next_map, next_pull) propagated along the orbit; these are the lemmas isomorphism-invariance and closure under reductions rest on, for every logic built on this skeleton.

Assignments form a finite type

def DescriptiveComplexity.SOBlock.botAssign (B : SOBlock) (A : Type) : B.Assignment A

The all-empty assignment of a block: the starting point of both iterations.

Equations

• B.botAssign A x✝¹ x✝ = False

theorem DescriptiveComplexity.SOBlock.mapAssign_botAssign (B : SOBlock) {A A' : Type} (e : A ≃ A') : B.mapAssign e (B.botAssign A) = B.botAssign A'

Transport along an equivalence maps the empty assignment to the empty assignment.

instance DescriptiveComplexity.instFiniteAssignment {B : SOBlock} {A : Type} [Finite A] : Finite (B.Assignment A)

Realization transport with explicit structures

The structures a stage is read against are block expansions, which are not instances; this is FirstOrder.Language.StrongHomClass.realize_formula with the two structures passed explicitly, exactly as DescriptiveComplexity.realize_sentence_of_equiv does at the sentence level.

theorem DescriptiveComplexity.realize_formula_of_equiv {L' : FirstOrder.Language} {M N α : Type} {instM : L'.Structure M} {instN : L'.Structure N} (e : L'.Equiv M N) (φ : L'.Formula α) (v : α → M) : (φ.Realize fun (a : α) => e (v a)) ↔ φ.Realize v

The data of a simultaneous induction

structure DescriptiveComplexity.StepDef (L : FirstOrder.Language) : Type 1

A simultaneous first-order induction: a block of relation variables, one first-order step formula per variable – over the base vocabulary expanded by the block, its free variables the arguments of the variable – and an output sentence over the same expanded vocabulary, read at the value of the iteration. The step formulas are unrestricted; which iteration is applied to them (inflationary or partial) is chosen by the logics built on this data.

• B : SOBlock

  The relation variables computed by the iteration.

• step (i : self.B.ι) : (L.sum self.B.lang).Formula (Fin (self.B.arity i))

  The step formula of each variable; its free variables are the arguments of the variable.

• out : (L.sum self.B.lang).Sentence

  The first-order output, over the expanded vocabulary – unrestricted, in particular free to negate fixed-point atoms.

def DescriptiveComplexity.StepDef.next {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (ρ : d.B.Assignment A) : d.B.Assignment A

One application of the step formulas to an assignment.

Equations

• d.next ρ i x = (d.step i).Realize x

def DescriptiveComplexity.StepDef.inflStep {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (ρ : d.B.Assignment A) : d.B.Assignment A

The inflationary step: accumulate the step formulas into the previous stage.

Equations

• d.inflStep ρ i x = (ρ i x ∨ d.next ρ i x)

def DescriptiveComplexity.StepDef.inflStage {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] (n : ℕ) : d.B.Assignment A

The stages of the inflationary iteration.

Equations

• d.inflStage A n = d.inflStep^[n] (d.B.botAssign A)

def DescriptiveComplexity.StepDef.partStage {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] (n : ℕ) : d.B.Assignment A

The stages of the partial iteration.

Equations

• d.partStage A n = d.next^[n] (d.B.botAssign A)

def DescriptiveComplexity.StepDef.inflLimit {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] : d.B.Assignment A

The value of the inflationary iteration: the union of the stages. On a finite structure this is the stage at the atom count (DescriptiveComplexity.StepDef.inflLimit_eq_stage_card).

Equations

• d.inflLimit A i x = ∃ (n : ℕ), d.inflStage A n i x

theorem DescriptiveComplexity.StepDef.inflStage_succ {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (n : ℕ) : d.inflStage A (n + 1) = d.inflStep (d.inflStage A n)

theorem DescriptiveComplexity.StepDef.partStage_succ {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (n : ℕ) : d.partStage A (n + 1) = d.next (d.partStage A n)

theorem DescriptiveComplexity.StepDef.inflStage_le_succ {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] (n : ℕ) (i : d.B.ι) (x : Fin (d.B.arity i) → A) (h : d.inflStage A n i x) : d.inflStage A (n + 1) i x

The inflationary stages increase.

theorem DescriptiveComplexity.StepDef.inflStage_le_of_le {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] {m n : ℕ} (hmn : m ≤ n) (i : d.B.ι) (x : Fin (d.B.arity i) → A) (h : d.inflStage A m i x) : d.inflStage A n i x

The inflationary stages increase, monotonically.

theorem DescriptiveComplexity.StepDef.partStage_eq_of_isFixedPt {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] {m n : ℕ} (hm : Function.IsFixedPt d.next (d.partStage A m)) (hn : Function.IsFixedPt d.next (d.partStage A n)) : d.partStage A m = d.partStage A n

Two partial stages that are both fixed points of the step are equal: the value of a converging partial iteration does not depend on which stable stage witnesses the convergence.

Stabilization on finite structures

theorem DescriptiveComplexity.StepDef.exists_inflStage_succ_eq {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] [Finite A] : ∃ N ≤ Nat.card (BAtom d.B A), d.inflStage A (N + 1) = d.inflStage A N

The inflationary stages plateau within the atom count.

theorem DescriptiveComplexity.StepDef.isFixedPt_inflStep_card {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] [Finite A] : Function.IsFixedPt d.inflStep (d.inflStage A (Nat.card (BAtom d.B A)))

The inflationary iteration reaches a fixed point within the atom count – the height of the subset lattice of the block's atoms, not the number of assignments.

theorem DescriptiveComplexity.StepDef.inflStage_eq_of_card_le {L : FirstOrder.Language} (d : StepDef L) {A : Type} [L.Structure A] [Finite A] {n : ℕ} (hn : Nat.card (BAtom d.B A) ≤ n) : d.inflStage A n = d.inflStage A (Nat.card (BAtom d.B A))

The inflationary stages are constant from the atom count on.

theorem DescriptiveComplexity.StepDef.inflLimit_eq_stage_card {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] [Finite A] : d.inflLimit A = d.inflStage A (Nat.card (BAtom d.B A))

On a finite structure, the value of the inflationary iteration is the stage at the atom count.

theorem DescriptiveComplexity.StepDef.isFixedPt_inflStep_inflLimit {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] [Finite A] : Function.IsFixedPt d.inflStep (d.inflLimit A)

The value of the inflationary iteration is a fixed point of the inflationary step.

theorem DescriptiveComplexity.StepDef.exists_isFixedPt_partStage_iff {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] [Finite A] : (∃ (n : ℕ), Function.IsFixedPt d.next (d.partStage A n)) ↔ Function.IsFixedPt d.next (d.partStage A (Nat.card (d.B.Assignment A)))

If the partial iteration converges at all, it converges within the number of assignments of the block – the pigeonhole DescriptiveComplexity.isFixedPt_iterate_card_iff read on the stages.

Transport along isomorphisms

theorem DescriptiveComplexity.StepDef.next_map {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (ρ : d.B.Assignment M) : d.next (d.B.mapAssign e.toEquiv ρ) = d.B.mapAssign e.toEquiv (d.next ρ)

One application of the step formulas commutes with transporting the assignment along an isomorphism: the step formulas cannot tell isomorphic expanded structures apart.

theorem DescriptiveComplexity.StepDef.inflStep_map {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (ρ : d.B.Assignment M) : d.inflStep (d.B.mapAssign e.toEquiv ρ) = d.B.mapAssign e.toEquiv (d.inflStep ρ)

The inflationary step commutes with transport along an isomorphism.

theorem DescriptiveComplexity.StepDef.inflStage_map {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (n : ℕ) : d.inflStage N n = d.B.mapAssign e.toEquiv (d.inflStage M n)

The inflationary stages transport along an isomorphism.

theorem DescriptiveComplexity.StepDef.partStage_map {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (n : ℕ) : d.partStage N n = d.B.mapAssign e.toEquiv (d.partStage M n)

The partial stages transport along an isomorphism.

theorem DescriptiveComplexity.StepDef.inflLimit_map {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) : d.inflLimit N = d.B.mapAssign e.toEquiv (d.inflLimit M)

The value of the inflationary iteration transports along an isomorphism.

theorem DescriptiveComplexity.StepDef.isFixedPt_next_map_iff {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (ρ : d.B.Assignment M) : Function.IsFixedPt d.next (d.B.mapAssign e.toEquiv ρ) ↔ Function.IsFixedPt d.next ρ

Being a fixed point of the step is insensitive to transporting the assignment along an isomorphism.

Pullback through an interpretation

theorem DescriptiveComplexity.SOBlock.pullAssign_botAssign (B : SOBlock) {Tag : Type} [Finite Tag] {dm : ℕ} {A : Type} : B.pullAssign (B.botAssign (Tag × (Fin dm → A))) = (pull Tag dm B).botAssign A

Pulling back the empty assignment gives the empty assignment.

noncomputable def DescriptiveComplexity.StepDef.pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (dd : StepDef L₂) (I : FOInterpretation L₁ L₂ Tag dm) : StepDef L₁

The pullback of a simultaneous induction through a tagged interpretation: the block is pulled back variable by variable (DescriptiveComplexity.SOBlock.pull), the step formula of a pulled variable is the pullback of the original variable's step formula at the pulled variable's tag tuple (DescriptiveComplexity.guardPull, through the extended interpretation DescriptiveComplexity.FOInterpretation.extendSO), and the output sentence is pulled through the extended interpretation.

Equations

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

theorem DescriptiveComplexity.StepDef.next_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (I : FOInterpretation L₁ L₂ Tag dm) (dd : StepDef L₂) {A : Type} [L₁.Structure A] (ρ : dd.B.Assignment (I.Map A)) : (dd.pull I).next (dd.B.pullAssign ρ) = dd.B.pullAssign (dd.next ρ)

One application of the pulled step formulas is the pullback of one application of the original ones: the single commuting square from which every transport of the iterations along a reduction follows.

theorem DescriptiveComplexity.StepDef.inflStep_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (I : FOInterpretation L₁ L₂ Tag dm) (dd : StepDef L₂) {A : Type} [L₁.Structure A] (ρ : dd.B.Assignment (I.Map A)) : (dd.pull I).inflStep (dd.B.pullAssign ρ) = dd.B.pullAssign (dd.inflStep ρ)

The inflationary step commutes with the pullback.

theorem DescriptiveComplexity.StepDef.inflStage_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (I : FOInterpretation L₁ L₂ Tag dm) (dd : StepDef L₂) (A : Type) [L₁.Structure A] (n : ℕ) : (dd.pull I).inflStage A n = dd.B.pullAssign (dd.inflStage (I.Map A) n)

The inflationary stages of the pulled induction are the pullbacks of the original stages.

theorem DescriptiveComplexity.StepDef.partStage_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (I : FOInterpretation L₁ L₂ Tag dm) (dd : StepDef L₂) (A : Type) [L₁.Structure A] (n : ℕ) : (dd.pull I).partStage A n = dd.B.pullAssign (dd.partStage (I.Map A) n)

The partial stages of the pulled induction are the pullbacks of the original stages.

theorem DescriptiveComplexity.StepDef.inflLimit_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (I : FOInterpretation L₁ L₂ Tag dm) (dd : StepDef L₂) (A : Type) [L₁.Structure A] : (dd.pull I).inflLimit A = dd.B.pullAssign (dd.inflLimit (I.Map A))

The value of the pulled inflationary iteration is the pullback of the original value.

theorem DescriptiveComplexity.StepDef.isFixedPt_next_pull_iff {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {dm : ℕ} (I : FOInterpretation L₁ L₂ Tag dm) (dd : StepDef L₂) {A : Type} [L₁.Structure A] (ρ : dd.B.Assignment (I.Map A)) : Function.IsFixedPt (dd.pull I).next (dd.B.pullAssign ρ) ↔ Function.IsFixedPt dd.next ρ

Being a fixed point of the step is insensitive to pulling the assignment back: the pullback of assignments is a bijection (DescriptiveComplexity.SOBlock.mergeAssign_pullAssign) intertwining the two steps.