Horn formulas and intersection closure

Horn clauses have at most one positive literal occurrence. Models of Horn formulas are closed under coordinatewise AND. Conversely, every AND-closed Boolean relation on finitely many coordinates has a Horn definition without auxiliary variables. Empty and nullary relations are included. The finite-extension proof is original; the characterization is [Bod26], Lemma 6.31, pp. 75–76 (September 14, 2026 version), with finite coordinate types replacing numbered variables and false/true replacing 0/1. See [Che06], Section 4, for the corresponding Boolean CSP tractability cases.

Flipping every literal polarity gives the dual Horn characterization for coordinatewise OR. These are semantic normal-form theorems; no efficient construction of the normal form is claimed.

Main results

• Cslib.Logic.PL.isPolymorphism_and_iff_exists_hornCNF: AND preservation iff Horn definability.
• Cslib.Logic.PL.isPolymorphism_or_iff_exists_dualHornCNF: the dual OR characterization.

def Cslib.Logic.PL.Clause.IsHorn {V : Type u_1} (c : Clause V) : Prop

At most one positive literal occurrence, counting repetitions.

def Cslib.Logic.PL.CNF.IsHorn {V : Type u_1} (φ : CNF V) : Prop

Every clause has at most one positive literal occurrence.

theorem Cslib.Logic.PL.isPolymorphism_and_iff {V : Type u_1} (R : Set (V → Bool)) : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 && a 1) R ↔ ∀ x ∈ R, ∀ y ∈ R, (fun (i : V) => x i && y i) ∈ R

Binary AND preservation is closure under pointwise conjunction.

theorem Cslib.Logic.PL.Clause.IsHorn.positive_unique {V : Type u_1} {c : Clause V} (hc : c.IsHorn) {p q : Literal V} (hp : p ∈ c) (hq : q ∈ c) (hp' : p.2 = true) (hq' : q.2 = true) : p = q

A Horn clause cannot have two different positive literals. Repetition still counts in IsHorn, so this necessary condition is not a characterization.

theorem Cslib.Logic.PL.Clause.eval_and_of_isHorn {V : Type u_1} {c : Clause V} (hc : c.IsHorn) {x y : V → Bool} (hx : eval x c = true) (hy : eval y c = true) : eval (fun (i : V) => x i && y i) c = true

A Horn clause is preserved by coordinatewise conjunction, including negative-only and empty clauses, repeated negative literals and tautologies.

theorem Cslib.Logic.PL.CNF.isPolymorphism_and {V : Type u_1} {φ : CNF V} (hφ : φ.IsHorn) : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 && a 1) {a : V → Bool | eval a φ = true}

Models of a Horn CNF are AND-preserved.

theorem Cslib.Logic.PL.mem_of_extensions_of_and {V : Type u_1} [Finite V] {R : Set (V → Bool)} (hR : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 && a 1) R) (a : V → Bool) (hne : ∃ b ∈ R, ∀ (i : V), a i = true → b i = true) (hext : ∀ (i : V), a i = false → ∃ b ∈ R, b i = false ∧ ∀ (j : V), a j = true → b j = true) : a ∈ R

Finite intersections of extensions of a tuple recover that tuple when every false coordinate can be made false by such an extension. Nonemptiness handles nullary relations.

theorem Cslib.Logic.PL.exists_separating_clause_of_and {V : Type u_1} [Finite V] {R : Set (V → Bool)} (hR : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 && a 1) R) {a : V → Bool} (ha : a ∉ R) : ∃ (c : Clause V), c.IsHorn ∧ (∀ b ∈ R, Clause.eval b c = true) ∧ Clause.eval a c = false

A tuple outside a finite AND-closed relation is separated by a Horn clause over the same variables.

theorem Cslib.Logic.PL.isPolymorphism_and_iff_exists_hornCNF {V : Type u_1} [Finite V] (R : Set (V → Bool)) : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 && a 1) R ↔ ∃ (φ : CNF V), φ.IsHorn ∧ ∀ (a : V → Bool), a ∈ R ↔ CNF.eval a φ = true

Finite Boolean AND-preserved relations are exactly Horn CNF relations, with no auxiliaries. Empty relations and empty coordinate types are included.

def Cslib.Logic.PL.Clause.flip {V : Type u_1} (c : Clause V) : Clause V

Complement the polarity of every literal, without changing variables or occurrences.

def Cslib.Logic.PL.CNF.flip {V : Type u_1} (φ : CNF V) : CNF V

Complement every literal polarity in a formula.

def Cslib.Logic.PL.Clause.IsDualHorn {V : Type u_1} (c : Clause V) : Prop

A dual Horn clause has at most one negative literal occurrence.

def Cslib.Logic.PL.CNF.IsDualHorn {V : Type u_1} (φ : CNF V) : Prop

A formula is dual Horn when all its clauses are dual Horn.

theorem Cslib.Logic.PL.Clause.isDualHorn_iff {V : Type u_1} (c : Clause V) : c.IsDualHorn ↔ (List.filter (fun (l : Literal V) => !l.2) c).length ≤ 1

The polarity-flipping definition counts exactly the negative literal occurrences.

theorem Cslib.Logic.PL.CNF.isDualHorn_iff {V : Type u_1} (φ : CNF V) : φ.IsDualHorn ↔ ∀ c ∈ φ, c.IsDualHorn

Dual Horn syntax can be checked one clause at a time.

@[simp]

theorem Cslib.Logic.PL.Clause.flip_flip {V : Type u_1} (c : Clause V) : c.flip.flip = c

Complementing polarities is an involution on clauses.

@[simp]

theorem Cslib.Logic.PL.CNF.flip_flip {V : Type u_1} (φ : CNF V) : φ.flip.flip = φ

Complementing polarities is an involution on formulas.

@[simp]

theorem Cslib.Logic.PL.Clause.eval_flip {V : Type u_1} (c : Clause V) (a : V → Bool) : eval a c.flip = eval (fun (i : V) => !a i) c

Flipping polarities evaluates a clause under the complemented assignment.

@[simp]

theorem Cslib.Logic.PL.CNF.eval_flip {V : Type u_1} (φ : CNF V) (a : V → Bool) : eval a φ.flip = eval (fun (i : V) => !a i) φ

Flipping polarities evaluates a formula under the complemented assignment.

@[simp]

theorem Cslib.Logic.PL.CNF.satisfiable_flip {V : Type u_1} (φ : CNF V) : φ.flip.Satisfiable ↔ φ.Satisfiable

Complementing all variables preserves satisfiability.

theorem Cslib.Logic.PL.isPolymorphism_or_iff_and_complement {V : Type u_1} (R : Set (V → Bool)) : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 || a 1) R ↔ IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 && a 1) {a : V → Bool | (fun (i : V) => !a i) ∈ R}

Coordinatewise OR preservation becomes AND preservation under complementation.

theorem Cslib.Logic.PL.CNF.isPolymorphism_or {V : Type u_1} {φ : CNF V} (hφ : φ.IsDualHorn) : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 || a 1) {a : V → Bool | eval a φ = true}

Models of a dual Horn CNF are OR-preserved, with no finiteness requirement on variables.

theorem Cslib.Logic.PL.isPolymorphism_or_iff_exists_dualHornCNF {V : Type u_1} [Finite V] (R : Set (V → Bool)) : IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 || a 1) R ↔ ∃ (φ : CNF V), φ.IsDualHorn ∧ ∀ (a : V → Bool), a ∈ R ↔ CNF.eval a φ = true

Finite OR-preserved Boolean relations are exactly dual Horn CNF relations, without auxiliary variables.