
TL;DR
The paper constructs two ordered structures with identical one-variable definable sets, illustrating limitations in axiomatizing o-minimal theories and implications for definable completeness and the pigeonhole principle.
Contribution
It provides a counterexample showing that definable completeness does not imply the pigeonhole principle, challenging previous assumptions in o-minimal theory.
Findings
Counterexample to axiomatization of o-minimal theories with one-variable sets
Definable completeness does not imply the pigeonhole principle
Partial answer to questions by Schoutens and Fornasiero
Abstract
We give an example of two ordered structures M, N in the same language L with the same universe, the same order and admitting the same one-variable definable subsets such that M is a model of the common theory of o-minimal L-structures and N admits a definable, closed, bounded, and discrete subset and a definable injective self-mapping of that subset which is not surjective. This answers negatively two questions by Schoutens; the first being whether there is an axiomatization of the common theory of o-minimal structures in a given language by conditions on one-variable definable sets alone. The second being whether definable completeness and type completeness imply the pigeonhole principle. It also partially answers a question by Fornasiero asking whether definable completeness of an expansion of a real closed field implies the pigeonhole principle.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
\newaliascnt
lemmatheorem \aliascntresetthelemma \newaliascntremarktheorem \aliascntresettheremark \newaliascntcorollarytheorem \aliascntresetthecorollary \newaliascntpropositiontheorem \aliascntresettheproposition \newaliascntquestiontheorem \aliascntresetthequestion \newaliascntfacttheorem \aliascntresetthefact \newaliascntconjecturetheorem \aliascntresettheconjecture
\newaliascntexampletheorem \aliascntresettheexample \newaliascntdefinitiontheorem \aliascntresetthedefinition
Pseudo-finite sets, pseudo-o-minimality
Nadav Meir
Department of Mathematics, Ben Gurion University of the Negev
P.O.B. 653, Be’er Sheva 8410501, Israel.
Abstract.
We give an example of two ordered structures in the same language with the same universe, the same order and admitting the same one-variable definable subsets such that is a model of the common theory of o-minimal -structures and admits a definable, closed, bounded, and discrete subset and a definable injective self-mapping of that subset which is not surjective. This answers negatively two questions by Schoutens; the first being whether there is an axiomatization of the common theory of o-minimal structures in a given language by conditions on one-variable definable sets alone. The second being whether definable completeness and type completeness imply the pigeonhole principle. It also partially answers a question by Fornasiero asking whether definable completeness of an expansion of a real closed field implies the pigeonhole principle.
Key words and phrases:
Definably complete, Type complete, pseudo-o-minimal, o-minimalism, pigeonhole principle
2000 Mathematics Subject Classification:
03C64
The work in this paper is part of the author’s Ph.D. studies at the Department of Mathematics, Ben-Gurion University of the Negev under the supervision of Assaf Hasson.
The author was partially supported by ISF Grant 181/60 and the Hillel Gauchman scholarship.
1. Introduction
o-minimality is not preserved under ultraproducts, as shown in the following example:
Example \theexample.
Let where is a binary relation symbol and is a unary predicate. For every , let be a structure interpreting as a dense linear order without end points and as a set of points of size . Then each is o-minimal. But for any non-principal ultrafilter on , in the ultraproduct , the definable set is infinite and discrete, thus the ultraproduct of o-minimal structures need not be o-minimal.
Section 1 can be generalized to any first-order language . So By Łos’ Theorem, given a first-order language , there is no first-order theory , such that is o-minimal for every -structure .
Here we focus our attention on some properties implied by o-minimality which are first-order, i.e., those properties which both hold in all o-minimal structures, and, given a language , can be axiomatized by a set of -sentences. Rigorously, we follow the conventions from [Sch14], defined below:
Definition \thedefinition.
Given a language , let be the set of all -sentences satisfied in every o-minimal -structure.
An -structure for is pseudo-o-minimal if .
Fact \thefact ([Sch14, Corollary 10.2]).
An -structure for is pseudo-o-minimal if and only if is elementarily equivalent to an ultraproduct of o-minimal structures.
The following two definitions are examples of first-order weakenings of o-minimality.
Definition \thedefinition.
An expansion of a dense linear order without endpoints is definably complete if every definable subset of has a least upper bound.
Definition \thedefinition.
An expansion of a dense linear order without endpoints is locally o-minimal if for any definable subset and any there are such that and if or then either or .
Notice that both definable completeness and local o-minimality, in a given language , are axiomatized by first-order schemes which hold in any o-minimal structure. Thus, any pseudo-o-minimal -structure is definably complete and locally o-minimal.
Fornasiero, Hieronymi, Miller, Schoutens, Servi and others proved many tameness properties for definably complete and for locally o-minimal structures. (See, e.g, [Mil01, Hie11, For10, FS11, For13, Hie13, Sch14, FH15].) Citing all tameness properties proved in this area will be longer than this paper, so we give two elementary examples by Miller:
Fact \thefact ([Mil01, Corollary 1.5]).
Let be an expansion of a dense linear order without endpoints. Then the following are equivalent:
- (1)
* is definably complete.* 2. (2)
* has the intermediate value property, i.e., the image of an interval under a definable continuous map is an interval.* 3. (3)
Intervals in are definably connected, i.e. for every interval and every disjoint open definable subsets , if , then either or . 4. (4)
* is definably connected.*
Fact \thefact ([Mil01, Proposition 1.10]).
Let be definably complete. Let be definable and continuous with closed and bounded. Then is closed and bounded. In particular, If is definable and continuous with closed and bounded, then achieves a maximum and a minimum on .
In [Sch14], Schoutens presented a strengthening of local o-minimality by the name of type completeness, as defined below. In a sense this strengthening extends the locality to :
Definition \thedefinition.
An expansion of a dense linear order without endpoints is type complete if it is locally o-minimal and, in addition, for any definable subset there are such that if or , then either or .
Type completeness is a first-order scheme, and therefore satisfied by any pseudo-o-minimal structure.
Several tameness results were proved for definably complete type complete structures in [Sch14]. For example, a version of o-minimal cell decomposition called quasi-cell decomposition ([Sch14, Theorem 8.10]) and the following monotonicity theorem:
Fact \thefact ([Sch14, Theorem 3.2]).
Let be a definably complete type complete structure. The set of discontinuities of a one-variable definable map is discrete, closed, and bounded, and consists entirely of jump discontinuities. Moreover, there is a definable discrete, closed, bounded subset so that in between any two consecutive points of , the map is monotone, that is to say, either strictly increasing, strictly decreasing, or constant.
Of particular importance in the study of definably complete structures are the definable pseudo-finite sets, as defined below.
Definition \thedefinition.
Let be a definably complete structure. A definable subset is pseudo-finite if it is closed, bounded, and discrete.
These definable sets play a role in each of the papers cited above. We follow the convention in [For10, For13], where there is an extensive study of pseudo-finite sets and their tameness properties. In [For13], the wording was justified in the definably complete context by saying that pseudo-finite sets are first-order analogue of finite subsets of , with evidence given by numerous tameness properties of such sets.
One must not confuse pseudo-finite sets defined above with pseudo--finite sets, as we define below, coined in [Sch14]. Though, as we will see in Section 1 the two definitions coincide if is assumed to be pseudo-o-minimal.
Definition \thedefinition.
Let be a pseudo-o-minimal structure. A definable set is pseudo--finite if satisfies the common theory of o-minimal structures expanded by a unary predicate for a distinguished finite subset.
The following section can be immediately extracted from [Sch14, Corollary 12.6] together with [Sch14, Theorem 12.7].
Fact \thefact.
Let be a pseudo-o-minimal structure. A definable set is pseudo-finite if and only if it is pseudo--finite.
A tameness property of pseudo-finite sets occurring naturally is “the discrete pigeonhole principle” [Sch14]. (Or just “the pigeonhole principle” in [For10, For13].)
Definition \thedefinition.
An expansion of a dense linear order without endpoints has the pigeonhole principle if for any pseudo-finite and definable , if f is injective, then it is surjective.
We remark that the pigeonhole principle can be formulated as “every pseudo-finite set is definably Dedekind finite”, and as this is a first-order scheme, every pseudo-o-minimal structure has the pigeonhole principle.
In [For10] and [For13], Fornasiero conjectured the following:
Conjecture \theconjecture.
If is a definably complete expansion of a real closed field, then has the pigeonhole principle.
This conjecture remained open even for a definably complete expansion of a dense linear order. Clearly, the conjecture holds for pseudo-o-minimal. Consequently, it is connected to two other questions asked by Schoutens in [Sch14]:
Question \thequestion.
Does every definably complete type complete structure have the pigeonhole principle?
Question \thequestion.
Is there an axiomatization of pseudo-o-minimality by first-order conditions on one-variable formulae only?
To clarify the meaning of a first-order conditions on one-variable formulae only, this does not mean a first-order sentence conditioned on a specific one-variable formula, as the following example demonstrates how any first-order theory is axiomatized by such sentences, in particular .
Example \theexample.
Let be any language and be any -theory (not necessarily complete). For every sentence , let and let . Then is a first order condition on , however , so is an axiomatization of .
Clearly, this is not the intended meaning in the question. Rather, following the terminology of [Sch14], we interpret a first-order condition on one-variable formulae as first-order scheme ranging over all one-variable formulae. Rigorously, a first-order condition on one-variable formulae is obtained as follows:
- •
Let be a first-order sentence in the language where is a unary predicate.
- •
Let be the set of partitioned -formulae where is a single variable and is a finite tuple of variables not appearing in .
- •
For every , let be the -formula obtained by replacing any instance of by .
- •
.
For example, definable completeness is axiomatized in the above fashion by setting to be
[TABLE]
Namely, is the -sentence stating if is bounded, then it has a least upper bound. Following the same terminology, an axiomatization of pseudo-o-minimality by first-order conditions on one-variable formulae only is an -theory such that
[TABLE]
In [Ren14], Rennet showed that there is no recursive first-order axiomatization of pseudo-o-minimality in the language of rings . In particular, as definable completeness and type completeness are both recursive first-order schemes, given a recursive language, they cannot axiomatize pseudo-o-minimality.
In this paper, we show a stronger result (with respect to one-variable definable sets) by constructing two ordered structures on the same universe, in the same language, with the same definable subsets in one variable, where is pseudo-o-minimal and does not have the pigeonhole principle. This gives a negative answer to both Sections 1 and 1, as well as a partial answer to Section 1. Furthermore, this gives a stronger result then a negative answer to Section 1. It shows that not only is there no first order axiomatization as above, but also there is no second order theory in the language where is a unary predicate on subsets interpreted as the definable subsets. This result is strictly stronger as any axiomatization as above is equivalent to a second order theory in , but not vice-versa.
This also implies that there is no result analogous to Section 1 in the theory of definably complete type complete structures, namely there is a definably complete type complete structure and a pseudo-finite subset such that does not satisfy the common theory of definably complete type complete structures expanded by a unary predicate for a finite set.
It is still open whether we can extend this result to the case where is an expansion of a real closed field and fully answer Section 1.
Acknowledgements
The author is grateful to Phillip Hieronymi for presenting the question which motivated this paper, as well as for the fruitful discussions. The author is grateful to Assaf Hasson for the fruitful discussions and the warm support along the way. The author thanks Itay Kaplan for his helpful comments on a preliminary version of this paper and for the discussion which helped clarify and strengthen the main result.
Outline
The construction is done as follows: In Section 3, the theory is constructed as an expansion of a dense linear without endpoints by a predicate for a discrete, closed, and bounded set and some extra structure in the language such that . We then introduce an expansion and an -theory containing a function symbol which is bijective on . We show and are consistent. In Section 4 we prove quantifier elimination for .
In Section 5, we give the construction of which will be an expansion of some model of to with the same one-variable definable sets as such that does not have the pigeonhole principle. This is done by tweaking a given model of expanding so that is now injective but not surjective. It is done carefully enough, so that any definable set in differs from a set definable in by finitely many constant terms. In Section 6 we show quantifier elimination in and deduce that any definable subset of is definable in . We then define to be a trivial expansion of to and to be and show that possess the properties proclaimed in the introduction.
2. Preliminaries - cyclic orders
In this section, we present the standard definition of a cyclic order, as defined below, and present some of its properties needed for the construction following.
Definition \thedefinition.
A cyclic order on a set is a ternary relation satisfying the following axioms:
- (1)
Cyclicity: If , then . 2. (2)
Asymmetry: If , then not . 3. (3)
Transitivity: If and , then . 4. (4)
Totality: If are distinct, then either or .
The following fact is folklore (e.g., [Hun35] and [Č66, Part I, §4]) and can be easily verified:
Fact \thefact.
If is a linearly ordered set, then the relation defined by
[TABLE]
is a cyclic order on .
We call the cyclic order induced by .**
Definition \thedefinition.
Let be a linearly ordered set. A -cut in is a pair of subsets of such that and for every .
Fact \thefact ([Nov84, Lemma 3.8]).
Let be a set with two linear orders, , on . Let be a -cut in and be a -cut in . If and , then .
Definition \thedefinition.
Let be a cyclic order on a set . For any , denote
[TABLE]
Lemma \thelemma.
Let be a cyclic order on a set and let . If then
[TABLE]
Proof.
- •
To prove :
- –
By definition, .
- –
If , then together with , and transitivity, we get .
- –
If , then by cyclicity, . By cyclicity again, . Now by transitivity, , which is equivalent by cyclicity to .
- •
To prove , if
[TABLE]
then and by totality, and . By cyclicity, we get that and , which in turn, by transitivity, implies which by cyclicity is equivalent to which by asymmetry, implies that .
∎
Definition \thedefinition.
Let be a cyclic order on a set and let . Two elements are -close if either or is finite.
Denote if are -close.
Lemma \thelemma.
Let be a cyclic order on a set and let . Then is an equivalence relation on .
Proof.
- •
for all , so reflexivity holds.
- •
Symmetry is obvious by definition.
- •
To prove transitivity, let such that and . Assume towards a contradiction that and are both infinite. We may further assume, without loss of generality, that . So by cyclicity, also and . By Section 2,
[TABLE]
By Equation (2), is infinite and by Equation (3), is infinite. But by Equation (1), either or is infinite, so either or .
∎
Lemma \thelemma.
Let be a cyclic order on a set . Let and let such that
[TABLE]
Then .
Proof.
By symmetry of and cyclicity of , it suffices to show that . So assume towards a contradiction
[TABLE]
By cyclicity on (5), we get
[TABLE]
By transitivity applied to (4) and (6) we get , which in turn by cyclicity is equivalent to (7) below. By cyclicity and transitivity applied to (4) and (5), we get (8) below.
[TABLE]
By the assumption of the section, either or is finite. By Section 2 and by (7) and (8), this implies that at least one of the following is finite: , so or . Contradiction. ∎
3. Definitions of and
Definition \thedefinition.
Let where is a binary relation symbol, is a unary predicate, are function symbols and are constant symbols. Let be the -theory consisting of the following axioms:
- (1)
. 2. (2)
is a dense linear order without end points. 3. (3)
is discretely ordered, i.e., every non-maximal (respectively, non-minimal) element in has an immediate successor (respectively, predecessor) in . 4. (4)
is closed, i.e., for all , there is an interval disjoint from containing . 5. (5)
. 6. (6)
are such that and there are infinitely many elements in between any two of them. 7. (7)
is the cyclic forward projection on :
[TABLE] 8. (8)
is defined as the cyclic successor function on , and as the identity outside of :
[TABLE]
is defined as .
The consistency of will be proven together with the consistency of defined in Section 3 below.
Definition \thedefinition.
Let where are unary function symbols.
Let be together with the following axioms:
- (9)
is bijective and . 2. (10)
and is a partial order isomorphism. 3. (11)
and is a partial order isomorphisms. 4. (12)
For all and for every
[TABLE]
are infinite, i.e. .
Notice that this is a first-order scheme. 5. (13)
for every 6. (14)
for all and for every .
Proposition \theproposition.
* is consistent.*
Proof.
We prove finite satisfiability of take some sufficiently large natural number . Take with the lexicographic order and consider a structure which is a DLO containing as an ordered subset.
Let .
Let
[TABLE]
and let
Let the circular projection, as defined in Axiom 7.
Let be the circular successor function, as defined in Axiom 8 and let
Then satisfies Axioms 1, 2, 3, 5, 4, 8, 7, 9, 10, 11 and 13 by definition. As for Axioms 6, 12 and 14:
Any finite segment of Axiom 6 is contained in the following axiomatization, for a fixed :
- LABEL:axiomInfBetweenk*.
are such that and there are at least elements in between any two of them. 2. LABEL:finfk*.
For all and for every .
- (a)
There are at least elements in . 2. (b)
There are at least elements in . 3. LABEL:circularAxiomk*.
for all .
If then satisfies Axioms LABEL:axiomInfBetweenk* and LABEL:finfk*, by definition.
Under the assumption , we prove that satisfies Axiom LABEL:circularAxiomk*, thus is finitely satisfiable.
For all :
[TABLE]
So proving Axiom 14k reduces to proving that for any and one of the following holds:
- (a)
2. (b)
3. (c)
where is subtraction modulo .
If then (a) holds.
If then (b) holds.
If then (c) holds. ∎
4. Quantifier Elimination in
We now show that eliminates quantifiers:
Remark \theremark.
Let and . Then the following hold:
- (1)
** 2. (2)
** 3. (3)
** 4. (4)
** 5. (5)
** 6. (6)
** 7. (7)
** 8. (8)
** 9. (9)
**
Remark \theremark.
If then:
- (1)
. 2. (2)
* and for all .* 3. (3)
* for all , . for all , .*
If :
- (1)
. 2. (2)
* for all .* 3. (3)
* for .* 4. (4)
. 5. (5)
.
Lemma \thelemma.
For any and ,
[TABLE]
Proof.
If then and .
If then and . ∎
Proposition \theproposition.
* admits quantifier elimination.*
Proof.
Let such that are atomic and negated atomic formulas. We need to find a quantifier-free -formula such
[TABLE]
Firstly, since \vdash\exists x\big{(}\chi\left(\bar{y},x\right)\land\theta\left(\bar{y}\right)\big{)}\leftrightarrow\exists x\big{(}\chi\left(\bar{y},x\right)\big{)}\land\theta\left(\bar{y}\right) we may assume that occurs in for all . Secondly,
[TABLE]
[TABLE]
So we may assume is either of the form or of the form where are atomic and negated atomic formulas such that occurs in each . We may assume that is neither ‘’ nor ‘’ for any , as such occurrence would be either superfluous or inconsistent. So each is of the form where are terms with variables in .
By Section 4, we may assume either
[TABLE]
or
[TABLE]
where are with variables from , . By Section 4, we may assume that does not occur in any . Next, notice that are positive Boolean combinations of and if is for some we can just replace with . So we may assume , i.e. either
[TABLE]
or
[TABLE]
where are terms not containing .
If is as in (9), then by Section 4, is equivalent to
[TABLE]
If is as in (10), then since is co-dense, is equivalent to
[TABLE]
∎
5. Definition of and the relation to
Definition \thedefinition.
Let be arbitrary, with universe .
Let be the restriction of to , i.e., . Consequently, .
Let be the same -structure as with a slight modification on and , as follows.
[TABLE]
In words, there is some convex set with maximum such that the order type of is . maps to a convex subset of of order type with maximum , by Axiom 11 in Section 3.
Then are obtained from by applying a shift by one element in , respectively.
Lemma \thelemma.
* preserves the cyclic order on , i.e.*
[TABLE]
Proof.
Define a new ordering on by
[TABLE]
By Axioms 10 and 11 in Section 3, and and
[TABLE]
Additionally, by definition of , it follows that is a -cut in and is a -cut in . So by Section 2, . In conclusion
[TABLE]
∎
Lemma \thelemma.
Let be as in Section 3. Then , the closure of under composition is an Abelian group.
Proof.
By definition, , so are invertible and where is the group generated by .
Since is definable by the cyclic order on (Axiom 8 in Section 3) and preserves the cyclic order on (Section 5), it follows that . Now is Abelian, as the group defined by is Abelian. ∎
Corollary \thecorollary.
Let and .
[TABLE]
Proof.
Since , so is . Therefore, by Axiom 12,
[TABLE]
By Section 5, . ∎
Lemma \thelemma.
Let and . There are such that
[TABLE]
Proof.
By definition of (Section 5), there are such that
[TABLE]
By Section 5, the right hand side in Equation (11) is equal to
[TABLE]
and the right hand side in Equation (12) is equal to
[TABLE]
∎
Corollary \thecorollary.
For all and every :
[TABLE]
6. Quantifier elimination in
In this section, unless otherwise specified, we work inside , so is and is .
Lemma \thelemma.
* satisfies the following:*
- (1)
* and is a partial order isomorphism, and its inverse is .* 2. (2)
* and is a partial order isomorphisms, and its inverse is .* 3. (3)
* for every * 4. (4)
* is injective and not surjective on . Moreover, .* 5. (5)
* for all .* 6. (6)
* for all .* 7. (7)
For all and for every
[TABLE]
are infinite, i.e. . 8. (8)
For all and for every
[TABLE]
are infinite, i.e. .
Proof.
- •
Items 1, 2 and 3 follow by definition of and by Axioms 10, 11 and 13 in Section 3.
- •
Item 4 follows from Items 1 and 2, as
[TABLE]
- •
To prove Item 5, we separate into two cases:
- –
if for some , then , so
[TABLE]
So by definition of ,
[TABLE]
- –
if for all , then for all . So
[TABLE]
- •
To prove Item 6, by Items 4 and 3, for all , for some , therefore by Item 5
[TABLE]
- •
Item 7 follows from Axiom 12 in Section 3 and Section 5.
- •
Item 8 follows from 5 and Section 5.
∎
Corollary \thecorollary.
Let ,
- (1)
If and , then . 2. (2)
If and , then . 3. (3)
If and , then . 4. (4)
If and , then . 5. (5)
If and , then . 6. (6)
If and , then .
Proof.
and follow from Section 6, Items 1 and 6.
and follow from Section 6, Items 2 and 6.
follows from Section 6, Items 2 and 5.
follows from Section 6, Items 1 and 5. ∎
Corollary \thecorollary.
Let , .
[TABLE]
Remark \theremark.
If then . In particular,
- •
* for all .*
- •
* for all .*
- •
* for any , .*
Remark \theremark.
If then:
- •
.
- •
.
Corollary \thecorollary.
[TABLE]
Definition \thedefinition.
Following standard terminology, a constant term is a term with no free variables.
Definition \thedefinition.
Given two -definable maps , denote if there are finitely many constant terms , such that
[TABLE]
is an equivalence relation. For any -definable map , let be its equivalence class.
Lemma \thelemma.
.
Proof.
- •
If then both and are the identity on , so the equality is trivial.
- •
If and or then the equality follows by Items 1 and 2 in Section 6.
In conclusion, the equality holds for all .
∎
For any finite-to-one map , if and then . Since are injective and is injective outside , the composition is well defined, for any composition of .
Proposition \theproposition.
, the closure of under composition is an Abelian group.
Proof.
[TABLE]
So . In particular are invertible and where is the group generated by . By Section 6, . The claim now follows from the fact the group defined by is Abelian. ∎
Remark \theremark.
Let and . If there are infinitely many elements in between and , then .
By infinitely many elements in between and , we mean with respect to the order and not the cyclic order , i.e., either and , or and .
This is weaker than ; for example, but there are infinitely many elements in between and .
Lemma \thelemma.
Let . Then there are finitely many constant terms , such that if , then there are only finitely many elements in between and .
Proof.
Let where . Let , for any , so . If there are infinitely many elements in between and , then there is some with infinitely many elements in between and , so by Section 6, and thus . So if
[TABLE]
then there are finitely many elements in between and . ∎
Lemma \thelemma.
* for all and for every .*
Proof.
Let and . By Axiom 14 in Section 3,
[TABLE]
By Section 5,
[TABLE]
and the section follows from Section 2. ∎
Lemma \thelemma.
for any and :
[TABLE]
Proof.
We prove the section by induction on . For the claim holds by definition of . For , By Section 6, . So
[TABLE]
By the induction hypothesis, is equivalent to and is equivalent to . ∎
Definition \thedefinition.
- (1)
. 2. (2)
. 3. (3)
. 4. (4)
For any functions and , let .
Lemma \thelemma.
Let , , and . Then
- (1)
There are constant terms such that
[TABLE] 2. (2)
There are constant terms such that
[TABLE]
Proof.
- (1)
By Section 6 applied twice, there are constant terms such that whenever , there are finitely many elements in between and .
- •
If , then by Item 3 of Section 6, . In particular,
[TABLE]
- •
If , , then by Section 6, Item 7 there are infinitely many elements in between and . As there are only finitely many elements in between and , it follows that
[TABLE] 2. (2)
The proof is similar.
∎
Definition \thedefinition.
- (1)
We define for inductively, as follows:
- •
- •
.
- •
for all .
Notice that this is a syntactic definition, e.g., . 2. (2)
For any quantifier free -formula and variable we define by induction on the complexity of :
- •
If does not occur in , then .
- •
If is atomic of the form then .
- •
If is atomic of the form where , , and is an -term such that does not occur in , then .
- •
If is atomic of the form where , , and , then .
- •
If is a Boolean combination of atomic formulas , then is the lexicographic maximum of .
Definition \thedefinition.
A quantifier free -formula is -corrected if any term appearing in belongs to .
Lemma \thelemma.
For any quantifier free -formula and variable , there is some -corrected formula such that and .
Proof.
A Boolean combination of -corrected formulas is -corrected, so we may assume is atomic.
- •
If is of the form for some then .
- •
If is of the form for some then .
- •
If of the form for some term and :
- –
If , then by Section 6, there is some with , and constant terms such that f for all .
So
[TABLE]
- –
If , then there are such that for all and . So for all and for all . So
[TABLE]
and , so we can apply the previous case to get a formula where every term to the left of belongs to .
If does not appear in we are done. Otherwise, if for some term , a symmetric argument applied to will an -corrected formula equivalent to as needed.
∎
Lemma \thelemma.
- (1)
Let be an -corrected atomic formula of rank or of rank for some . Then there is some quantifier free formula such that and .
Proof.
- (1)
Assume .
If is of the form where , by Section 6, and .
If is of the form where , , and is some -term not containing
In which case, and
[TABLE]
- (a)
Applying Section 6 to , there is some -corrected formula of rank such that for all . So
[TABLE] 2. (b)
Applying Section 6 to and , we obtain that
[TABLE]
is equivalent to one of the following:
[TABLE]
As in (1)a, there are and of rank equivalent to and , respectively. So (13) is equivalent to one of the following:
[TABLE]
an each is -corrected of rank .
By Section 6, is equivalent to
[TABLE]
and the latter is an -corrected formula of rank . 2. (2)
Assume . Then is of the form where , and . Replace with on the left of to get . Apply Item (1) of this section to and get some quantifier-free formula with . Replacing back, we get for any and
[TABLE]
∎
Lemma \thelemma.
Let be an -corrected atomic formula of rank for some . Then there is some quantifier free formula such that and .
Proof.
By Section 6, we may assume is either of the form or of the form for some .
- (1)
In case is , by Section 6,
[TABLE]
and the formula in (21) is of rank . 2. (2)
In case is , by Section 6, there are finitely many constant terms such that for all . So
[TABLE]
and
Now, replacing with in (20), we get
[TABLE]
By noticing that , the formula in (23) is of rank .
∎
Lemma \thelemma.
Let be an -corrected atomic formula of rank . Then there is some quantifier free formula such that and .
Proof.
By Sections 4 and 4 we may assume is of the form where and . Now
[TABLE]
By Section 4, the right hand side is equivalent to a quantifier free formula of rank . ∎
Lemma \thelemma.
Let be a quantifier free formula with free variable . Then there is some -corrected formula such that for some and .
Proof.
By Section 6 we may assume is -corrected. Since the lexicographic order on well-ordered sets is well-ordered, by induction it suffices to show that if , then there is some -corrected such that and . As a Boolean combination of formulas of rank at most is of rank at most as well, we may further assume that is atomic.
- •
If for some , then by Section 6 there is some quantifier free formula such that .
- •
If for some , then by Section 6 there is some quantifier free formula such that .
- •
If for some , then by Section 6 there is some quantifier free formula such that .
- •
If for some , then by Section 6 there is some quantifier free formula such that .
So in conclusion, whenever is -corrected and , there is some quantifier free formula such that and . By Section 6, there is some -corrected formula such that and . ∎
Theorem 6.1**.**
* admits quantifier elimination.*
Proof.
Let be a quantifier free -formula. It suffices to find a quantifier free formula such that . By Section 6, we may assume is -corrected and . Since , there is some quantifier-free -formula and -terms with variables in such that
[TABLE]
Now by Section 4, there is some quantifier-free formula such that
[TABLE]
As , in conclusion,
[TABLE]
and is a quantifier-free -formula with variables from . ∎
Corollary \thecorollary.
Every one-variable set definable in is definable in .
Proof.
By Theorem 6.1, every definable set in is quantifier-free definable. By Section 6, every quantifier-free one-variable set definable in is equivalent to an -corrected formula of rank , which in turn is definable (with parameters) in . ∎
We conclude by articulating the answers to Questions 1 and 1.
Theorem 6.2**.**
There is a definably complete type complete structure without the pigeonhole property.
Proof.
The failure of the pigeonhole principle in is witnessed by and . But by Section 6, and have the same definable sets in one free variable. In particular, is definably complete and type complete. ∎
Theorem 6.3**.**
There are two ordered structures in the same language on the same universe, admitting the same order and the same definable subsets with being pseudo-o-minimal and not.
In particular, the answer to Section 1 is negative and there is no axiomatization of pseudo-o-minimality by first-order conditions on one-variable formulae only. Furthermore, there is no axiomatization of pseudo-o-minimality by any second order theory in the language where is interpreted as the definable one-variable subsets.
Proof.
is pseudo-o-minimal and is not pseudo-o-minimal as the failure of the pigeonhole principle is witnessed by and . But and by Section 6, and have the same definable sets in one free variable. We may now define to be and to be a trivial expansion of to (letting every function symbol be interpreted as the identity map and any relation symbol be interpreted as the ).
∎
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[FH 15] Antongiulio Fornasiero and Philipp Hieronymi. A fundamental dichotomy for definably complete expansions of ordered fields. J. Symb. Log. , 80(4):1091–1115, 2015.
- 2[For 10] Antongiulio Fornasiero. Tame structures and open cores. ar Xiv e-prints , page ar Xiv:1003.3557, Mar 2010.
- 3[For 13] Antongiulio Fornasiero. Locally o-minimal structures and structures with locally o-minimal open core. Ann. Pure Appl. Logic , 164(3):211–229, 2013.
- 4[FS 11] Antongiulio Fornasiero and Tamara Servi. Relative Pfaffian closure for definably complete Baire structures. Illinois J. Math. , 55(3):1203–1219 (2013), 2011.
- 5[Hie 11] Philipp Hieronymi. Expansions of subfields of the real field by a discrete set. Fund. Math. , 215(2):167–175, 2011.
- 6[Hie 13] Philipp Hieronymi. An analogue of the Baire category theorem. J. Symbolic Logic , 78(1):207–213, 2013.
- 7[Hun 35] Edward V. Huntington. Inter-relations among the four principal types of order. Trans. Amer. Math. Soc. , 38(1):1–9, 1935.
- 8[Mil 01] Chris Miller. Expansions of dense linear orders with the intermediate value property. J. Symbolic Logic , 66(4):1783–1790, 2001.
