HORN-SAT is existential second-order definable

HORN-SAT is Σ₁-definable (DescriptiveComplexity.hornSat_sigmaSODefinable), hence in NP: its kernel is the one of SAT (DescriptiveComplexity.satKernel – every clause contains a true literal) conjoined with the first-order Horn condition (DescriptiveComplexity.hornCondKernel – no clause has two distinct positive literals), over the same single existential block guessing a truth assignment.

Membership in NP is of course not the sharp statement: Horn satisfiability is decidable in linear time (Dowling & Gallier 1984), and HORN-SAT is the canonical complete problem for polynomial time. What the library can state without a definition of PTIME is the hardness half, in DescriptiveComplexity.Problems.HornSat.Hardness.

theorem DescriptiveComplexity.hornSat_sigmaSODefinable : SigmaSODefinable 1 HORNSAT

HORN-SAT is Σ₁-definable: guess a truth assignment and check, in first-order logic, that every clause contains a true literal and that no clause has two positive literals. Since NP is defined as Σ₁-definability, this is the statement HORNSAT ∈ NP.

theorem DescriptiveComplexity.hornSat_mem_NP : NP.Mem HORNSAT

HORN-SAT is in NP.