Semantic Entailment

Let be a First-Order Predicate Logic Language.
Let be a set of Sentences in and let be a Sentence in
We say semantically entails or
if is Satisfied in every Model of .

Furthermore, let be a set of formulae in and
Introduce new constants in
one for each free variable occurring in
For any ,
let be the Sentence in the new language
obtained from by replacing free vars with the new constants
Set
We say entails or , if