Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally

In the context of proliferation of many logical systems in the area of mathematical logic and computer science, we present a generalization of forcing in institution-independent model theory which is used to prove two abstract results: Downward Löwenheim-Skolem Theorem (DLST) and Omitting Types Theorem (OTT). We instantiate these general results to many first-order logics, which are, roughly speaking, logics whose sentences can be constructed from atomic formulas by means of Boolean connectives and classical first-order quantifiers. These include first-order logic (FOL), logic of order-sorted algebras (OSA), preorder algebras (POA), as well as their infinitary variants FOL _{ω1, ω}, OSA _{ω1, ω}, POA _{ω1, ω}. In addition to the first technique for proving OTT, we develop another one, in the spirit of institution-independent model theory, which consists of borrowing the Omitting Types Property (OTP) from a simpler institution across an institution comorphism. As a result we export the OTP from FOL to partial algebras (PA) and higher-order logic with Henkin semantics (HNK), and from the institution of FOL_{ω1, ω} to PA_{ω1, ω} and HNK_{ω1, ω}. The second technique successfully extends the domain of application of OTT to non conventional logical systems for which the standard methods may fail.