SO-Horn: existential second-order logic with a Horn kernel

The fragment SO-Horn of Grädel (Grädel 1992): existential second-order sentences whose first-order kernel is a conjunction of Horn clauses in the quantified relation variables. On ordered structures SO-Horn captures polynomial time – the Horn kernel is exactly what makes the guessed relations determined rather than merely guessed, since a satisfiable Horn formula has a least model, computable by unit propagation.

The kernel, as data

The Horn condition constrains only the occurrences of the second-order variables: a clause is

guard(x̄) ∧ R₁(x̄) ∧ … ∧ Rₙ(x̄) → R₀(x̄)   (or → ⊥)

where guard is an arbitrary first-order formula over the input vocabulary alone (in the definability notion below, over its ordered expansion). Rather than carve this shape out of FirstOrder.Language.BoundedFormula with a syntactic predicate, the kernel is represented here as data: a DescriptiveComplexity.HornClause bundles its guard, the list of its body atoms and its optional head atom, and a DescriptiveComplexity.HornProgram is a list of clauses sharing k universally quantified first-order variables. This is Grädel's clausal normal form, and it is what a reduction consuming an SO-Horn definition needs to see: the discharge of DescriptiveComplexity.Problems.HornSat.Hardness reads the clause list directly, and emits one propositional Horn clause per clause and per instantiation of the k variables.

DescriptiveComplexity.SigmaSOHornDefinable is the resulting definability notion, the SO-Horn analogue of DescriptiveComplexity.SigmaSODefinable; it is closed under (ordered) first-order reductions by DescriptiveComplexity.SecondOrderHornPull, which is what makes it a DescriptiveComplexity.ComplexityClass – the class DescriptiveComplexity.PTIME of DescriptiveComplexity.Hierarchy.

Horn programs

structure DescriptiveComplexity.HornClause (L : FirstOrder.Language) (B : SOBlock) (k : ℕ) : Type

A Horn clause over the input vocabulary L and the block B, with k universally quantified first-order variables: an arbitrary first-order guard over L and a list of second-order body atoms imply the head atom – or ⊥, when the head is none (a goal clause).

• guard : L.Formula (Fin k)

  The first-order guard, over the input vocabulary alone.

• body : List (SOAtom B k)

  The body: second-order atoms, all of them positive.

• head : Option (SOAtom B k)

  The head: a second-order atom, or none for a goal clause.

@[reducible, inline]

abbrev DescriptiveComplexity.HornProgram (L : FirstOrder.Language) (B : SOBlock) (k : ℕ) : Type

An SO-Horn kernel, as data: a finite conjunction of Horn clauses, each implicitly universally quantified over the same k first-order variables.

Equations

• DescriptiveComplexity.HornProgram L B k = List (DescriptiveComplexity.HornClause L B k)

Semantics

def DescriptiveComplexity.HornClause.HeadHolds {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} (c : HornClause L B k) (ρ : B.Assignment A) (v : Fin k → A) : Prop

The truth value of the head of a clause: False for a goal clause.

Equations

• c.HeadHolds ρ v = c.head.elim False fun (h : DescriptiveComplexity.SOAtom B k) => h.Holds ρ v

def DescriptiveComplexity.HornClause.Holds {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (c : HornClause L B k) (ρ : B.Assignment A) (v : Fin k → A) : Prop

A Horn clause holds at a valuation when its guard and all its body atoms force its head.

Equations

• c.Holds ρ v = ((c.guard.Realize v ∧ ∀ a ∈ c.body, a.Holds ρ v) → c.HeadHolds ρ v)

def DescriptiveComplexity.HornProgram.Holds {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (prog : HornProgram L B k) (ρ : B.Assignment A) : Prop

An assignment satisfies a program when every clause holds at every valuation of the universally quantified variables.

Equations

• prog.Holds ρ = ∀ (v : Fin k → A), ∀ c ∈ prog, c.Holds ρ v

Isomorphism-invariance

theorem DescriptiveComplexity.HornClause.holds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (c : HornClause L B k) (ρ : B.Assignment M) (v : Fin k → M) : (c.Holds (B.mapAssign e.toEquiv ρ) fun (j : Fin k) => e (v j)) ↔ c.Holds ρ v

theorem DescriptiveComplexity.HornProgram.holds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (prog : HornProgram L B k) (ρ : B.Assignment M) : prog.Holds (B.mapAssign e.toEquiv ρ) ↔ prog.Holds ρ

theorem DescriptiveComplexity.exists_holds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (prog : HornProgram L B k) : (∃ (ρ : B.Assignment M), prog.Holds ρ) ↔ ∃ (ρ : B.Assignment N), prog.Holds ρ

Horn satisfiability is isomorphism-invariant: a program has a satisfying assignment on one structure iff it has one on any isomorphic structure.

SO-Horn definability

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

A decision problem is SO-Horn definable if, on nonempty finite ordered structures, it is defined by an existential second-order sentence with a Horn kernel: there is a block of relation variables and a Horn program over the ordered expansion of the vocabulary such that the yes-instances are exactly the structures admitting a satisfying assignment.

This is the SO-Horn analogue of DescriptiveComplexity.SigmaSODefinable; a single block suffices, since existential second-order quantifiers merge.

The guards live over L.sum Language.order, and the equivalence is required for every linear order on A, exactly as in DescriptiveComplexity.OrderedFOReduction: since the problem itself does not see the order, this is order-invariant SO-Horn definability. The order is not a convenience here – it is the setting of Grädel's capture theorem, it is what lets a Horn program traverse an unbounded conjunction along the order, and it is forced by closure under ordered first-order reductions (DescriptiveComplexity.SigmaSOHornDefinable.of_orderedReduction), which pull the lexicographic order of the interpreted universe back into the guards.

Equations

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

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

SO-Horn definability only depends on the finite instances of a problem.