Let be a First-Order Predicate Logic language.
Let be an -Structure.
Given a formula in the language ,
we say is satisfied in if Interpretation
where is the number of free variables in