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

研究成果: Contribution to journalArticle査読

4 被引用数 (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.

本文言語英語
ページ(範囲)469-498
ページ数30
ジャーナルLogica Universalis
8
3-4
DOI
出版ステータス出版済み - 12 6 2014
外部発表はい

All Science Journal Classification (ASJC) codes

  • Logic
  • Applied Mathematics

フィンガープリント 「Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル