FO(LFP) = SO-Horn: the translation into the fragment

The hard half of Grädel's equivalence (Grädel 1992): every FO(LFP) definable problem is SO-Horn definable (DescriptiveComplexity.LFPDefinable.sigmaSOHornDefinable). With the easy half DescriptiveComplexity.SigmaSOHornDefinable.lfpDefinable the two formalisms are interchangeable (DescriptiveComplexity.lfpDefinable_iff_sigmaSOHornDefinable), so the fragment inherits the closure property that only a full logic has by construction: SO-Horn definability is closed under complement (DescriptiveComplexity.SigmaSOHornDefinable.compl), and level 0 of the polynomial hierarchy collapses, Π₀ᵖ = Σ₀ᵖ (DescriptiveComplexity.piP_zero_eq) – polynomial time, as defined by the Horn fragment, is closed under complement.

The construction

Where a Σ₁ certificate could guess a fixed point and its derivation order, a Horn program must derive them. The program built here (DescriptiveComplexity.LFPHorn.trProg) has one goal clause – “the output sentence is not false” – and rules computing, as its least model, the entire evaluation of the FO(LFP) definition (DescriptiveComplexity.LFPHorn.canonAssign):

• the fixed point itself, on a copy of the original block, by the original rules (DescriptiveComplexity.LFPHorn.liftedRules);
• the complement of the fixed point, the part a positive formalism cannot see directly: relations N j i (t̄, x̄) – the atom i x̄ is not yet derived at stage (j, t̄) – for stages indexed lexicographically by hc + 1 static copies of the tuples t̄ ∈ A^hm (DescriptiveComplexity.LFPHorn.hs copies suffice on every nonempty structure, where tuples alone would fail on one-element universes: (hc+1)·n^hm always exceeds the Σᵢ n^{arityᵢ} rounds after which the stages stabilize, DescriptiveComplexity.derivesIn_iff_derives_of_card_le). The base rules populate N at the bottom stage; the step rules carry an underived atom to the next stage when no rule instance derives it, that unbounded conjunction over the valuations being assembled by the non-firing accumulators NF j (c, a) (t̄, x̄, w̄) walking the lexicographic order of the valuations w̄ ∈ A^k – the technique of DescriptiveComplexity.Problems.HornSat.Definability, applied to a rule system rather than one clause body, with the order machinery of DescriptiveComplexity.OrderWalk;
• an evaluator for the output sentence: truth and falsity relations for every subformula (DescriptiveComplexity.subs lists them; no recursion over the syntax is needed in the index type), with falsity of a fixed-point atom read from N at the last stage, implication evaluated clausewise, and the universal quantifier assembled by one more accumulator along the order.

Correctness is the identity between the least model of this program and the canonical assignment: soundness (DescriptiveComplexity.LFPHorn.trRules_sound, the canonical assignment satisfies every rule) gives one inclusion and makes the canonical assignment the witness when the output holds; completeness (the DescriptiveComplexity.LFPHorn.derives_n/derives_nf/derives_eval inductions along stages, valuations and subformulas) shows every canonical fact derivable, so that any satisfying assignment of the program contains it – in particular the falsity of the output, when false, always reaches the goal clause (DescriptiveComplexity.LFPHorn.holds_iff_exists).

Stripping a relational summand out of terms

def DescriptiveComplexity.stripTerm {L₀ R : FirstOrder.Language} [R.IsRelational] {α : Type} : (L₀.sum R).Term α → L₀.Term α

A term over L₀.sum R with R relational is a term over L₀: the summand contributes no function symbols.

Equations

• DescriptiveComplexity.stripTerm (FirstOrder.Language.var a) = FirstOrder.Language.var a
• DescriptiveComplexity.stripTerm (FirstOrder.Language.func (Sum.inl f) ts) = FirstOrder.Language.func f fun (i : Fin l) => DescriptiveComplexity.stripTerm (ts i)
• DescriptiveComplexity.stripTerm (FirstOrder.Language.func (Sum.inr f) _ts) = isEmptyElim f

theorem DescriptiveComplexity.realize_stripTerm {L₀ R : FirstOrder.Language} [R.IsRelational] {α A : Type} [L₀.Structure A] [R.Structure A] (v : α → A) (t : (L₀.sum R).Term α) : FirstOrder.Language.Term.realize v (stripTerm t) = FirstOrder.Language.Term.realize v t

The subformula closure of a sentence, as a list

def DescriptiveComplexity.subs {Lg : FirstOrder.Language} {n : ℕ} : Lg.BoundedFormula Empty n → List ((n' : ℕ) × Lg.BoundedFormula Empty n')

The subformulas of a bounded formula over Empty, each with its binder depth, as a list; the formula itself is included.

Equations

• DescriptiveComplexity.subs FirstOrder.Language.BoundedFormula.falsum = [⟨x✝, FirstOrder.Language.BoundedFormula.falsum⟩]
• DescriptiveComplexity.subs (FirstOrder.Language.BoundedFormula.equal t u) = [⟨x✝, FirstOrder.Language.BoundedFormula.equal t u⟩]
• DescriptiveComplexity.subs (FirstOrder.Language.BoundedFormula.rel r ts) = [⟨x✝, FirstOrder.Language.BoundedFormula.rel r ts⟩]
• DescriptiveComplexity.subs (a.imp b) = ⟨x✝, a.imp b⟩ :: (DescriptiveComplexity.subs a ++ DescriptiveComplexity.subs b)
• DescriptiveComplexity.subs a.all = ⟨x✝, a.all⟩ :: DescriptiveComplexity.subs a

theorem DescriptiveComplexity.self_mem_subs {Lg : FirstOrder.Language} {n : ℕ} (φ : Lg.BoundedFormula Empty n) : ⟨n, φ⟩ ∈ subs φ

theorem DescriptiveComplexity.subs_trans {Lg : FirstOrder.Language} {n : ℕ} {φ : Lg.BoundedFormula Empty n} {x : (n' : ℕ) × Lg.BoundedFormula Empty n'} (hx : x ∈ subs φ) : subs x.snd ⊆ subs φ

theorem DescriptiveComplexity.left_mem_subs_imp {Lg : FirstOrder.Language} {n : ℕ} (a b : Lg.BoundedFormula Empty n) : ⟨n, a⟩ ∈ subs (a.imp b)

theorem DescriptiveComplexity.right_mem_subs_imp {Lg : FirstOrder.Language} {n : ℕ} (a b : Lg.BoundedFormula Empty n) : ⟨n, b⟩ ∈ subs (a.imp b)

theorem DescriptiveComplexity.mem_subs_all {Lg : FirstOrder.Language} {n : ℕ} (a : Lg.BoundedFormula Empty (n + 1)) : ⟨n + 1, a⟩ ∈ subs a.all

def DescriptiveComplexity.ctxB {Lg : FirstOrder.Language} {n : ℕ} : Lg.BoundedFormula Empty n → ℕ

A bound on the binder depths of the subformula closure.

Equations

• DescriptiveComplexity.ctxB (a.imp b) = max (DescriptiveComplexity.ctxB a) (DescriptiveComplexity.ctxB b)
• DescriptiveComplexity.ctxB a.all = DescriptiveComplexity.ctxB a
• DescriptiveComplexity.ctxB x✝ = x✝¹

theorem DescriptiveComplexity.le_ctxB {Lg : FirstOrder.Language} {n : ℕ} (φ : Lg.BoundedFormula Empty n) : n ≤ ctxB φ

theorem DescriptiveComplexity.fst_le_ctxB {Lg : FirstOrder.Language} {n : ℕ} {φ : Lg.BoundedFormula Empty n} {x : (n' : ℕ) × Lg.BoundedFormula Empty n'} (hx : x ∈ subs φ) : x.fst ≤ ctxB φ

The headed clauses of the rule system

noncomputable def DescriptiveComplexity.LFPHorn.headed {L : FirstOrder.Language} (d : LFPDef L) : List (HornClause (L.sum FirstOrder.Language.order) d.B d.k × SOAtom d.B d.k)

The rules with a head, paired with their heads: goal clauses derive nothing, so only these participate in the stage machinery.

Equations

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

theorem DescriptiveComplexity.LFPHorn.mem_headed {L : FirstOrder.Language} (d : LFPDef L) {ca : HornClause (L.sum FirstOrder.Language.order) d.B d.k × SOAtom d.B d.k} : ca ∈ headed d ↔ ca.1 ∈ d.rules ∧ ca.1.head = some ca.2

Dimensions of the construction

noncomputable def DescriptiveComplexity.LFPHorn.hm {L : FirstOrder.Language} (d : LFPDef L) : ℕ

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

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.hc {L : FirstOrder.Language} (d : LFPDef L) : ℕ

The number of copies of the stage relations, minus one.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.hs {L : FirstOrder.Language} (d : LFPDef L) : ℕ

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

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.hX {L : FirstOrder.Language} (d : LFPDef L) : ℕ

The number of variables reserved for evaluating the output sentence.

Equations

• DescriptiveComplexity.LFPHorn.hX d = DescriptiveComplexity.ctxB d.out

noncomputable def DescriptiveComplexity.LFPHorn.kk {L : FirstOrder.Language} (d : LFPDef L) : ℕ

The universally quantified first-order variables shared by all clauses of the translated program: three stage-tuple blocks, two valuation blocks, the evaluation block, and one spare.

Equations

• DescriptiveComplexity.LFPHorn.kk d = 3 * DescriptiveComplexity.LFPHorn.hm d + 2 * d.k + DescriptiveComplexity.LFPHorn.hX d + 1

theorem DescriptiveComplexity.LFPHorn.ctx_le_hX {L : FirstOrder.Language} (d : LFPDef L) {n : ℕ} {ψ : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n} (h : ⟨n, ψ⟩ ∈ subs d.out) : n ≤ hX d

The binder depth of a subformula of the output is within the evaluation block. (A dedicated lemma, so that proof terms in the rules carry exactly this type.)

theorem DescriptiveComplexity.LFPHorn.left_mem_out {L : FirstOrder.Language} (d : LFPDef L) {n : ℕ} {a b : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n} (h : ⟨n, a.imp b⟩ ∈ subs d.out) : ⟨n, a⟩ ∈ subs d.out

The left subformula of an implication in the output.

theorem DescriptiveComplexity.LFPHorn.right_mem_out {L : FirstOrder.Language} (d : LFPDef L) {n : ℕ} {a b : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n} (h : ⟨n, a.imp b⟩ ∈ subs d.out) : ⟨n, b⟩ ∈ subs d.out

The right subformula of an implication in the output.

theorem DescriptiveComplexity.LFPHorn.all_mem_out {L : FirstOrder.Language} (d : LFPDef L) {n : ℕ} {a : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty (n + 1)} (h : ⟨n, a.all⟩ ∈ subs d.out) : ⟨n + 1, a⟩ ∈ subs d.out

The body of a universally quantified subformula of the output.

The block of the translation

def DescriptiveComplexity.LFPHorn.SubIx {L : FirstOrder.Language} (d : LFPDef L) : Type

Index of the subformula relations: a subformula of the output sentence, with its binder depth.

Equations

• DescriptiveComplexity.LFPHorn.SubIx d = { x : (n' : ℕ) × ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n' // x ∈ DescriptiveComplexity.subs d.out }

noncomputable def DescriptiveComplexity.LFPHorn.HIx {L : FirstOrder.Language} (d : LFPDef L) : Type

Index of the non-firing relations: a headed clause of the rule system.

Equations

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

instance DescriptiveComplexity.LFPHorn.instFiniteSubIx {L : FirstOrder.Language} (d : LFPDef L) : Finite (SubIx d)

instance DescriptiveComplexity.LFPHorn.instFiniteHIx {L : FirstOrder.Language} (d : LFPDef L) : Finite (HIx d)

@[reducible, inline]

abbrev DescriptiveComplexity.LFPHorn.TrIx {L : FirstOrder.Language} (d : LFPDef L) : Type

The relation variables of the translated program: the original block (computing the fixed point), the stage complements N, the non-firing accumulators NF, the subformula truth/falsity relations, and the ∀-accumulators.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.LFPHorn.rIx {L : FirstOrder.Language} (d : LFPDef L) (i : d.B.ι) : TrIx d

The original relation variables.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.LFPHorn.nIx {L : FirstOrder.Language} (d : LFPDef L) (j : Fin (hs d)) (i : d.B.ι) : TrIx d

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

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.LFPHorn.nfIx {L : FirstOrder.Language} (d : LFPDef L) (j : Fin (hs d)) (ca : HIx d) : TrIx d

NF j (c, a) (t̄, x̄, w̄): no valuation up to w̄ fires the clause c at stage (j, t̄) to derive the atom a.idx x̄.

Equations

• DescriptiveComplexity.LFPHorn.nfIx d j ca = Sum.inr (Sum.inr (Sum.inl (j, ca)))

@[reducible, inline]

abbrev DescriptiveComplexity.LFPHorn.tfIx {L : FirstOrder.Language} (d : LFPDef L) (x : SubIx d) (b : Bool) : TrIx d

Truth (true) and falsity (false) of a subformula of the output.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.LFPHorn.acIx {L : FirstOrder.Language} (d : LFPDef L) (x : SubIx d) : TrIx d

The accumulator of a universally quantified subformula.

Equations

• DescriptiveComplexity.LFPHorn.acIx d x = Sum.inr (Sum.inr (Sum.inr (Sum.inr x)))

noncomputable def DescriptiveComplexity.LFPHorn.trArity {L : FirstOrder.Language} (d : LFPDef L) : TrIx d → ℕ

The arities: stage relations carry a stage tuple in front, non-firing relations also a valuation tuple behind, subformula relations their binder depth.

Equations

• DescriptiveComplexity.LFPHorn.trArity d (Sum.inl i) = d.B.arity i
• DescriptiveComplexity.LFPHorn.trArity d (Sum.inr (Sum.inl (fst, i))) = DescriptiveComplexity.LFPHorn.hm d + d.B.arity i
• DescriptiveComplexity.LFPHorn.trArity d (Sum.inr (Sum.inr (Sum.inl (fst, ca)))) = DescriptiveComplexity.LFPHorn.hm d + d.B.arity (↑ca).2.idx + d.k
• DescriptiveComplexity.LFPHorn.trArity d (Sum.inr (Sum.inr (Sum.inr (Sum.inl (x_1, snd))))) = (↑x_1).fst
• DescriptiveComplexity.LFPHorn.trArity d (Sum.inr (Sum.inr (Sum.inr (Sum.inr x_1)))) = (↑x_1).fst + 1

noncomputable def DescriptiveComplexity.LFPHorn.trBlock {L : FirstOrder.Language} (d : LFPDef L) : SOBlock

The block of the translated program.

Equations

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

The shared first-order variables and their layout

All clauses of the translated program share kk d universally quantified variables: three stage-tuple blocks (current stage, next stage, and the atom tuple), two valuation blocks for the rule being tested, a block for the free variables of the output's subformulas, and one spare variable for the ∀-accumulators.

noncomputable def DescriptiveComplexity.LFPHorn.vT1 {L : FirstOrder.Language} (d : LFPDef L) (q : Fin (hm d)) : Fin (kk d)

The current stage tuple t̄.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.vT2 {L : FirstOrder.Language} (d : LFPDef L) (q : Fin (hm d)) : Fin (kk d)

The next stage tuple t̄'.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.vX {L : FirstOrder.Language} (d : LFPDef L) (q : Fin (hm d)) : Fin (kk d)

The atom tuple x̄ (also the interpreted arguments ȳ of the output's fixed-point atoms).

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.vW1 {L : FirstOrder.Language} (d : LFPDef L) (q : Fin d.k) : Fin (kk d)

The first valuation block w̄.

Equations

• DescriptiveComplexity.LFPHorn.vW1 d q = ⟨3 * DescriptiveComplexity.LFPHorn.hm d + ↑q, ⋯⟩

noncomputable def DescriptiveComplexity.LFPHorn.vW2 {L : FirstOrder.Language} (d : LFPDef L) (q : Fin d.k) : Fin (kk d)

The second valuation block w̄'.

Equations

• DescriptiveComplexity.LFPHorn.vW2 d q = ⟨3 * DescriptiveComplexity.LFPHorn.hm d + d.k + ↑q, ⋯⟩

noncomputable def DescriptiveComplexity.LFPHorn.vE {L : FirstOrder.Language} (d : LFPDef L) (q : Fin (hX d)) : Fin (kk d)

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

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.vS {L : FirstOrder.Language} (d : LFPDef L) : Fin (kk d)

The spare variable, the accumulator's predecessor.

Equations

• DescriptiveComplexity.LFPHorn.vS d = ⟨3 * DescriptiveComplexity.LFPHorn.hm d + 2 * d.k + DescriptiveComplexity.LFPHorn.hX d, ⋯⟩

noncomputable def DescriptiveComplexity.LFPHorn.xa {L : FirstOrder.Language} (d : LFPDef L) (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.LFPHorn.xa d i q = DescriptiveComplexity.LFPHorn.vX d ⟨↑q, ⋯⟩

noncomputable def DescriptiveComplexity.LFPHorn.eSel {L : FirstOrder.Language} (d : LFPDef L) {n : ℕ} (hn : n ≤ hX d) (q : Fin n) : Fin (kk d)

The first n variables of the evaluation block.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.j0 {L : FirstOrder.Language} (d : LFPDef L) : Fin (hs d)

The first copy.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.jTop {L : FirstOrder.Language} (d : LFPDef L) : Fin (hs d)

The last copy.

Equations

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

Atom builders

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

An atom of an original relation variable.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.nAt {L : FirstOrder.Language} (d : LFPDef L) (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.LFPHorn.nfAt {L : FirstOrder.Language} (d : LFPDef L) (j : Fin (hs d)) (ca : HIx d) (ts : Fin (hm d) → Fin (kk d)) (xs : Fin (d.B.arity (↑ca).2.idx) → Fin (kk d)) (ws : Fin d.k → Fin (kk d)) : SOAtom (trBlock d) (kk d)

An atom NF j (c, a) (t̄, x̄, w̄).

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.tfAt {L : FirstOrder.Language} (d : LFPDef L) (x : SubIx d) (b : Bool) (es : Fin (↑x).fst → Fin (kk d)) : SOAtom (trBlock d) (kk d)

A truth or falsity atom of a subformula.

Equations

• DescriptiveComplexity.LFPHorn.tfAt d x b es = { idx := DescriptiveComplexity.LFPHorn.tfIx d x b, args := es }

noncomputable def DescriptiveComplexity.LFPHorn.acAt {L : FirstOrder.Language} (d : LFPDef L) (x : SubIx d) (es : Fin ((↑x).fst + 1) → Fin (kk d)) : SOAtom (trBlock d) (kk d)

An accumulator atom of a subformula.

Equations

• DescriptiveComplexity.LFPHorn.acAt d x es = { idx := DescriptiveComplexity.LFPHorn.acIx d x, args := es }

The rules of the translated program

noncomputable def DescriptiveComplexity.LFPHorn.iotaList {L : FirstOrder.Language} (d : LFPDef L) : List d.B.ι

The relation variables, as a list.

Equations

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

theorem DescriptiveComplexity.LFPHorn.mem_iotaList {L : FirstOrder.Language} (d : LFPDef L) (i : d.B.ι) : i ∈ iotaList d

noncomputable def DescriptiveComplexity.LFPHorn.liftAtom {L : FirstOrder.Language} (d : LFPDef L) (a : SOAtom d.B d.k) : SOAtom (trBlock d) (kk d)

An original atom, over the lifted block and variables.

Equations

• DescriptiveComplexity.LFPHorn.liftAtom d a = DescriptiveComplexity.LFPHorn.rAt d a.idx fun (q : Fin (d.B.arity a.idx)) => DescriptiveComplexity.LFPHorn.vW1 d (a.args q)

noncomputable def DescriptiveComplexity.LFPHorn.liftClause {L : FirstOrder.Language} (d : LFPDef L) (c : HornClause (L.sum FirstOrder.Language.order) d.B d.k) : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

An original rule, over the lifted block and variables.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.liftedRules {L : FirstOrder.Language} (d : LFPDef L) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

The original headed rules, lifted: they compute the fixed point on the R-part of the block. (Goal clauses of the rule system are not lifted: in FO(LFP) they derive nothing, and their content is carried by the output sentence.)

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.stagePairs {L : FirstOrder.Language} (d : LFPDef L) : List (Fin (hs d) × Fin (hs d))

The stage-successor pairs of copies: within one copy, or crossing to the next.

Equations

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

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

noncomputable def DescriptiveComplexity.LFPHorn.stageG {L : FirstOrder.Language} (d : LFPDef L) (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.

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

Base rules: at the first stage, nothing is derived.

Equations

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

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

Step rules: an atom underivable at a stage all of whose potential derivations fail to fire stays underivable at the next stage.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.nfClauses {L : FirstOrder.Language} (d : LFPDef L) (j : Fin (hs d)) (ca : HIx d) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

The non-firing rules for one copy and one headed clause (c, a): walking the valuations w̄' along their lexicographic order, NF (t̄, x̄, w̄') is derived when the previous accumulator holds (at the base, nothing) and the clause does not derive a.idx x̄ at valuation w̄' – because its guard fails, because its head tuple differs from x̄, or because one of its body atoms is not derived at the stage.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.nfRules {L : FirstOrder.Language} (d : LFPDef L) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

All non-firing rules.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.evTerm {L : FirstOrder.Language} (d : LFPDef L) {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

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

noncomputable def DescriptiveComplexity.LFPHorn.evalClauses {L : FirstOrder.Language} (d : LFPDef L) (x : SubIx d) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

The rules evaluating one subformula of the output, by shape.

Equations

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

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

All subformula-evaluation rules.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.goalClause {L : FirstOrder.Language} (d : LFPDef L) : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

The unique goal clause: the output sentence must not be false at the fixed point.

Equations

• DescriptiveComplexity.LFPHorn.goalClause d = { guard := ⊤, body := [DescriptiveComplexity.LFPHorn.tfAt d ⟨⟨0, d.out⟩, ⋯⟩ false Fin.elim0], head := none }

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

The rules of the translated program: everything but the goal clause.

Equations

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

noncomputable def DescriptiveComplexity.LFPHorn.trProg {L : FirstOrder.Language} (d : LFPDef L) : HornProgram (L.sum FirstOrder.Language.order) (trBlock d) (kk d)

The translated program.

Equations

• DescriptiveComplexity.LFPHorn.trProg d = DescriptiveComplexity.LFPHorn.trRules d ++ [DescriptiveComplexity.LFPHorn.goalClause d]

The canonical assignment

Over a fixed ordered structure, each relation variable of the block has an intended value; the correctness proof shows that the least model of the translated program is exactly this assignment.

theorem DescriptiveComplexity.LFPHorn.comp_addCases {m n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (f₁ : Fin m → α) (f₂ : Fin n → α) : (fun (q : Fin (m + n)) => g (Fin.addCases f₁ f₂ q)) = fun (i : Fin (m + n)) => Fin.addCases (fun (q : Fin m) => g (f₁ q)) (fun (q : Fin n) => g (f₂ q)) i

Composition distributes over Fin.addCases.

noncomputable def DescriptiveComplexity.LFPHorn.srank {L : FirstOrder.Language} (d : LFPDef L) (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.LFPHorn.srank d A j t = DescriptiveComplexity.orank (toLex (j, toLex t))

noncomputable def DescriptiveComplexity.LFPHorn.canonN {L : FirstOrder.Language} (d : LFPDef L) (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: at stage (j, t̄), the atom i x̄ is not yet derived. (A named definition, so that reduction stops here rather than exposing the recursion of DescriptiveComplexity.derivesIn.)

Equations

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

def DescriptiveComplexity.LFPHorn.NFsem {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] (r : ℕ) (c : HornClause (L.sum FirstOrder.Language.order) d.B d.k) (a : SOAtom d.B d.k) (x : Fin (d.B.arity a.idx) → A) (w : Fin d.k → A) : Prop

The clause c with head atom a does not derive the atom a.idx x̄ at stage rank r, at any valuation lexicographically up to w̄.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.LFPHorn.lfpStr {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] : ((L.sum FirstOrder.Language.order).sum d.B.lang).Structure A

The structure interpreting the expanded vocabulary at the least fixed point of the rules – the structure the output sentence is read in.

Equations

• DescriptiveComplexity.LFPHorn.lfpStr d A = (L.sum FirstOrder.Language.order).sumStructure d.B.lang A

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

Truth of a subformula of the output at the least fixed point.

Equations

• DescriptiveComplexity.LFPHorn.evalT d A ψ v = ψ.Realize default v

noncomputable def DescriptiveComplexity.LFPHorn.canonAc {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] (x : SubIx d) : (Fin ((↑x).fst + 1) → A) → Prop

The intended accumulator of a universally quantified subformula: 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.LFPHorn.canonAc d A x = fun (x : Fin ((↑x).fst + 1) → A) => False

noncomputable def DescriptiveComplexity.LFPHorn.canonAssign {L : FirstOrder.Language} (d : LFPDef L) (A : Type) [L.Structure A] [LinearOrder A] : (trBlock d).Assignment A

The canonical assignment: the fixed point on the original variables, the complements of its stages on N, the non-firing predicates on NF, truth and falsity of the output's subformulas, and the accumulators.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.LFPHorn.canonAssign d A (Sum.inl i) = fun (x : Fin ((DescriptiveComplexity.LFPHorn.trBlock d).arity (Sum.inl i)) → A) => DescriptiveComplexity.Derives d.rules ⟨i, x⟩
• DescriptiveComplexity.LFPHorn.canonAssign d A (Sum.inr (Sum.inl (j, i))) = DescriptiveComplexity.LFPHorn.canonN d A j i
• DescriptiveComplexity.LFPHorn.canonAssign d A (Sum.inr (Sum.inr (Sum.inr (Sum.inr x)))) = DescriptiveComplexity.LFPHorn.canonAc d A x

Atom characterizations under the canonical assignment

theorem DescriptiveComplexity.LFPHorn.rAt_holds {L : FirstOrder.Language} {d : LFPDef L} {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 ↔ Derives d.rules ⟨i, fun (q : Fin (d.B.arity i)) => V (sel q)⟩

theorem DescriptiveComplexity.LFPHorn.canonN_addCases {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {i : d.B.ι} {t : Fin (hm d) → A} {x : Fin (d.B.arity i) → A} : (canonN d A j i fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases t x i_1) ↔ ¬derivesIn d.rules (srank d A j t) ⟨i, x⟩

theorem DescriptiveComplexity.LFPHorn.nAt_holds {L : FirstOrder.Language} {d : LFPDef L} {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 ↔ ¬derivesIn d.rules (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.LFPHorn.nfAt_holds {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {ca : HIx d} {ts : Fin (hm d) → Fin (kk d)} {xs : Fin (d.B.arity (↑ca).2.idx) → Fin (kk d)} {ws : Fin d.k → Fin (kk d)} {V : Fin (kk d) → A} : (nfAt d j ca ts xs ws).Holds (canonAssign d A) V ↔ NFsem d A (srank d A j fun (q : Fin (hm d)) => V (ts q)) (↑ca).1 (↑ca).2 (fun (q : Fin (d.B.arity (↑ca).2.idx)) => V (xs q)) fun (q : Fin d.k) => V (ws q)

theorem DescriptiveComplexity.LFPHorn.tAt_holds {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {x : SubIx d} {es : Fin (↑x).fst → Fin (kk d)} {V : Fin (kk d) → A} : (tfAt d x true es).Holds (canonAssign d A) V ↔ evalT d A (↑x).snd fun (q : Fin (↑x).fst) => V (es q)

theorem DescriptiveComplexity.LFPHorn.fAt_holds {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {x : SubIx d} {es : Fin (↑x).fst → Fin (kk d)} {V : Fin (kk d) → A} : (tfAt d x false es).Holds (canonAssign d A) V ↔ ¬evalT d A (↑x).snd fun (q : Fin (↑x).fst) => V (es q)

theorem DescriptiveComplexity.LFPHorn.acAt_holds {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {x : SubIx d} {es : Fin ((↑x).fst + 1) → Fin (kk d)} {V : Fin (kk d) → A} : (acAt d x es).Holds (canonAssign d A) V ↔ canonAc d A x fun (q : Fin ((↑x).fst + 1)) => V (es q)

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

The accumulator of ∀, at an explicit snoc tuple.

Counting: the last stage is beyond every derivation

theorem DescriptiveComplexity.LFPHorn.card_le_srank_top {L : FirstOrder.Language} (d : LFPDef L) {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) : Nat.card (BAtom d.B A) ≤ srank d A (jTop d) t

Soundness: the canonical assignment satisfies the rules

Each rule family preserves the canonical assignment; the goal clause is dealt with at assembly time, where it encodes the output sentence itself.

theorem DescriptiveComplexity.LFPHorn.lifted_sound {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} {ca : HornClause (L.sum FirstOrder.Language.order) d.B d.k × SOAtom d.B d.k} (hca : ca ∈ headed d) : (liftClause d ca.1).Holds (canonAssign d A) V

theorem DescriptiveComplexity.LFPHorn.srank_bot {L : FirstOrder.Language} {d : LFPDef L} {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.LFPHorn.nBase_sound {L : FirstOrder.Language} {d : LFPDef L} {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.LFPHorn.stageG_covBy {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {V : Fin (kk d) → A} {j j' : Fin (hs d)} (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.LFPHorn.nStep_sound {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {V : Fin (kk d) → A} {j j' : Fin (hs d)} (hjj : (j, j') ∈ stagePairs d) {i : d.B.ι} : { guard := stageG d j j' ⊓ maxTupF (vW1 d), body := nAt d j i (vT1 d) (xa d i) :: List.map (fun (ca : HIx d) => nfAt d j ca (vT1 d) (xa d (↑ca).2.idx) (vW1 d)) (List.filter (fun (ca : { x : HornClause (L.sum FirstOrder.Language.order) d.B d.k × SOAtom d.B d.k // x ∈ headed d }) => decide ((↑ca).2.idx = i)) (headed d).attach), head := some (nAt d j' i (vT2 d) (xa d i)) }.Holds (canonAssign d A) V

theorem DescriptiveComplexity.LFPHorn.NFsem_base {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {r : ℕ} {c₀ : HornClause (L.sum FirstOrder.Language.order) d.B d.k} {a₀ : SOAtom d.B d.k} {x : Fin (d.B.arity a₀.idx) → A} {w : Fin d.k → A} (hbot : ∀ (p : Fin d.k) (a : A), w p ≤ a) (hfail : ¬(c₀.guard.Realize w ∧ (∀ b ∈ c₀.body, derivesIn d.rules r ⟨b.idx, fun (q : Fin (d.B.arity b.idx)) => w (b.args q)⟩) ∧ (fun (q : Fin (d.B.arity a₀.idx)) => w (a₀.args q)) = x)) : NFsem d A r c₀ a₀ x w

Extending a non-firing certificate at the bottom valuation.

theorem DescriptiveComplexity.LFPHorn.NFsem_step {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {r : ℕ} {c₀ : HornClause (L.sum FirstOrder.Language.order) d.B d.k} {a₀ : SOAtom d.B d.k} {x : Fin (d.B.arity a₀.idx) → A} {w w' : Fin d.k → A} (hsucc : TupSucc w w') (hprev : NFsem d A r c₀ a₀ x w) (hfail : ¬(c₀.guard.Realize w' ∧ (∀ b ∈ c₀.body, derivesIn d.rules r ⟨b.idx, fun (q : Fin (d.B.arity b.idx)) => w' (b.args q)⟩) ∧ (fun (q : Fin (d.B.arity a₀.idx)) => w' (a₀.args q)) = x)) : NFsem d A r c₀ a₀ x w'

Extending a non-firing certificate along the successor valuation.

theorem DescriptiveComplexity.LFPHorn.nfClauses_sound {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {V : Fin (kk d) → A} {j : Fin (hs d)} {ca : HIx d} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (hc : c ∈ nfClauses d j ca) : c.Holds (canonAssign d A) V

Evaluating the output sentence

noncomputable def DescriptiveComplexity.LFPHorn.evTermVal {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {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 the least fixed point.

Equations

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

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

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

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

theorem DescriptiveComplexity.LFPHorn.evalT_rel_inl {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {n l : ℕ} {r : (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 (FirstOrder.Language.BoundedFormula.rel (Sum.inl r) ts) v ↔ FirstOrder.Language.Structure.RelMap r fun (q : Fin l) => evTermVal v (ts q)

theorem DescriptiveComplexity.LFPHorn.evalT_rel_inr {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {n l : ℕ} {r : 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 (FirstOrder.Language.BoundedFormula.rel (Sum.inr r) ts) v ↔ Derives d.rules ⟨↑r, fun (q : Fin (d.B.arity ↑r)) => evTermVal v (ts (Fin.cast ⋯ q))⟩

theorem DescriptiveComplexity.LFPHorn.realize_evTerm {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {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 (fun (q : Fin n) => V (eSel d hn q)) t

theorem DescriptiveComplexity.LFPHorn.eSel_snoc {L : FirstOrder.Language} {d : LFPDef L} {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.

theorem DescriptiveComplexity.LFPHorn.comp_snoc_lambda {n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (f : Fin n → α) (c : α) : (fun (q : Fin (n + 1)) => g (Fin.snoc f c q)) = Fin.snoc (fun (q : Fin n) => g (f q)) (g c)

Composition distributes over Fin.snoc.

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

All rules are sound

theorem DescriptiveComplexity.LFPHorn.trRules_sound {L : FirstOrder.Language} {d : LFPDef L} {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

The other inclusion: each component of the canonical assignment is contained in the least model of the translated program. The fixed point part is leastness itself; the stage complements walk the stage order, the non-firing predicates walk the valuation order, and the subformula relations follow the structure of the output.

noncomputable def DescriptiveComplexity.LFPHorn.packV {L : FirstOrder.Language} {d : LFPDef L} {A : Type} (t1 t2 x : Fin (hm d) → A) (w1 w2 : Fin d.k → 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.

noncomputable def DescriptiveComplexity.LFPHorn.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.LFPHorn.padF f p = if h : ↑p < m then f ⟨↑p, h⟩ else Classical.arbitrary A

theorem DescriptiveComplexity.LFPHorn.packV_comp_vT1 {L : FirstOrder.Language} {d : LFPDef L} {A : Type} {t1 t2 x : Fin (hm d) → A} {w1 w2 : Fin d.k → A} {e : Fin (hX d) → A} {sp : A} : (fun (q : Fin (hm d)) => packV t1 t2 x w1 w2 e sp (vT1 d q)) = t1

theorem DescriptiveComplexity.LFPHorn.packV_comp_vT2 {L : FirstOrder.Language} {d : LFPDef L} {A : Type} {t1 t2 x : Fin (hm d) → A} {w1 w2 : Fin d.k → A} {e : Fin (hX d) → A} {sp : A} : (fun (q : Fin (hm d)) => packV t1 t2 x w1 w2 e sp (vT2 d q)) = t2

theorem DescriptiveComplexity.LFPHorn.packV_comp_vW1 {L : FirstOrder.Language} {d : LFPDef L} {A : Type} {t1 t2 x : Fin (hm d) → A} {w1 w2 : Fin d.k → A} {e : Fin (hX d) → A} {sp : A} : (fun (q : Fin d.k) => packV t1 t2 x w1 w2 e sp (vW1 d q)) = w1

theorem DescriptiveComplexity.LFPHorn.packV_comp_vW2 {L : FirstOrder.Language} {d : LFPDef L} {A : Type} {t1 t2 x : Fin (hm d) → A} {w1 w2 : Fin d.k → A} {e : Fin (hX d) → A} {sp : A} : (fun (q : Fin d.k) => packV t1 t2 x w1 w2 e sp (vW2 d q)) = w2

theorem DescriptiveComplexity.LFPHorn.packV_comp_eSel {L : FirstOrder.Language} {d : LFPDef L} {A : Type} {t1 t2 x : Fin (hm d) → A} {w1 w2 : Fin d.k → A} {sp : A} {n : ℕ} [Nonempty A] (hn : n ≤ hX d) {v : Fin n → A} : (fun (q : Fin n) => packV t1 t2 x w1 w2 (padF v) sp (eSel d hn q)) = v

theorem DescriptiveComplexity.LFPHorn.packV_vS {L : FirstOrder.Language} {d : LFPDef L} {A : Type} {t1 t2 x : Fin (hm d) → A} {w1 w2 : Fin d.k → A} {e : Fin (hX d) → A} {sp : A} : packV t1 t2 x w1 w2 e sp (vS d) = sp

theorem DescriptiveComplexity.LFPHorn.packV_comp_xa {L : FirstOrder.Language} {d : LFPDef L} {A : Type} {t1 t2 : Fin (hm d) → A} {w1 w2 : Fin d.k → A} {e : Fin (hX d) → A} {sp : A} {i : d.B.ι} [Nonempty A] {xt : Fin (d.B.arity i) → A} : (fun (q : Fin (d.B.arity i)) => packV t1 t2 (padF xt) w1 w2 e sp (xa d i q)) = xt

theorem DescriptiveComplexity.LFPHorn.derives_congr_tuple {A : Type} {Lg : FirstOrder.Language} {B : SOBlock} {k : ℕ} {rules : List (HornClause Lg B k)} {ix : B.ι} {w w' : Fin (B.arity ix) → A} [Lg.Structure A] (h : w = w') (hd : Derives rules ⟨ix, w⟩) : Derives rules ⟨ix, w'⟩

Rewriting the tuple of a derived atom.

Membership of the rules in the program

theorem DescriptiveComplexity.LFPHorn.mem_trProg_trRules {L : FirstOrder.Language} {d : LFPDef L} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ trRules d) : c ∈ trProg d

theorem DescriptiveComplexity.LFPHorn.mem_trProg_lifted {L : FirstOrder.Language} {d : LFPDef L} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ liftedRules d) : c ∈ trProg d

theorem DescriptiveComplexity.LFPHorn.mem_trProg_nBase {L : FirstOrder.Language} {d : LFPDef L} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ nBase d) : c ∈ trProg d

theorem DescriptiveComplexity.LFPHorn.mem_trProg_nStep {L : FirstOrder.Language} {d : LFPDef L} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ nStep d) : c ∈ trProg d

theorem DescriptiveComplexity.LFPHorn.mem_trProg_nfRules {L : FirstOrder.Language} {d : LFPDef L} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ nfRules d) : c ∈ trProg d

theorem DescriptiveComplexity.LFPHorn.mem_trProg_evalRules {L : FirstOrder.Language} {d : LFPDef L} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ evalRules d) : c ∈ trProg d

theorem DescriptiveComplexity.LFPHorn.mem_evalRules {L : FirstOrder.Language} {d : LFPDef L} {x : SubIx d} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ evalClauses d x) : c ∈ evalRules d

The fixed point itself

theorem DescriptiveComplexity.LFPHorn.derives_r {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {i : d.B.ι} {x : Fin (d.B.arity i) → A} (h : Derives d.rules ⟨i, x⟩) : Derives (trProg d) ⟨rIx d i, x⟩

The fixed point of the rules is derivable on the R-part: leastness, against the lifted rules.

The stage complements

theorem DescriptiveComplexity.LFPHorn.NFsem_of_not_derivesIn {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {r : ℕ} {c : HornClause (L.sum FirstOrder.Language.order) d.B d.k} {a : SOAtom d.B d.k} (hc : c ∈ d.rules) (ha : c.head = some a) {xt : Fin (d.B.arity a.idx) → A} (hnd : ¬derivesIn d.rules (r + 1) ⟨a.idx, xt⟩) (w : Fin d.k → A) : NFsem d A r c a xt w

A stage that derives nothing new certifies non-firing at every valuation.

theorem DescriptiveComplexity.LFPHorn.stageG_realize {L : FirstOrder.Language} {d : LFPDef L} {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

The stage-successor guard is realizable along a cover.

theorem DescriptiveComplexity.LFPHorn.stagePairs_of_covBy {L : FirstOrder.Language} {d : LFPDef L} {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.LFPHorn.derives_nBase {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {i : d.B.ι} {t : Fin (hm d) → A} (ht : ∀ (p : Fin (hm d)) (a : A), t p ≤ a) (xt : Fin (d.B.arity i) → A) : Derives (trProg d) ⟨nIx d (j0 d) i, fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases t xt i_1⟩

At the bottom stage, everything is underived, by the base rules.

theorem DescriptiveComplexity.LFPHorn.mem_trProg_nfClauses {L : FirstOrder.Language} {d : LFPDef L} {j : Fin (hs d)} {ca : HIx d} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ nfClauses d j ca) : c ∈ trProg d

Membership of a non-firing clause in the program.

theorem DescriptiveComplexity.LFPHorn.fireNF {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {j : Fin (hs d)} {ca : HIx d} {t : Fin (hm d) → A} {xt : Fin (d.B.arity (↑ca).2.idx) → A} {w : Fin d.k → A} {V : Fin (kk d) → A} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (hcmem : c ∈ nfClauses d j ca) (hhead : c.head = some (nfAt d j ca (vT1 d) (xa d (↑ca).2.idx) (vW2 d))) (hg : c.guard.Realize V) (hb : ∀ b ∈ c.body, Derives (trProg d) ⟨b.idx, fun (q : Fin ((trBlock d).arity b.idx)) => V (b.args q)⟩) (ht1 : (fun (q : Fin (hm d)) => V (vT1 d q)) = t) (hxa : (fun (q : Fin (d.B.arity (↑ca).2.idx)) => V (xa d (↑ca).2.idx q)) = xt) (hw2 : (fun (q : Fin d.k) => V (vW2 d q)) = w) : Derives (trProg d) ⟨nfIx d j ca, fun (i : Fin (hm d + d.B.arity (↑ca).2.idx + d.k)) => Fin.addCases (fun (i : Fin (hm d + d.B.arity (↑ca).2.idx)) => Fin.addCases t xt i) w i⟩

Firing one non-firing clause, given its guard and bodies.

theorem DescriptiveComplexity.LFPHorn.derives_nf {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {j : Fin (hs d)} {t : Fin (hm d) → A} (hN : ∀ (i : d.B.ι) (xt : Fin (d.B.arity i) → A), ¬derivesIn d.rules (srank d A j t) ⟨i, xt⟩ → Derives (trProg d) ⟨nIx d j i, fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases t xt i_1⟩) (ca : HIx d) (xt : Fin (d.B.arity (↑ca).2.idx) → A) (w : Fin d.k → A) (hnf : NFsem d A (srank d A j t) (↑ca).1 (↑ca).2 xt w) : Derives (trProg d) ⟨nfIx d j ca, fun (i : Fin (hm d + d.B.arity (↑ca).2.idx + d.k)) => Fin.addCases (fun (i : Fin (hm d + d.B.arity (↑ca).2.idx)) => Fin.addCases t xt i) w i⟩

The non-firing certificates are derivable, walking the valuations.

theorem DescriptiveComplexity.LFPHorn.derives_n {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (S : Lex (Fin (hs d) × Lex (Fin (hm d) → A))) (i : d.B.ι) (xt : Fin (d.B.arity i) → A) : ¬derivesIn d.rules (orank S) ⟨i, xt⟩ → Derives (trProg d) ⟨nIx d (ofLex S).1 i, fun (i_1 : Fin (hm d + d.B.arity i)) => Fin.addCases (ofLex (ofLex S).2) xt i_1⟩

The stage complements are derivable, walking the stages.

The subformula relations

theorem DescriptiveComplexity.LFPHorn.mem_trProg_evalClauses {L : FirstOrder.Language} {d : LFPDef L} {x : SubIx d} {c : HornClause (L.sum FirstOrder.Language.order) (trBlock d) (kk d)} (h : c ∈ evalClauses d x) : c ∈ trProg d

theorem DescriptiveComplexity.LFPHorn.derives_eval {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {n : ℕ} (ψ : ((L.sum FirstOrder.Language.order).sum d.B.lang).BoundedFormula Empty n) (hmem : ⟨n, ψ⟩ ∈ subs d.out) (v : Fin n → A) : (evalT d A ψ v → Derives (trProg d) ⟨tfIx d ⟨⟨n, ψ⟩, hmem⟩ true, v⟩) ∧ (¬evalT d A ψ v → Derives (trProg d) ⟨tfIx d ⟨⟨n, ψ⟩, hmem⟩ false, v⟩)

Truth and falsity of every subformula of the output are derivable, by structural induction; universally quantified subformulas accumulate their instances along the order.

Assembly: the translated program defines the same problem

theorem DescriptiveComplexity.LFPHorn.evalT_out_iff {L : FirstOrder.Language} {d : LFPDef L} {A : Type} [L.Structure A] [LinearOrder A] {v : Fin 0 → A} : evalT d A d.out v ↔ d.Holds A

The truth of the output sentence, as the canonical value of its root.

theorem DescriptiveComplexity.LFPHorn.holds_iff_exists {L : FirstOrder.Language} (d : LFPDef L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : d.Holds A ↔ ∃ (ρ : (trBlock d).Assignment A), (trProg d).Holds ρ

The translated program has a satisfying assignment exactly when the FO(LFP) definition holds. Left to right, the canonical assignment satisfies every rule, and the goal clause because the output is true; right to left, any satisfying assignment contains the least model, and if the output were false its falsity would be derivable, firing the goal clause.

The equivalence of FO(LFP) and SO-Horn

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

Every FO(LFP) definable problem is SO-Horn definable – the hard direction of Grädel's equivalence, by the staged translation above. Together with DescriptiveComplexity.SigmaSOHornDefinable.lfpDefinable this makes the two formalisms interchangeable.

theorem DescriptiveComplexity.lfpDefinable_iff_sigmaSOHornDefinable {L : FirstOrder.Language} (P : DecisionProblem L) : LFPDefinable P ↔ SigmaSOHornDefinable P

FO(LFP) = SO-Horn (Grädel 1992): a problem is FO(LFP) definable iff it is SO-Horn definable, on ordered structures.

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

SO-Horn definability is closed under complement: through the logic FO(LFP), where complementation is negating the output formula. This is the statement that was out of reach of the fragment alone.

Level 0 of the hierarchy: Π₀ᵖ = Σ₀ᵖ

theorem DescriptiveComplexity.sigmaSOHornDefinable_compl_iff {L : FirstOrder.Language} (P : DecisionProblem L) : SigmaSOHornDefinable Pᶜ ↔ SigmaSOHornDefinable P

Complementation is a bijection of the SO-Horn definable problems.

theorem DescriptiveComplexity.piP_zero_eq : PiP 0 = SigmaP 0

Π₀ᵖ = Σ₀ᵖ: polynomial time is closed under complement – Grädel's capture theorem at level 0 of the hierarchy, the identity that was open while the fragment stood alone: it needs the least model of a Horn program computed inside the fragment, which is what the translation through FO(LFP) provides.