The logic of metric structures was introduced by Ben Yaacov, Berenstein , Henson and Usvyatsov. It is a version of continuous logic which allows fruitful model theory for  many kinds of metric structures .There are many aspects of   this logic which make it similar to  first order logic, like compactness, a complete proof system, an omitting types theorem for complete  types  etc. But when one tries to generalize the omitting type criteria to general (non-complete) types the problem turns out to be essentially more difficult than the first order situation.For instance one can have two types (in a complete theory) that each one can be omitted , but they can not be omitted simultaneously.