FO(LFP): first-order logic with a least fixed point

The logic FO(LFP) (Immerman 1986; Vardi 1982), in the clausal normal form this library uses for kernels everywhere else: a DescriptiveComplexity.LFPDef bundles

• a block of relation variables and a finite list of rules deriving them – the same DescriptiveComplexity.HornClause data as an SO-Horn program, read here as an inductive definition rather than a constraint;
• an arbitrary first-order output sentence over the input vocabulary expanded by those variables, evaluated at the least fixed point.

Why the output formula is the point

The fixed point is the same object in both logics – the least model of a set of rules. What distinguishes FO(LFP) from SO-Horn is what one is allowed to say about it. An SO-Horn program can only reject models, through goal clauses, and a goal clause tests its atoms positively; FO(LFP) evaluates an unrestricted first-order sentence, so it may negate fixed-point atoms.

That is exactly the closure that SO-Horn lacks: DescriptiveComplexity.LFPDefinable is closed under complement by negating the output (DescriptiveComplexity.LFPDefinable.compl, a one-liner), whereas the corresponding statement for SO-Horn is open – see DescriptiveComplexity.Problems.HornSat. The inclusion DescriptiveComplexity.SigmaSOHornDefinable.lfpDefinable transports every SO-Horn definition into this logic, so PTIME as defined by the Horn fragment sits inside FO(LFP) together with its complements.

What is proved here, and where the equivalence is completed

DescriptiveComplexity.SigmaSOHornDefinable.lfpDefinable is one half of the equivalence of the two formalisms: every SO-Horn definition is an FO(LFP) definition. The other half – bringing an FO(LFP) definition back into the Horn fragment – is the translation of DescriptiveComplexity.FixedPointHorn, built on the stage theory of this file: the stages DescriptiveComplexity.derivesIn stabilize once the atom count is reached (DescriptiveComplexity.derivesIn_iff_derives_of_card_le), so a stage indexed by a large enough tuple stands in for the fixed point, and its complement can be derived positively, one stage at a time. Together the two halves make the notions interchangeable (DescriptiveComplexity.lfpDefinable_iff_sigmaSOHornDefinable) and give PiP 0 = SigmaP 0 (DescriptiveComplexity.piP_zero_eq).

The notion is also closed under (ordered) first-order reductions (DescriptiveComplexity.LFPDefinable.of_orderedReduction), so it is class-worthy in the sense of DescriptiveComplexity.ComplexityClass.

A second consumer of the stage theory is not formalized: a Σ₁ definition, giving FO(LFP) ⊆ NP directly, would guess a fixed point together with a well-founded derivation order and check both first-order. The semantic key is provided here – DescriptiveComplexity.derives_eq_of_closed_of_wf says that a relation closed under the rules and well-foundedly derivable is exactly the least fixed point, DescriptiveComplexity.derives_step_of_depth supplies the witnessing order from the stages, and DescriptiveComplexity.LFPDef.holds_iff_of_certificate packages this – but the formula building remains to be done. (The inclusion itself already follows by composing the translation with the Horn membership of DescriptiveComplexity.Problems.HornSat.)

The fixed point

Rather than a stage-indexed iteration, the least model is the inductive predicate DescriptiveComplexity.Derives: a tuple is derived when some rule fires on already-derived tuples. Being an inductive definition it comes with exactly the two properties a least fixed point needs – it satisfies the rules (DescriptiveComplexity.lfpAssign_rule) and it is contained in every assignment that does (DescriptiveComplexity.lfpAssign_least).

Rules whose head is none derive nothing and are simply inert here, so an SO-Horn program can be handed over unchanged: its goal clauses reappear in the output formula.

The least model of a rule system

inductive DescriptiveComplexity.Derives {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] (rules : List (HornClause Lg B k)) : (i : B.ι) × (Fin (B.arity i) → A) → Prop

The tuples derivable by a system of rules: the least fixed point, as an inductive predicate. A rule fires when its guard holds and all its body atoms are already derived, and it derives its head atom.

• rule {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {c : HornClause Lg B k} (hc : c ∈ rules) {a : SOAtom B k} (ha : c.head = some a) {v : Fin k → A} (hg : c.guard.Realize v) (hb : ∀ b ∈ c.body, Derives rules ⟨b.idx, fun (j : Fin (B.arity b.idx)) => v (b.args j)⟩) : Derives rules ⟨a.idx, fun (j : Fin (B.arity a.idx)) => v (a.args j)⟩

def DescriptiveComplexity.lfpAssign {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] (rules : List (HornClause Lg B k)) : B.Assignment A

The least fixed point of a rule system, as an assignment of the block.

Equations

• DescriptiveComplexity.lfpAssign rules i x = DescriptiveComplexity.Derives rules ⟨i, x⟩

theorem DescriptiveComplexity.lfpAssign_rule {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {c : HornClause Lg B k} (hc : c ∈ rules) {a : SOAtom B k} (ha : c.head = some a) (v : Fin k → A) : c.Holds (lfpAssign rules) v

The least fixed point satisfies every rule with a head. (A clause with no head is a constraint, not a rule: it derives nothing, and is what the output formula of DescriptiveComplexity.LFPDef takes over.)

theorem DescriptiveComplexity.lfpAssign_least_of_closed {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {ρ : B.Assignment A} (hρ : ∀ c ∈ rules, ∀ (a : SOAtom B k), c.head = some a → ∀ (v : Fin k → A), c.guard.Realize v → (∀ b ∈ c.body, b.Holds ρ v) → a.Holds ρ v) {p : (i : B.ι) × (Fin (B.arity i) → A)} (hp : Derives rules p) : ρ p.fst p.snd

The least fixed point is contained in every prefixpoint: in every assignment closed under the rules.

theorem DescriptiveComplexity.lfpAssign_least {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {ρ : B.Assignment A} (hρ : ∀ (v : Fin k → A), ∀ c ∈ rules, c.Holds ρ v) {p : (i : B.ι) × (Fin (B.arity i) → A)} (hp : Derives rules p) : ρ p.fst p.snd

The least fixed point is contained in every assignment satisfying the rules.

Stages, depth, and the certificate characterization

Putting FO(LFP) back into the Horn fragment, and certifying a fixed point in Σ₁, both need the same thing: a way to say “this relation is the least fixed point” that a positive formalism can test. Closure alone is not enough (anything larger is closed too); what pins the least fixed point down is closure together with well-founded derivability – every element derived by a rule from strictly earlier elements. That is DescriptiveComplexity.derives_eq_of_closed_of_wf below, and the stages provide the witnessing order.

@[reducible, inline]

abbrev DescriptiveComplexity.BAtom (B : SOBlock) (A : Type) : Type

The atoms of a block over a structure: a relation variable and a tuple.

Equations

• DescriptiveComplexity.BAtom B A = ((i : B.ι) × (Fin (B.arity i) → A))

def DescriptiveComplexity.stepDerives {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] (rules : List (HornClause Lg B k)) (S : BAtom B A → Prop) : BAtom B A → Prop

One application of the rules to a set of atoms.

Equations

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

def DescriptiveComplexity.derivesIn {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] (rules : List (HornClause Lg B k)) : ℕ → BAtom B A → Prop

The stages of the derivation: what is derivable in at most n rounds.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.derivesIn rules 0 = fun (x : DescriptiveComplexity.BAtom B A) => False

theorem DescriptiveComplexity.derivesIn_succ {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {n : ℕ} {q : BAtom B A} (h : derivesIn rules n q) : derivesIn rules (n + 1) q

theorem DescriptiveComplexity.derivesIn_le {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {m n : ℕ} (hmn : m ≤ n) {q : BAtom B A} (h : derivesIn rules m q) : derivesIn rules n q

theorem DescriptiveComplexity.derives_iff_derivesIn {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {q : BAtom B A} : Derives rules q ↔ ∃ (n : ℕ), derivesIn rules n q

The stages exhaust the least fixed point.

Depth, and the certificate

noncomputable def DescriptiveComplexity.depth {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] (rules : List (HornClause Lg B k)) (q : BAtom B A) : ℕ

The stage at which an atom first appears.

Equations

• DescriptiveComplexity.depth rules q = sInf {n : ℕ | DescriptiveComplexity.derivesIn rules n q}

theorem DescriptiveComplexity.derivesIn_depth {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {q : BAtom B A} (h : Derives rules q) : derivesIn rules (depth rules q) q

theorem DescriptiveComplexity.depth_le {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {n : ℕ} {q : BAtom B A} (h : derivesIn rules n q) : depth rules q ≤ n

theorem DescriptiveComplexity.derives_step_of_depth {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {q : BAtom B A} (h : Derives rules q) : ∃ c ∈ rules, ∃ (a : SOAtom B k), c.head = some a ∧ ∃ (v : Fin k → A), q = ⟨a.idx, fun (j : Fin (B.arity a.idx)) => v (a.args j)⟩ ∧ c.guard.Realize v ∧ ∀ b ∈ c.body, Derives rules ⟨b.idx, fun (j : Fin (B.arity b.idx)) => v (b.args j)⟩ ∧ depth rules ⟨b.idx, fun (j : Fin (B.arity b.idx)) => v (b.args j)⟩ < depth rules q

Every derived atom is derived from atoms of strictly smaller depth: the least fixed point comes with a well-founded derivation order.

Stabilization: the stages close within Nat.card many rounds

On a finite structure the stages are an increasing chain of subsets of the finitely many atoms, so they stabilize by the time the atom count is reached – after that many rounds, DescriptiveComplexity.derivesIn is the least fixed point. This is what lets a stage indexed by a large enough tuple stand in for the fixed point itself in DescriptiveComplexity.FixedPointHorn.

theorem DescriptiveComplexity.derivesIn_iff_derives_of_card_le {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] [Finite A] {rules : List (HornClause Lg B k)} {r : ℕ} (hr : Nat.card (BAtom B A) ≤ r) {q : BAtom B A} : derivesIn rules r q ↔ Derives rules q

The stages stabilize at the atom count: after Nat.card (BAtom B A) many rounds, being derivable within that many rounds is being derivable.

theorem DescriptiveComplexity.derives_eq_of_closed_of_wf {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [Lg.Structure A] {rules : List (HornClause Lg B k)} {R : BAtom B A → Prop} {lt : BAtom B A → BAtom B A → Prop} (hwf : WellFounded lt) (hclosed : ∀ c ∈ rules, ∀ (a : SOAtom B k), c.head = some a → ∀ (v : Fin k → A), c.guard.Realize v → (∀ b ∈ c.body, R ⟨b.idx, fun (j : Fin (B.arity b.idx)) => v (b.args j)⟩) → R ⟨a.idx, fun (j : Fin (B.arity a.idx)) => v (a.args j)⟩) (hderiv : ∀ (q : BAtom B A), R q → ∃ c ∈ rules, ∃ (a : SOAtom B k), c.head = some a ∧ ∃ (v : Fin k → A), q = ⟨a.idx, fun (j : Fin (B.arity a.idx)) => v (a.args j)⟩ ∧ c.guard.Realize v ∧ ∀ b ∈ c.body, R ⟨b.idx, fun (j : Fin (B.arity b.idx)) => v (b.args j)⟩ ∧ lt ⟨b.idx, fun (j : Fin (B.arity b.idx)) => v (b.args j)⟩ q) (q : BAtom B A) : R q ↔ Derives rules q

The certificate characterization: a relation closed under the rules and all of whose atoms are derived from strictly ≺-earlier ones, for a well-founded ≺, is the least fixed point.

This is what makes the least fixed point testable by a positive formalism: it is the shape a Σ₁ certificate for FO(LFP) would check. (The translation back into the Horn fragment, DescriptiveComplexity.FixedPointHorn, instead walks the stages directly, through their stabilization DescriptiveComplexity.derivesIn_iff_derives_of_card_le below.)

The fixed point transports along isomorphisms

theorem DescriptiveComplexity.derives_map {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [Lg.Structure M] [Lg.Structure N] (e : Lg.Equiv M N) {rules : List (HornClause Lg B k)} {q : BAtom B M} (h : Derives rules q) : Derives rules ⟨q.fst, fun (j : Fin (B.arity q.fst)) => e (q.snd j)⟩

Derivability transports along an isomorphism of structures: the rules only see the guards, which an isomorphism preserves.

theorem DescriptiveComplexity.lfpAssign_map {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [Lg.Structure M] [Lg.Structure N] (e : Lg.Equiv M N) (rules : List (HornClause Lg B k)) : lfpAssign rules = B.mapAssign e.toEquiv (lfpAssign rules)

The least fixed point transports along an isomorphism.

The fixed point commutes with pullbacks

The least fixed point of the pulled rules is the pullback of the least fixed point: both inclusions are an application of leastness, since each side is closed under the other's rules (DescriptiveComplexity.HornProgram.pull_holds). This is the fixed-point half of closure of DescriptiveComplexity.LFPDefinable under (ordered) first-order reductions; what remains for that closure is to pull the output sentence back, through DescriptiveComplexity.FOInterpretation.extendSO and DescriptiveComplexity.FOInterpretation.ordExtendLEquiv, which is bookkeeping between the three structures involved rather than mathematics.

theorem DescriptiveComplexity.lfpAssign_pull {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {Tag : Type} [Finite Tag] {d : ℕ} {B : SOBlock} {k : ℕ} {A : Type} [L₁.Structure A] (I : FOInterpretation L₁ L₂ Tag d) (rules : List (HornClause L₂ B k)) : lfpAssign (HornProgram.pull I rules) = B.pullAssign (lfpAssign rules)

Definitions in FO(LFP)

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

A definition in FO(LFP), in clausal normal form: a block of relation variables, a list of rules defining them inductively, and a first-order output sentence over the vocabulary expanded by the variables, read at the least fixed point.

• B : SOBlock

  The relation variables computed by the fixed point.

• k : ℕ

  The number of first-order variables shared by the rules.

• rules : List (HornClause (L.sum FirstOrder.Language.order) self.B self.k)

  The rules defining the variables. Rules with no head derive nothing.

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

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

def DescriptiveComplexity.LFPDef.Holds {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] : Prop

The value of a definition on a structure: the output read at the least fixed point of the rules.

Equations

• d.Holds A = A ⊨ d.out

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

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

Equations

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

theorem DescriptiveComplexity.LFPDef.holds_not {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] : d.not.Holds A ↔ ¬d.Holds A

theorem DescriptiveComplexity.LFPDef.holds_iff_of_certificate {L : FirstOrder.Language} (d : LFPDef L) {A : Type} [L.Structure A] [LinearOrder A] {ρ : d.B.Assignment A} {lt : BAtom d.B A → BAtom d.B A → Prop} (hwf : WellFounded lt) (hclosed : ∀ c ∈ d.rules, ∀ (a : SOAtom d.B d.k), c.head = some a → ∀ (v : Fin d.k → A), c.guard.Realize v → (∀ b ∈ c.body, b.Holds ρ v) → a.Holds ρ v) (hderiv : ∀ (q : BAtom d.B A), ρ q.fst q.snd → ∃ c ∈ d.rules, ∃ (a : SOAtom d.B d.k), c.head = some a ∧ ∃ (v : Fin d.k → A), q = ⟨a.idx, fun (j : Fin (d.B.arity a.idx)) => v (a.args j)⟩ ∧ c.guard.Realize v ∧ ∀ b ∈ c.body, (ρ b.idx fun (j : Fin (d.B.arity b.idx)) => v (b.args j)) ∧ lt ⟨b.idx, fun (j : Fin (d.B.arity b.idx)) => v (b.args j)⟩ q) : d.Holds A ↔ A ⊨ d.out

A certified fixed point can be used in place of the real one. If ρ is closed under the rules and every one of its atoms is derived from ≺-earlier ones, for a well-founded ≺, then reading the output at ρ gives the value of the definition.

This is the interface a Σ₁ definition of an FO(LFP) definable problem would consume: guess ρ and ≺ and check these conditions first-order, ≺ coming from the stages (DescriptiveComplexity.derives_step_of_depth). The translation into the Horn fragment (DescriptiveComplexity.FixedPointHorn) instead derives the stages themselves.

def DescriptiveComplexity.LFPDefinable {L : FirstOrder.Language} (P : DecisionProblem L) : Prop

A decision problem is FO(LFP) definable if, on nonempty finite ordered structures, it is the value of a definition in FO(LFP). As for DescriptiveComplexity.SigmaSOHornDefinable, the equivalence is required for every linear order, so the notion is order-invariant.

Equations

• DescriptiveComplexity.LFPDefinable P = ∃ (d : DescriptiveComplexity.LFPDef L), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ d.Holds A

theorem DescriptiveComplexity.LFPDefinable.compl {L : FirstOrder.Language} {P : DecisionProblem L} (h : LFPDefinable P) : LFPDefinable Pᶜ

FO(LFP) definability is closed under complement. This is the one line that the Horn fragment cannot supply, and the reason to have the logic at all: negate the output formula.

SO-Horn definitions are FO(LFP) definitions

A Horn program splits into its rules (the clauses with a head), which define the fixed point, and its goal clauses (those without), which merely say that the fixed point avoids certain configurations – a first-order statement about it, and so exactly what an output formula can express.

@[reducible, inline]

abbrev DescriptiveComplexity.varSym (B : SOBlock) (i : B.ι) : B.lang.Relations (B.arity i)

The symbol of a relation variable of the block.

Equations

• DescriptiveComplexity.varSym B i = ⟨i, ⋯⟩

@[reducible, inline]

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

The symbol of a relation variable, in the expanded vocabulary.

Equations

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

noncomputable def DescriptiveComplexity.atomF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (a : SOAtom B k) : ((L.sum FirstOrder.Language.order).sum B.lang).Formula (Empty ⊕ Fin k)

A second-order atom, as a first-order atom over the expanded vocabulary.

Equations

• DescriptiveComplexity.atomF a = (DescriptiveComplexity.varOutSym L B a.idx).formula fun (j : Fin (B.arity a.idx)) => FirstOrder.Language.var (Sum.inr (a.args j))

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

A guard, transported to the expanded vocabulary.

Equations

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

noncomputable def DescriptiveComplexity.goalOutF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (c : HornClause (L.sum FirstOrder.Language.order) B k) : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence

A goal clause, as the first-order statement that it never fires.

Equations

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

noncomputable def DescriptiveComplexity.hornOutF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence

The output formula of the translation: no goal clause of the program ever fires at the fixed point.

Equations

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

theorem DescriptiveComplexity.realize_atomF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ρ : B.Assignment A) (a : SOAtom B k) (v : Empty ⊕ Fin k → A) : (atomF a).Realize v ↔ a.Holds ρ fun (j : Fin k) => v (Sum.inr j)

theorem DescriptiveComplexity.realize_guardOutF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ρ : B.Assignment A) (φ : (L.sum FirstOrder.Language.order).Formula (Fin k)) (v : Empty ⊕ Fin k → A) : (guardOutF φ).Realize v ↔ φ.Realize fun (j : Fin k) => v (Sum.inr j)

theorem DescriptiveComplexity.realize_goalOutF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ρ : B.Assignment A) (c : HornClause (L.sum FirstOrder.Language.order) B k) : A ⊨ goalOutF c ↔ ∀ (v : Fin k → A), ¬(c.guard.Realize v ∧ ∀ b ∈ c.body, b.Holds ρ v)

theorem DescriptiveComplexity.realize_hornOutF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ρ : B.Assignment A) (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : A ⊨ hornOutF prog ↔ ∀ c ∈ prog, c.head = none → ∀ (v : Fin k → A), ¬(c.guard.Realize v ∧ ∀ b ∈ c.body, b.Holds ρ v)

theorem DescriptiveComplexity.SigmaSOHornDefinable.lfpDefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : SigmaSOHornDefinable P) : LFPDefinable P

Every SO-Horn definition is an FO(LFP) definition: keep the rules, and turn the goal clauses into the output formula.

theorem DescriptiveComplexity.SigmaSOHornDefinable.compl_lfpDefinable {L : FirstOrder.Language} {P : DecisionProblem L} (h : SigmaSOHornDefinable Pᶜ) : LFPDefinable P

The complements of the SO-Horn definable problems are FO(LFP) definable too – which is what the Horn fragment on its own cannot say.

Closure under reductions

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

FO(LFP) definability is closed under ordered first-order reductions. The rules pull back as a Horn program and their fixed point commutes with the pullback (DescriptiveComplexity.lfpAssign_pull); the output sentence pulls back through DescriptiveComplexity.FOInterpretation.extendSO, the two views of the interpreted structure being identified by DescriptiveComplexity.FOInterpretation.extendSOEquiv and DescriptiveComplexity.FOInterpretation.ordExtendLEquiv.