TY - JOUR
T1 - Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally
AU - Găină, Daniel
N1 - Publisher Copyright:
© 2013, Springer Basel.
PY - 2014/12/6
Y1 - 2014/12/6
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84916238915&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84916238915&partnerID=8YFLogxK
U2 - 10.1007/s11787-013-0090-0
DO - 10.1007/s11787-013-0090-0
M3 - Article
AN - SCOPUS:84916238915
VL - 8
SP - 469
EP - 498
JO - Logica Universalis
JF - Logica Universalis
SN - 1661-8297
IS - 3-4
ER -