Types
摘要
If \(\mathcal {M}\) be a \(\mathcal {L}\) -structure, ThM is a complete \(\mathcal {L}\) -theory that carries global information about \(\mathcal {M}\) . A finer analysis of \(\mathcal {M}\) may be effected by including the first-order information carried by the elements of M or \(M^{n}\) . For instance, if \(\Phi \) is the set of all \(\mathcal {L}\) -formulae, by fixing \(a \in M\) we determine the set \(p(x) = \{\varphi (x) \in \Phi: \mathcal {M} \models \varphi (a)\}\) . Note that \(p(x) \supseteq ThM\) and, for any \(\mathcal {L}\) -formula \(\psi (x)\) in which at most x occurs free, either \(\psi (x) \in p(x)\) or \(\neg \psi (x) \in p(x)\) . Because of this, we may regard \(p(x)\) as a generalisation of ThM that records first-order information at the level of a single element of M. We call this generalisation a (complete) type. In this chapter we use types to refine our study of \(\mathcal {L}\) -structures. Sections 9.1 and 9.2 introduce key definitions and single out types with special properties. In Sect. 9.3 we briefly look at an application of types outside model theory, which is closely connected with the final sections of Chap. 12 . Section 9.4 is devoted to the connection between types and elementary maps, which prepares the ground for the study of homogeneity in Sect. 9.5. Section 9.6 focusses on atomic structures: it includes the proofs of two fundamental results, i.e. the Omitting Types theorem and the Ryll-Nardzewski theorem. Section 9.7 discusses saturated structures and closes with a discussion of large model-theoretic frameworks known as monster models.