## Abstract

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.

Original language | English |
---|---|

Pages (from-to) | 469-498 |

Number of pages | 30 |

Journal | Logica Universalis |

Volume | 8 |

Issue number | 3-4 |

DOIs | |

Publication status | Published - Dec 6 2014 |

Externally published | Yes |

## All Science Journal Classification (ASJC) codes

- Logic
- Applied Mathematics