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

The fragment SO-Krom of Grädel (Grädel 1992): existential second-order sentences whose first-order kernel is a conjunction of Krom clauses – 2-clauses – in the quantified relation variables. On ordered structures SO-Krom captures nondeterministic logarithmic space, the NL analogue of the SO-Horn characterization of polynomial time (DescriptiveComplexity.SecondOrderHorn).

Horn and Krom, side by side

Both fragments restrict the occurrences of the second-order variables only, leaving the input vocabulary unconstrained – it is evaluated in the structure, not guessed. They ration the guessed relations differently:

• SO-Horn: any number of negative second-order atoms, at most one positive. A satisfiable Horn formula has a least model, computable by unit propagation, which is what makes the guess deterministic and the class P.
• SO-Krom: at most two second-order atoms, of either sign. A 2-CNF has no least model, so the guess stays a genuine guess; what keeps it below NP is that binary clauses propagate one implication at a time, i.e. along a path. Satisfiability of the instantiated kernel is 2-SAT, decided by reachability in the implication graph.

Neither fragment contains the other: Horn clauses may be arbitrarily wide, Krom clauses may have two positive literals.

The kernel, as data

As in the Horn case, the kernel is represented as data rather than carved out of FirstOrder.Language.BoundedFormula by a syntactic predicate. A clause is

guard(x̄) → ℓ₁ ∨ ℓ₂

where each ℓᵢ is a signed atom in the relation variables (DescriptiveComplexity.KromLit) and guard is an arbitrary first-order formula over the input vocabulary alone (in the definability notion below, over its ordered expansion). A DescriptiveComplexity.KromClause carries its guard and its two literals as Options, so unit clauses and the empty clause (guard → ⊥, the goal clause of the Horn presentation) need no separate treatment; a DescriptiveComplexity.KromProgram is a list of clauses sharing k universally quantified first-order variables. This clausal form is what a reduction consuming an SO-Krom definition needs to see: a discharge emits one propositional 2-clause per clause and per instantiation of the k variables, its literal signs read off the clause.

DescriptiveComplexity.SigmaSOKromDefinable is the resulting definability notion; it is closed under (ordered) first-order reductions by DescriptiveComplexity.SecondOrderKromPull, which is what makes it a DescriptiveComplexity.ComplexityClass – the class DescriptiveComplexity.NL of DescriptiveComplexity.LogSpace.

Krom programs

structure DescriptiveComplexity.KromLit (B : SOBlock) (k : ℕ) : Type

A literal in the relation variables of a block: an atom together with a sign (positive = false for a negated atom).

• atom : SOAtom B k

  The underlying second-order atom.

• positive : Bool

  The sign of the literal: true for the atom, false for its negation.

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

A Krom clause over the input vocabulary L and the block B, with k universally quantified first-order variables: an arbitrary first-order guard over L implies the disjunction of at most two signed second-order literals. A none literal is absent, so a clause with both literals absent is the goal clause guard → ⊥.

• guard : L.Formula (Fin k)

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

• lit₁ : Option (KromLit B k)

  The first literal of the clause, if any.

• lit₂ : Option (KromLit B k)

  The second literal of the clause, if any.

@[reducible, inline]

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

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

Equations

• DescriptiveComplexity.KromProgram L B k = List (DescriptiveComplexity.KromClause L B k)

Semantics

def DescriptiveComplexity.KromLit.Holds {B : SOBlock} {k : ℕ} {A : Type} (l : KromLit B k) (ρ : B.Assignment A) (v : Fin k → A) : Prop

The truth value of a literal: its atom, or the negation of its atom.

Equations

• l.Holds ρ v = if l.positive = true then l.atom.Holds ρ v else ¬l.atom.Holds ρ v

def DescriptiveComplexity.KromLit.slotHolds {B : SOBlock} {k : ℕ} {A : Type} (o : Option (KromLit B k)) (ρ : B.Assignment A) (v : Fin k → A) : Prop

The truth value of one of the two literal slots of a clause: False when the literal is absent.

Equations

• DescriptiveComplexity.KromLit.slotHolds o ρ v = o.elim False fun (l : DescriptiveComplexity.KromLit B k) => l.Holds ρ v

theorem DescriptiveComplexity.KromLit.slotHolds_iff {B : SOBlock} {k : ℕ} {A : Type} {o : Option (KromLit B k)} {ρ : B.Assignment A} {v : Fin k → A} : slotHolds o ρ v ↔ ∃ l ∈ o, l.Holds ρ v

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

A Krom clause holds at a valuation when its guard forces one of its (at most two) literals.

Equations

• c.Holds ρ v = (c.guard.Realize v → DescriptiveComplexity.KromLit.slotHolds c.lit₁ ρ v ∨ DescriptiveComplexity.KromLit.slotHolds c.lit₂ ρ v)

def DescriptiveComplexity.KromProgram.Holds {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] (prog : KromProgram 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.KromLit.holds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (l : KromLit B k) (ρ : B.Assignment M) (v : Fin k → M) : (l.Holds (B.mapAssign e.toEquiv ρ) fun (j : Fin k) => e (v j)) ↔ l.Holds ρ v

theorem DescriptiveComplexity.KromLit.slotHolds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (o : Option (KromLit B k)) (ρ : B.Assignment M) (v : Fin k → M) : (slotHolds o (B.mapAssign e.toEquiv ρ) fun (j : Fin k) => e (v j)) ↔ slotHolds o ρ v

theorem DescriptiveComplexity.KromClause.holds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (c : KromClause 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.KromProgram.holds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (prog : KromProgram L B k) (ρ : B.Assignment M) : prog.Holds (B.mapAssign e.toEquiv ρ) ↔ prog.Holds ρ

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

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

SO-Krom definability

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

A decision problem is SO-Krom definable if, on nonempty finite ordered structures, it is defined by an existential second-order sentence with a Krom kernel: there is a block of relation variables and a Krom 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-Krom analogue of DescriptiveComplexity.SigmaSOHornDefinable; a single block suffices, since existential second-order quantifiers merge.

As for SO-Horn, the guards live over L.sum Language.order and the equivalence is required for every linear order on A, so this is order-invariant SO-Krom definability: the order is the setting of Grädel's capture theorem, and it is forced by closure under ordered first-order reductions (DescriptiveComplexity.SigmaSOKromDefinable.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.sigmaSOKromDefinable_congr {L : FirstOrder.Language} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : SigmaSOKromDefinable P ↔ SigmaSOKromDefinable Q

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