FO(IFP): first-order logic with an inflationary fixed point

The inflationary fixed-point logic (Gurevich–Shelah 1986; Abiteboul–Vianu 1989; Ebbinghaus–Flum 1995, ch. 7): iterate the step formulas of a DescriptiveComplexity.StepDef inflationarily – each stage accumulates what the step formulas derive on top of the previous stage – and read the output sentence at the limit. No positivity is required of the step formulas: inflation makes the iteration monotone whatever they are, which is the whole point of the logic.

Two definability notions result, and keeping them distinct is the entire subject of the Abiteboul–Vianu theorem:

• DescriptiveComplexity.IFPDefinableFree – over the bare vocabulary, on unordered structures;
• DescriptiveComplexity.IFPDefinable – over the vocabulary expanded by an order, required for every linear order on the universe, the problem itself never seeing it. This is the setting of the capture theorem FO(≤, IFP) = PTIME (DescriptiveComplexity.FixedPointInflationaryLFP).

For SO(TC) the corresponding two notions coincide (DescriptiveComplexity.sotcDefinable_iff_free): a walk can guess an order into its state. Here they must not be conflated – an inflationary induction cannot manufacture an order (its stages are isomorphism-invariant, so on a bare set of n elements nothing asymmetric is ever derived), and the gap between the two notions is precisely what makes the unordered Abiteboul–Vianu theorem (DescriptiveComplexity.AbiteboulVianu) a theorem about P = PSPACE rather than a triviality.

Relation to FO(LFP), and why Gurevich–Shelah is not needed

DescriptiveComplexity.LFPDefinable.ifpDefinable embeds FO(LFP) into ordered FO(IFP): the rules of a Horn program, read as one simultaneous step (DescriptiveComplexity.hornStepF), form a StepDef whose inflationary stages are exactly the derivation stages DescriptiveComplexity.derivesIn (DescriptiveComplexity.inflStage_toStepDef). The converse translation – FO(≤, IFP) back into FO(LFP), hence the capture of PTIME – is DescriptiveComplexity.FixedPointInflationaryLFP.

This library states the Abiteboul–Vianu theorem for IFP versus PFP, as in Abiteboul and Vianu's original form. The classical statement for least fixed points on unordered structures needs Gurevich–Shelah (order-free LFP = IFP, by stage comparison) on top; phrasing the theorem with IFP makes that machinery unnecessary, a design decision, not an omission.

Closure properties

FO(IFP) definability is closed under complement by construction (DescriptiveComplexity.IFPDefinable.compl – negate the output), and under (ordered) first-order reductions (DescriptiveComplexity.IFPDefinableFree.of_foReduction, DescriptiveComplexity.IFPDefinable.of_orderedReduction): the stages commute with the pullback of the block (DescriptiveComplexity.StepDef.inflStage_pull) and the output sentence pulls back through the extended interpretation, exactly as for FO(LFP). The notion is class-worthy in the sense of DescriptiveComplexity.ComplexityClass.

The value of an inflationary definition

def DescriptiveComplexity.StepDef.IFPHolds {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] : Prop

The value of a simultaneous induction read inflationarily: the output sentence, at the limit of the inflationary iteration.

Equations

• d.IFPHolds A = A ⊨ d.out

def DescriptiveComplexity.StepDef.not {L : FirstOrder.Language} (d : StepDef L) : StepDef L

Negating the output complements the defined property: FO(IFP) is closed under complement by construction, being a logic rather than a fragment.

Equations

• d.not = { B := d.B, step := d.step, out := FirstOrder.Language.BoundedFormula.not d.out }

theorem DescriptiveComplexity.StepDef.ifpHolds_not {L : FirstOrder.Language} (d : StepDef L) (A : Type) [L.Structure A] : d.not.IFPHolds A ↔ ¬d.IFPHolds A

theorem DescriptiveComplexity.StepDef.ifpHolds_equiv {L : FirstOrder.Language} (d : StepDef L) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) : d.IFPHolds M ↔ d.IFPHolds N

The value of an inflationary definition is isomorphism-invariant.

Definability, ordered and order-free

def DescriptiveComplexity.IFPDefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is order-free FO(IFP) definable if, on nonempty finite structures, it is the value of a simultaneous induction over its own vocabulary, read inflationarily. This is the unordered notion the Abiteboul–Vianu theorem is about; the capture theorem for PTIME instead uses the ordered DescriptiveComplexity.IFPDefinable.

Equations

• DescriptiveComplexity.IFPDefinableFree P = ∃ (d : DescriptiveComplexity.StepDef L), ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ d.IFPHolds A

def DescriptiveComplexity.IFPDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is FO(≤, IFP) definable if, on nonempty finite ordered structures, it is the value of a simultaneous induction over the ordered expansion of its vocabulary, read inflationarily. As everywhere in this library, the equivalence is required for every linear order, so the notion is order-invariant: the formulas see the order, the problem does not.

Equations

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

theorem DescriptiveComplexity.ifpDefinableFree_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : IFPDefinableFree P ↔ IFPDefinableFree Q

Order-free FO(IFP) definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.ifpDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : IFPDefinable P ↔ IFPDefinable Q

FO(≤, IFP) definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.IFPDefinableFree.compl {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : IFPDefinableFree P) : IFPDefinableFree Pᶜ

Order-free FO(IFP) definability is closed under complement: negate the output formula.

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

FO(≤, IFP) definability is closed under complement: negate the output formula.

Closure under reductions

theorem DescriptiveComplexity.IFPDefinableFree.of_foReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : FOReduction P Q) (h : IFPDefinableFree Q) : IFPDefinableFree P

Order-free FO(IFP) definability is closed under first-order reductions: pull the induction back through the interpretation (DescriptiveComplexity.StepDef.pull); the inflationary limit commutes with the pullback (DescriptiveComplexity.StepDef.inflLimit_pull) and the output sentence pulls back through the extended interpretation.

theorem DescriptiveComplexity.IFPDefinable.of_orderedReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : OrderedFOReduction P Q) (h : IFPDefinable Q) : IFPDefinable P

FO(≤, IFP) definability is closed under ordered first-order reductions. The induction pulls back through the order-extended interpretation; the two readings of the interpreted ordered structure are identified by DescriptiveComplexity.FOInterpretation.ordExtendLEquiv, along which the inflationary limit transports (DescriptiveComplexity.StepDef.inflLimit_map).

theorem DescriptiveComplexity.IFPDefinable.of_foReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : FOReduction P Q) (h : IFPDefinable Q) : IFPDefinable P

FO(≤, IFP) definability is closed under plain first-order reductions, which are in particular ordered ones.

Horn rules as one simultaneous inflationary step

The rules of an FO(LFP) definition, read as a single simultaneous step: the step formula of the variable i says that some rule with head i fires – its guard holds and its body atoms are in the current stage – with the head's arguments instantiated at the free variables. Iterated inflationarily, the stages are exactly the derivation stages DescriptiveComplexity.derivesIn, so the limit is the least fixed point and FO(LFP) embeds into FO(≤, IFP) (DescriptiveComplexity.LFPDefinable.ifpDefinable). The step formulas produced here are positive in the block – inflation just does not care.

@[reducible, inline]

abbrev DescriptiveComplexity.varInSym (L : FirstOrder.Language) (B : SOBlock) (i : B.ι) : (L.sum B.lang).Relations (B.arity i)

The relation symbol of a block variable, in the expanded vocabulary L.sum B.lang (the generic-L sibling of DescriptiveComplexity.varOutSym).

Equations

• DescriptiveComplexity.varInSym L B i = Sum.inr (DescriptiveComplexity.varSym B i)

noncomputable def DescriptiveComplexity.bodyAtomF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (b : SOAtom B k) {n : ℕ} : (L.sum B.lang).Formula (Fin n ⊕ Fin k)

A second-order body atom, as a formula over the expanded vocabulary; its arguments are read from the rule-variable component.

Equations

• DescriptiveComplexity.bodyAtomF b = (DescriptiveComplexity.varInSym L B b.idx).formula fun (j : Fin (B.arity b.idx)) => FirstOrder.Language.var (Sum.inr (b.args j))

noncomputable def DescriptiveComplexity.guardStepF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (φ : L.Formula (Fin k)) {n : ℕ} : (L.sum B.lang).Formula (Fin n ⊕ Fin k)

A guard, transported to the expanded vocabulary, over head-argument and rule variables.

Equations

• DescriptiveComplexity.guardStepF φ = FirstOrder.Language.Formula.relabel Sum.inr (FirstOrder.Language.LHom.sumInl.onFormula φ)

noncomputable def DescriptiveComplexity.ruleStepF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (c : HornClause L B k) (i : B.ι) : (L.sum B.lang).Formula (Fin (B.arity i) ⊕ Fin k)

The contribution of one rule to the step formula of the variable i: the rule's head is about i, its arguments are the free variables, its guard holds, and its body atoms are in the current stage.

Equations

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

noncomputable def DescriptiveComplexity.hornStepF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (rules : List (HornClause L B k)) (i : B.ι) : (L.sum B.lang).Formula (Fin (B.arity i))

The step formula of the variable i induced by a list of rules: some rule with head i fires, for some values of the rule variables.

Equations

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

theorem DescriptiveComplexity.realize_bodyAtomF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (ρ : B.Assignment A) (b : SOAtom B k) {n : ℕ} (w : Fin n ⊕ Fin k → A) : (bodyAtomF b).Realize w ↔ b.Holds ρ fun (q : Fin k) => w (Sum.inr q)

theorem DescriptiveComplexity.realize_guardStepF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (ρ : B.Assignment A) (φ : L.Formula (Fin k)) {n : ℕ} (w : Fin n ⊕ Fin k → A) : (guardStepF φ).Realize w ↔ φ.Realize fun (q : Fin k) => w (Sum.inr q)

theorem DescriptiveComplexity.realize_hornStepF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (ρ : B.Assignment A) (rules : List (HornClause L B k)) (i : B.ι) (x : Fin (B.arity i) → A) : (hornStepF rules i).Realize x ↔ stepDerives rules (fun (q : BAtom B A) => ρ q.fst q.snd) ⟨i, x⟩

The step formula induced by a list of rules realizes as one round of rule application (DescriptiveComplexity.stepDerives).

FO(LFP) embeds into FO(≤, IFP)

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

The simultaneous induction induced by an FO(LFP) definition: same block, the rules read as one simultaneous step, same output.

Equations

• d.toStepDef = { B := d.B, step := fun (i : d.B.ι) => DescriptiveComplexity.hornStepF d.rules i, out := d.out }

theorem DescriptiveComplexity.inflStage_toStepDef {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] (n : ℕ) : d.toStepDef.inflStage A n = fun (i : d.B.ι) (x : Fin (d.B.arity i) → A) => derivesIn d.rules n ⟨i, x⟩

The inflationary stages of the induced induction are the derivation stages of the rules.

theorem DescriptiveComplexity.inflLimit_toStepDef {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] : d.toStepDef.inflLimit A = lfpAssign d.rules

The value of the induced inflationary iteration is the least fixed point of the rules.

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

Every FO(LFP) definition is an FO(≤, IFP) definition: read the rules as one simultaneous step; inflation iterates them to their least fixed point, and the output survives unchanged. (The converse, closing the circle back into FO(LFP), is DescriptiveComplexity.FixedPointInflationaryLFP.)