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

Research output: Contribution to journalArticlepeer-review

8 Citations (Scopus)


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 languageEnglish
Pages (from-to)469-498
Number of pages30
JournalLogica Universalis
Issue number3-4
Publication statusPublished - Dec 6 2014
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Logic
  • Applied Mathematics


Dive into the research topics of 'Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally'. Together they form a unique fingerprint.

Cite this