Which is the definition of a Horn formula being positive?

On p208 of Ebbinghaus' Mathematical Logic

Every Horn formula is a formula in conjunctive normal form, ..., every member of the conjunction has the form (PHI), (PH2) or (PH3):

(PH1) $$q$$

(PH2) $$(q_0 \land ... \land q_n \to q)$$

(PH3) $$(\neg q_0 \lor ... \lor \neg q_n).$$

Horn formulas of the form (PH1) or (PH2) are called positive, those of the form (PH3) negative.

Which is the definition of a Horn formula being positive:

• a formula in CNF, whose members are either PH1 or PH2? (My guess)

• a formula which is either PH1 or PH2? (By the last sentence in the quote) (My guess, after reading the remaining of p208 and p209)

Thanks.

• I would have guessed that a positive Horn formula was a Horn formula which is also a positive formula, which would mean that each conjunct has the form PH1, since PH2 and PH3 are not positive formulas. I seem to recall seeing "strict Horn formula" used for a Horn formula where each conjunct is PH1 or PH2 but I could be remembering wrong, that would have been in a bygone millennium.
– bof
Commented Sep 5, 2020 at 2:09
• I deleted my answer after realizing I had not properly read Ebbinghaus' definition and your question. The notion of positivity makes sense for Horn clauses, i.e. members of the conjunction, which is what I was elaborating on in my answer; but I have nowhere seen it applied, nor do I see how it can be applied according to this definition, to entire Horn formulas. Commented Sep 6, 2020 at 22:20

Compare with a different source: Horn Formulas.

Definition: A formula $$F$$ in CNF is a Horn formula if every disjunction in $$F$$ contains at most one positive literal.

A disjunction in a Horn formula can equivalently be viewed as an implication $$K \to B$$ where $$K$$ is a conjunction of atoms.

According to the above definition, (PH1), (PH2) and (PH3) are all examples of Horn formulas, because (PH2) : $$(q_0 \land \ldots \land q_n \to q)$$, when written in CNF, will be:

$$(\lnot q_0 \lor \ldots \lor \lnot q_n \lor q)$$

and we have only one (and thus: at most one) positive literal: $$q$$.

In conclusion, according to Ebbinghaus definition, an Horn formula is a formula:

$$(\lnot q_0 \lor \ldots \lor \lnot q_n \lor q) \land \ldots \land (\lnot r_0 \lor \ldots \lor \lnot r_m)$$

where $$n$$ can be $$0$$.

Why in the following discussion regarding the satisfiability algorithm for Horn formulas the author consider only the negative and positive ones ?

Simply because, being an Horn formula $$\alpha$$ a conjunction, it will be satisfiable iff every conjunct is, and thus the author consider equivalently the set $$\Delta$$ of members of the conjunction $$\alpha$$.