A \(\mathcal {L}\) -theory T is model-complete if \(T \cup \mathcal {D}(\mathcal {M})\) is complete, where \(\mathcal {D}(\mathcal {M})\) is the diagram of \(\mathcal {M} \models T\) . If \(\mathcal {M} \models T\) and \(\mathcal {A} \sqsubseteq \mathcal {M}\) imply that \(T \cup \mathcal {D}(\mathcal {A})\) is a complete theory, then T is substructure-complete. When the extensions of T we have described are complete, important results follow concerning the complexity of the first-order information codified by a model of T. If, for instance, T is model-complete, then every formula is T-equivalent to an existential \(\mathcal {L}\) -formula and, if T is substructure-complete, every formula is T-equivalent to a quantifier-free \(\mathcal {L}\) -formula. In this chapter we pursue a comprehensive study of model-completeness and of substructure-completeness, starting with the former, weaker property. In Sect. 8.1, model-completeness is defined and simple theories of linear orders are tested for it. In Sect. 8.2 we study the preservation of formulae under substructures and extensions in order to obtain important characterisations of model-completeness. Section 8.3 covers essential material on unions of chains needed to establish Lindström’s test for model-completeness, which immediately yields this property for the algebraic theories discussed in the preceding chapters. From Sect. 8.4 we turn to quantifier elimination and its consequences. After showing how quantifier elimination may be enforced by suitable expansions of a first-order language, we prove a few different quantifier elimination tests. We focus on finite relational languages in Sect. 8.5 and on the connection between quantifier elimination and extensions of embeddings in Sects. 8.6 and 8.7. The final sections of this chapter discuss the impact of quantifier elimination on definability. In Sect. 8.8 we focus on strongly minimal theories, whose models have the least possible amount of parametrically definable sets, and show that, in particular, the theories of torsion-free, divisible abelian groups, of infinite vector spaces and of algebraically closed fields are strongly minimal. The models of strongly minimal theories support the model-theoretic dimension theory developed in Chap. 7 because they have the exchange property, a fact we prove in Sect. 8.8. In Sect. 8.9 we offer a brief discussion of o-minimal theories, linear orders in which the only parametrically definable subsets are the finite unions of points and intervals.

Model-Completeness and Quantifier Elimination

章节
发表日期：

2025年

查看全文

Davide Rizza

摘要

A \(\mathcal {L}\) -theory T is model-complete if \(T \cup \mathcal {D}(\mathcal {M})\) is complete, where \(\mathcal {D}(\mathcal {M})\) is the diagram of \(\mathcal {M} \models T\) . If \(\mathcal {M} \models T\) and \(\mathcal {A} \sqsubseteq \mathcal {M}\) imply that \(T \cup \mathcal {D}(\mathcal {A})\) is a complete theory, then T is substructure-complete. When the extensions of T we have described are complete, important results follow concerning the complexity of the first-order information codified by a model of T. If, for instance, T is model-complete, then every formula is T-equivalent to an existential \(\mathcal {L}\) -formula and, if T is substructure-complete, every formula is T-equivalent to a quantifier-free \(\mathcal {L}\) -formula. In this chapter we pursue a comprehensive study of model-completeness and of substructure-completeness, starting with the former, weaker property. In Sect. 8.1, model-completeness is defined and simple theories of linear orders are tested for it. In Sect. 8.2 we study the preservation of formulae under substructures and extensions in order to obtain important characterisations of model-completeness. Section 8.3 covers essential material on unions of chains needed to establish Lindström’s test for model-completeness, which immediately yields this property for the algebraic theories discussed in the preceding chapters. From Sect. 8.4 we turn to quantifier elimination and its consequences. After showing how quantifier elimination may be enforced by suitable expansions of a first-order language, we prove a few different quantifier elimination tests. We focus on finite relational languages in Sect. 8.5 and on the connection between quantifier elimination and extensions of embeddings in Sects. 8.6 and 8.7. The final sections of this chapter discuss the impact of quantifier elimination on definability. In Sect. 8.8 we focus on strongly minimal theories, whose models have the least possible amount of parametrically definable sets, and show that, in particular, the theories of torsion-free, divisible abelian groups, of infinite vector spaces and of algebraically closed fields are strongly minimal. The models of strongly minimal theories support the model-theoretic dimension theory developed in Chap. 7 because they have the exchange property, a fact we prove in Sect. 8.8. In Sect. 8.9 we offer a brief discussion of o-minimal theories, linear orders in which the only parametrically definable subsets are the finite unions of points and intervals.