Terminology: "true", "entailed", "provable", "holds"

General
18

if T ⊆ Horn_1, if s ∈ Horn_2, then if T ⊧ s then T ⊢ s.

If this is in Prolog and s is a Horn goal, then what is entailed by T should be the negation of s, no? So this should be:

if T ⊆ Horn_1, if s ∈ Horn_2, then if T ⊧ ¬s then T ∪ s ⊢ ⊥ .

Else I’m a bit confused.

Edit: how do you get syntax highlighting in comments that aren’t obviously Prolog?

How do you get syntax highlighting in comments that aren’t obviously Prolog?