scholarly journals MODEL COMPLETENESS OF O-MINIMAL FIELDS WITH CONVEX VALUATIONS

2015 ◽  
Vol 80 (1) ◽  
pp. 234-250 ◽  
Author(s):  
CLIFTON F. EALY ◽  
JANA MAŘÍKOVÁ
Keyword(s):  
Residue Field ◽  
Quantifier Elimination ◽  
Elementary Extension ◽  
Model Completeness ◽  
Elementary Substructure ◽  
The Way

AbstractWe let R be an o-minimal expansion of a field, V a convex subring, and (R0,V0) an elementary substructure of (R,V). Our main result is that (R,V) considered as a structure in a language containing constants for all elements of R0 is model complete relative to quantifier elimination in R, provided that kR (the residue field with structure induced from R) is o-minimal. Along the way we show that o-minimality of kR implies that the sets definable in kR are the same as the sets definable in k with structure induced from (R,V). We also give a criterion for a superstructure of (R,V) being an elementary extension of (R,V).

T-convexity and tame extensions

1995 ◽  
Vol 60 (1) ◽  
pp. 74-102 ◽  
Author(s):  
Lou van den Dries ◽  
Adam H. Lewenberg
Keyword(s):  
Convex Hull ◽  
Residue Field ◽  
Quantifier Elimination ◽  
Convex Hulls ◽  
Minimal Extension ◽  
Elementary Substructure ◽  
Real Closed Fields ◽  
Closed Fields ◽  
Natural Expansion

AbstractLet T be a complete o-minimal extension of the theory of real closed fields. We characterize the convex hulls of elementary substructures of models of T and show that the residue field of such a convex hull has a natural expansion to a model of T. We give a quantifier elimination relative to T for the theory of pairs (ℛ, V) where ℛ ⊨ T and V ≠ ℛ is the convex hull of an elementary substructure of ℛ. We deduce that the theory of such pairs is complete and weakly o-minimal. We also give a quantifier elimination relative to T for the theory of pairs with ℛ a model of T and a proper elementary substructure that is Dedekind complete in ℛ. We deduce that the theory of such “tame” pairs is complete.

scholarly journals Model Completeness, Uniform Interpolants and Superposition Calculus

2021 ◽  
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Automated Reasoning ◽  
Quantifier Elimination ◽  
Effective Solution ◽  
Model Completeness ◽  
Present Contribution ◽  
First Order ◽  
Reduction Strategies ◽  
Infinite State Systems ◽  
Infinite State ◽  
Superposition Calculus

AbstractUniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

More on definable sets of p-adic numbers

1988 ◽  
Vol 53 (3) ◽  
pp. 912-920 ◽  
Author(s):  
Philip Scowcroft
Keyword(s):  
Cross Section ◽  
Quantifier Elimination ◽  
Order Theory ◽  
Model Completeness ◽  
First Order ◽  
First Order Theory ◽  
Ordered Fields ◽  
Definable Sets ◽  
The Cross ◽  
Primitive Recursive

To eliminate quantifiers in the first-order theory of the p-adic field Qp, Ax and Kochen use a language containing a symbol for a cross-section map n → pn from the value group Z into Qp [1, pp. 48–49]. The primitive-recursive quantifier eliminations given by Cohen [2] and Weispfenning [10] also apply to a language mentioning the cross-section, but none of these authors seems entirely happy with his results. As Cohen says, “all the operations… introduced for our simple functions seem natural, with the possible exception of the map n → pn” [2, p. 146]. So all three authors show that various consequences of quantifier elimination—completeness, decidability, model-completeness—also hold for a theory of Qp not employing the cross-section [1, p. 453; 2, p. 146; 10, §4]. Macintyre directs a more specific complaint against the cross-section [5, p. 605]. Elementary formulae which use it can define infinite discrete subsets of Qp; yet infinite discrete subsets of R are not definable in the language of ordered fields, and so certain analogies between Qp and R suggested by previous model-theoretic work seem to break down.To avoid this problem, Macintyre gives up the cross-section and eliminates quantifiers in a theory of Qp written just in the usual language of fields supplemented by a predicate V for Qp's valuation ring and by predicates Pn for the sets of nth powers in Qp (for all n ≥ 2).

Stability theory for topological logic, with applications to topological modules

1986 ◽  
Vol 51 (3) ◽  
pp. 755-769 ◽  
Author(s):  
T. G. Kucera
Keyword(s):  
Stability Theory ◽  
Quantifier Elimination ◽  
Order Logic ◽  
First Order Logic ◽  
Elementary Substructure ◽  
First Order ◽  
Topological Modules ◽  
Individual Variables ◽  
The Stability ◽  
First Main Theorem

In this paper I show how to develop stability theory within the context of the topological logic first introduced by McKee [Mc 76], Garavaglia [G 78] and Ziegler [Z 76]. I then study some specific applications to topological modules; in particular I prove two quantifier élimination theorems, one a generalization of a result of Garavaglia.In the first section I present a summary of basic results on topological model theory, mostly taken from the book of Flum and Ziegler [FZ 80]. This is done primarily to fix notation, but I also introduce the notion of an Lt-elementary substructure. The important point with this concept, as with many others, appears to be to allow only individuals to appear as parameters, not open sets.In the second section I begin the study of stability theory for Lt. I first develop a translation of the topological language Lt into an ordinary first-order language L*. The first main theorem is (2.3), which shows that the translation is faithful to the model-theoretic content of Lt, and provides the necessary tools for studying Lt theories in the context of ordinary first-order logic. The translation allows me to consider individual stability theory for Lt: the stability-theoretic study of those types of Lt in which only individual variables occur freely and in which only individuals occur as parameters. I originally developed this stability theory entirely within Lt; the fact that the theorems and their proofs were virtually identical to those in ordinary first order logic suggested the reduction from Lt to L*.

On the angular component map modulo P

1990 ◽  
Vol 55 (3) ◽  
pp. 1125-1129 ◽  
Author(s):  
Johan Pas
Keyword(s):  
Natural Language ◽  
Residue Field ◽  
Quantifier Elimination ◽  
Function Symbol ◽  
Valued Fields ◽  
Valued Field ◽  
Angular Component ◽  
Henselian Valued Fields ◽  
Almost All ◽  
Component Map

In [10] we introduced a new first order language for valued fields. This language has three sorts of variables, namely variables for elements of the valued field, variables for elements of the residue field and variables for elements of the value group. contains symbols for the standard field, residue field, and value group operations and a function symbol for the valuation. Essential in our language is a function symbol for an angular component map modulo P, which is a map from the field to the residue field (see Definition 1.2).For this language we proved a quantifier elimination theorem for Henselian valued fields of equicharacteristic zero which possess such an angular component map modulo P [10, Theorem 4.1]. In the first section of this paper we give some partial results on the existence of an angular component map modulo P on an arbitrary valued field.By applying the above quantifier elimination theorem to ultraproducts ΠQp/D, we obtained a quantifier elimination, in the language , for the p-adic field Qp; and this elimination is uniform for almost all primes p [10, Corollary 4.3]. In §2 we prove that our language is essentially stronger than the natural language for p-adic fields in the sense that the angular component map modulo P cannot be defined, uniformly for almost all p, in terms of the natural language for p-adic fields.

Quantifier elimination in valued Ore modules

2010 ◽  
Vol 75 (3) ◽  
pp. 1007-1034 ◽  
Author(s):  
Luc Bélair ◽  
Françoise Point
Keyword(s):  
Residue Field ◽  
Quantifier Elimination ◽  
Difference Operators ◽  
Independence Property ◽  
Valued Fields ◽  
A Chain

AbstractWe consider valued fields with a distinguished isometry or contractive derivation as valued modules over the Ore ring of difference operators. Under certain assumptions on the residue field, we prove quantifier elimination first in the pure module language, then in that language augmented with a chain of additive subgroups, and finally in a two-sorted language with a valuation map. We apply quantifier elimination to prove that these structures do not have the independence property.

T-convexity and tame extensions II

1997 ◽  
Vol 62 (1) ◽  
pp. 14-34 ◽  
Author(s):  
Lou van den Dries
Keyword(s):  
Residue Class ◽  
Residue Field ◽  
Elementary Substructure ◽  
Real Closed Fields ◽  
Minimal Theory ◽  
Ordered Field ◽  
Closed Fields

I solve here some problems left open in “T-convexity and Tame Extensions” [9]. Familiarity with [9] is assumed, and I will freely use its notations. In particular, T will denote a complete o-minimal theory extending RCF, the theory of real closed fields. Let (, V) ⊨ Tconvex, let = V/m(V) be the residue field, with residue class map x ↦ : V ↦ , and let υ: → Γ be the associated valuation. “Definable” will mean “definable with parameters”. The main goal of this article is to determine the structure induced by (, V) on its residue fieldand on its value group Γ. In [9] we expanded the ordered field to a model of T as follows. Take a tame elementary substructure ′ of such that R′ ⊆ V and R′ maps bijectively onto under the residue class map, and make this bijection into an isomorphism ′ ≌ of T-models. (We showed such ′ exists, and that this gives an expansion of to a T-model that is independent of the choice of ′.).

Quantifier elimination in tame infinite p-adic fields

2001 ◽  
Vol 66 (3) ◽  
pp. 1493-1503
Author(s):  
Ingo Brigandt
Keyword(s):  
Natural Language ◽  
Residue Field ◽  
Quantifier Elimination ◽  
Valued Fields ◽  
Language Extension ◽  
Residue Fields

AbstractWe give an answer to the question as to whether quantifier elimination is possible in some infinite algebraic extensions of ℚp (‘infinite p-adic fields’) using a natural language extension. The present paper deals with those infinite p-adic fields which admit only tamely ramified algebraic extensions (so-called tame fields). In the case of tame fields whose residue fields satisfy Kaplansky's condition of having no extension of p-divisible degree quantifier elimination is possible when the language of valued fields is extended by the power predicates Pn introduced by Macintyre and, for the residue field, further predicates and constants. For tame infinite p-adic fields with algebraically closed residue fields an extension by Pn predicates is sufficient.

scholarly journals Counting algebraic points in expansions of o-minimal structures by a dense set

2020 ◽  
Author(s):  
Pantelis E Eleftheriou
Keyword(s):  
Rational Points ◽  
Real Field ◽  
Elementary Substructure ◽  
The Real ◽  
Semialgebraic Set ◽  
Minimal Structure ◽  
Infinite Set ◽  
Dense Set ◽  
The Way

Abstract The Pila–Wilkie theorem states that if a set $X\subseteq \mathbb{R}^n$ is definable in an o-minimal structure $\mathcal{R}$ and contains ‘many’ rational points, then it contains an infinite semialgebraic set. In this paper, we extend this theorem to an expansion $\widetilde{\mathcal{R}}=\langle {\mathcal{R}}, P\rangle$ of ${\mathcal{R}}$ by a dense set P, which is either an elementary substructure of ${\mathcal{R}}$, or it is $\mathrm{dcl}$-independent, as follows. If X is definable in $\widetilde{\mathcal{R}}$ and contains many rational points, then it is dense in an infinite semialgebraic set. Moreover, it contains an infinite set which is ${\emptyset}$-definable in $\langle \overline{\mathbb{R}}, P\rangle$, where $\overline{\mathbb{R}}$ is the real field. Along the way we introduce the notion of the ‘algebraic trace part’ $X^{{\, alg}}_t$ of any set $X\subseteq \mathbb{R}^n$, and we show that if X is definable in an o-minimal structure, then $X^{{\, alg}}_t$ coincides with the usual algebraic part of X.

scholarly journals Transfer Principles in Henselian Valued Fields

2021 ◽  
Vol 27 (2) ◽  
pp. 222-223
Author(s):  
Pierre Touchard
Keyword(s):  
Term Structure ◽  
Residue Field ◽  
Intermediate Structure ◽  
Elementary Extension ◽  
Similar Reduction ◽  
Valued Fields ◽  
Valued Field ◽  
Henselian Valued Fields ◽  
Leading Term ◽  
Transfer Principles

AbstractIn this thesis, we study transfer principles in the context of certain Henselian valued fields, namely Henselian valued fields of equicharacteristic $0$ , algebraically closed valued fields, algebraically maximal Kaplansky valued fields, and unramified mixed characteristic Henselian valued fields with perfect residue field. First, we compute the burden of such a valued field in terms of the burden of its value group and its residue field. The burden is a cardinal related to the model theoretic complexity and a notion of dimension associated to $\text {NTP}_2$ theories. We show, for instance, that the Hahn field $\mathbb {F}_p^{\text {alg}}((\mathbb {Z}[1/p]))$ is inp-minimal (of burden 1), and that the ring of Witt vectors $W(\mathbb {F}_p^{\text {alg}})$ over $\mathbb {F}_p^{\text {alg}}$ is not strong (of burden $\omega $ ). This result extends previous work by Chernikov and Simon and realizes an important step toward the classification of Henselian valued fields of finite burden. Second, we show a transfer principle for the property that all types realized in a given elementary extension are definable. It can be written as follows: a valued field as above is stably embedded in an elementary extension if and only if its value group is stably embedded in the corresponding extension of value groups, its residue field is stably embedded in the corresponding extension of residue fields, and the extension of valued fields satisfies a certain algebraic condition. We show, for instance, that all types over the power series field $\mathbb {R}((t))$ are definable. Similarly, all types over the quotient field of $W(\mathbb {F}_p^{\text {alg}})$ are definable. This extends previous work of Cubides and Delon and of Cubides and Ye.These distinct results use a common approach, which has been developed recently. It consists of establishing first a reduction to an intermediate structure called the leading term structure, or $\operatorname {\mathrm {RV}}$ -sort, and then of reducing to the value group and residue field. This leads us to develop similar reduction principles in the context of pure short exact sequences of abelian groups.Abstract prepared by Pierre Touchard.E-mail: [email protected]: https://miami.uni-muenster.de/Record/a612cf73-0a2f-42c4-b1e4-7d28934138a9

Sign in / Sign up

Export Citation Format

Share Document