Paper Info
Title
Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally.
Abstract
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 \({{\bf FOL}_{\omega_1,\omega}}\) , \({{\bf OSA}_{\omega_1,\omega}}\) , \({{\bf POA}_{\omega_1,\omega}}\) . 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 \({{\bf FOL}_{\omega_1,\omega}}\) to \({{\bf PA}_{\omega_1,\omega}}\) and \({{\bf HNK}_{\omega_1,\omega}}\) . The second technique successfully extends the domain of application of OTT to non conventional logical systems for which the standard methods may fail.
Year
DOI
Venue
2014
10.1007/s11787-013-0090-0
Logica Universalis
Keywords
Field
DocType
Primary 03C25,Secondary 03C95,Institution,model theory,forcing
Discrete mathematics,Algorithm,Preorder,Omega,Forcing (mathematics),Model theory,Löwenheim–Skolem theorem,Mathematics,Mathematical logic
Journal
Volume
Issue
ISSN
8
3-4
1661-8297
Citations 
PageRank 
References 
2
0.38
30
Authors
1
Name
Order
Citations
PageRank
Daniel Găină1425.30