1 Introduction and Preliminaries
Entscheidungsproblem, one of the fundamental problems of (mathematical) logic, asks for a singleinput Booleanoutput algorithm that takes a formula as input and outputs ‘yes’ if is logically valid and outputs ‘no’ otherwise. Now, we know that this problem is not (computably) solvable. One reason for this is the existence of an essentially undecidable and finitely axiomatizable theory, see e.g. visser ; for another proof see (bbj, , Theorem 11.2). However, by Gödel’s completeness theorem, the set of logically valid formulas is computably enumerable, i.e., there exists an inputfree algorithms that (after running) lists all the valid formulas (and nothing else). For the structures, since their theories are complete, the story is different: the theory of a structure is either decidable or that structure is not axiomatizable (by any computably enumerable set of sentences; see e.g. (enderton, , Corollaries 25G and 26I) or (monk, , Theorem 15.2)). For example, the additive theory of natural numbers was shown to be decidable by Presburger in 1929 (and by Skolem in 1930; see smorynski ). The multiplicative theory of the natural numbers was announced to be decidable by Skolem in 1930. Then it was expected that the theory of addition and multiplication of natural numbers would be decidable too; confirming Hilbert’s Program. But the world was shocked in 1931 by Gödel’s incompleteness theorem which implies that the theory of is undecidable (see the subsection 4.1 below). In this paper we study the theories of the sets , , and in the languages , and ; see the table below.
Thm. 2.3  Thm. 2.2  Thm. 2.1  Thm. 2.1  
Rem. 4  Thm. 3.2  Thm. 3.1  Thm. 3.1  
4.1  4.2  Thm. 4.2  Thm. 4.1  
4.1  4.2  4.4  4.3 
Let us note that order is definable in the language in these sets: in by , and in by Lagrange’s four square theorem is equivalent with The four square theorem holds in too: for any we have so for some integers ; therefore, holds. Thus, the same formula defines the order () in as well. Finally, in the relation is equivalent with the formula .
The decidability of in the languages and is already known. It is also known that the theories of and in the language are undecidable. The theory of in the language is decidable too by Tarski’s theorem (which states the decidability of the theory of ). Here, we prove this directly by presenting an explicit axiomatization. Finally, the structure is studied in this paper (seemingly, for the first time). We show, by the method of quantifier elimination, that the theory of this structure is decidable. Here, the (super)structure is not usable since it is undecidable (proved by Robinson robinson ; see also (smorynski, , Theorem 8.30)). On the other hand its (sub)structure is decidable (proved in mostowski by Mostowski; see also salehim ). So, the three structures and and are different from each other; the order relation is not definable in and the addition operation is not definable in (by our results). This paper is a continuation of the conference paper salehimo .
2 The Ordered Structure of Numbers
Definition 1 (Ordered Structure)
An ordered structure is a triple where is a nonempty set and is a binary relation on which satisfies the following axioms:
() , 
() and 
() ; 
and is a language.
Here could be empty, or any language, for example or or .
Definition 2 (Various Types of Orders)
A linear order relation is called dense if it satisfies
() . 
An order relation is called without endpoints if it satisfies
() and 
() . 
A discrete order has the property that any element has an immediate successor (i.e., there is no other element in between them). If the successor of is denoted by then a discrete order satisfies
() . 
The successor of an integer is .
Remark 1 (The Main Lemma of Quantifier Elimination)
It is known that a theory (or a structure) admits quantifier elimination if and only if every formula of the form is equivalent with a quantifierfree formula, where each is either an atomic formula or the negation of an atomic formula. This has been proved in e.g. (enderton, , Theorem 31F), (hinman, , Lemma 2.4.30), (kk, , Theorem 1, Chapter 4), (marker, , Lemma 3.1.5) and (smorynski, , Lemma 4.1). In the presence of a linear order relation () by the equivalences and , which follow from the axioms (of Definition 1), we do not need to consider the negated atomic formulas (when there is no relation symbol in the language other than ).
Convention:
Let denote the (propositional constant of) contradiction, and the truth. By convention, abbreviates . The symbols and are used interchangeably throughout the paper. For convenience, let us agree that as this does not contradict our intuition. Needless to say, symbolizes (times); also (times) is abbreviated as .
The following theorem has been proved in (marker, , Theorems 2.4.1 and 3.1.3). Here, we present a syntactic (prooftheoretic) proof.
Theorem 2.1 (Axiomatizablity of and )
The theory axiomatized by the finite set (i.e., the theory of dense linear orders without endpoints, see Definitions 1 and 2) completely axiomatizes the order theory of the real and rational numbers and, moreover, the structure (and also ) admits quantifier elimination, and so its theory is decidable.
Proof
All the atomic formulas are either of the form or for some variables and . If both of the variables are equal then is equivalent with by and is equivalent with . So, by Remark 1, it suffices to eliminate the quantifier of the formulas of the form
(1) 
where ’s, ’s and ’s are variables. Now, if then the formula (1) is equivalent with the quantifierfree formula
So, let us suppose that . Then if or the formula (1) is equivalent with the quantifierfree formula , by the axioms and (with and ) respectively, and if it is equivalent with the quantifierfree formula by the axiom (with and ).
In fact for any set such that the structure can be completely axiomatized by the finite set of axioms in Definitions 1 and 2.
The theory of the structure does not admit quantifier elimination: for example the formula is not equivalent with any quantifierfree formula in the language (note that it is not equivalent with ). If we add the successor operation to the language then that formula will be equivalent with and the process of quantifier elimination will go through.
Theorem 2.2 (Axiomatizablity of )
The finite theory of discrete linear orders without endpoints, consisting of the axioms , , , plus
() 
completely axiomatizes the order theory of the integer numbers and, moreover, the structure admits quantifier elimination, and so its theory is decidable.
Proof
We note that all the terms in the language are of the form for some variable and . So, all the atomic formulas are either of the form or for some variables . If a variable appears in the both sides of an atomic formula, then we have either or . The formula is equivalent with when and with otherwise; also is equivalent with when and with otherwise. So, it suffices to consider the atomic formulas of the form or or for some free term and . Now, by Remark 1, we eliminate the quantifier of the formulas
(2) 
The axioms prove and ; so we can assume that ’s and ’s and ’s in the formula (2) are equal to each other, say to . Then by the formula (2) is equivalent with
(3) 
for some (possibly new) terms (and ). Now, if then the formula (3) is equivalent with the quantifierfree formula
Let us then assume that . The formula
(4) 
is equivalent with the quantifierfree formula by the axiom (in Definition 2).
The structure can also be finitely axiomatized. The following theorem has been proved in (enderton, , Theorem 32A) so we do not present its proof here.
Theorem 2.3 (Axiomatizablity of )
The finite theory consisting of the axioms (in Definitions 1 and 2) and also the following two axioms
() , 
() , 
completely axiomatizes the order theory of the natural numbers and, moreover, the structure admits quantifier elimination, and so its theory is decidable.
Let us note that the structure does not admit quantifier elimination, since e.g. the formula is not equivalent with any quantifierfree formula in the language . However, this formula is equivalent with .
3 The Additive Ordered Structures of Numbers
Here we study the structures of the sets over the language .
Definition 3 (Some Group Theory)
A group is a structure where is a binary operation on , is a constant (a special element of ) and is a unary operation on which satisfy the following axioms:
; 
; 
. 
It is called an abelian group when it also satisfies
. 
A group is called nontrivial when
; 
and it is called divisible when for we have
where .
An ordered group is a group equipped with an order relation (which satisfies ) such that also the axiom
is satisfied in it.
The following has been proved in e.g. (marker, , Corollary 3.1.17):
Theorem 3.1 (Axiomatizablity of and )
The following infinite theory (of nontrivial ordered divisible abelian groups) completely axiomatizes the order and additive theory of the real and rational numbers and, moreover, the structure (and also ) admits quantifier elimination, and so its theory is decidable.
() 
() 
() 
() 
() 
() 
() 
() 
() 
() 
Proof
Firstly, let us note that , and can be proved from the presented axioms: if then by there exists some such that ; one can easily show that holds. Thus is proved; for note that for any we have by . A dual argument can prove the axiom . Also, the equivalences

and

can be proved from the axioms: (i) follows from (with ) and (ii) follows from which is derived from (with ).
Secondly, every term containing is equal to for some free term and . So, every atomic formula containing is equivalent with where . Whence, by Remark 1, it suffices to prove the equivalence of the formula
(5) 
with a quantifierfree formula. By the equivalences (i) and (ii) above we can assume that ’s and ’s and ’s in the formula (5) are equal to each other, say to . Then by the formula (5) is equivalent with
(6) 
for some (possibly new) terms (and ). Now, the quantifier of this formula can be eliminated just like the way that the quantifier of the formula (1) was eliminated in the proof of Theorem 2.1.
Remark 2 (Infinite Axiomatizablity)
To see that and are not finitely axiomatizable, it suffices to note that for a given natural number , the set of rational numbers, where , is closed under addition and so satisfies the axioms , , , , , , , , and the finite number of the instances of the axiom (for ) but does not satisfy the instance of for where is a prime number larger than .
For eliminating the quantifiers of the formulas of the structure we add the (binary) congruence relations (modulo standard natural numbers) to the language; let us note that is equivalent with . About these congruence relations the following Generalized Chinese Remainder Theorem will be useful later; below we present a proof of this theorem from frankel .
Proposition 1 (Generalized Chinese Remainder)
For integers and there exists some such that for if and only if holds for each , where is the greatest common divisor of and .
Proof
The ‘only if’ part is easy. We prove the ‘if’ part by induction on . For there is nothing to prove, and for we note that by Bézout’s Identity there are such that . Also, by the assumption there exists some such that . Now, if we take to be then we have and so and hold. For the induction step () suppose that holds for (and that holds for each ). Let be the least common multiplier of ; then the greatest common divisor of and is the least common multiplier of . Now holds for and so by the assumption we have (for ). Therefore, and so for some . By Bézout’s Identity there are such that . Now, for we have and also holds for each . This proves the desired conclusion.
The following theorem has been proved, in various formats, in e.g. (bbj, , Chapter 24), (enderton, , Theorem 32E), (hinman, , Corollary 2.5.18), (kk, , Secion III, Chapter 4), (marker, , Corollary 3.1.21), (monk, , Theorem 13.10) and (smorynski, , Section 4, Chapter III). Here, we present a slightly different proof.
Theorem 3.2 (Axiomatizablity of )
The infinite theory of nontrivial discretely ordered abelian groups with the division algorithm, that is , , , , , , , and
() 
() 
where (times) 
completely axiomatizes the order and additive theory of the integer numbers and, moreover, the (theory of the) structure admits quantifier elimination, so has a decidable theory.
Proof
The axiom is equivalent with and so the negation signs behind the congruences can be eliminated by the following equivalence: . Whence, by Remark 1, it suffices to show the equivalence of the formula
(7) 
with some quantifierfree formula, where ’s, ’s, ’s and ’s are natural numbers and ’s, ’s, ’s and ’s are free terms. By the equivalences

,

and

which are provable from the axioms, we can assume that ’s, ’s, ’s and ’s in the formula (7) are equal to each other, say to . Now, (7) is equivalent with
(8) 
for and some (possibly new) terms ’s, ’s, ’s and ’s. If then (8) is readily equivalent with the quantifierfree formula which results from substituting with . So, it suffices to eliminate the quantifier of
(9) 
By the equivalence of the formula with the following formula we can assume that (and by a dual argument). Also, is equivalent with where is the greatest common divisor of and , is their least common multiplier, and where satisfy Bézout’s Identity (see the proof of Proposition 1). So, we can assume that as well. Now, if then the formula (9) is equivalent with a quantifierfree formula by Theorem 2.2 (with just like the the way formula (4) was equivalent with some quantifierfree formula). So, suppose that . In this case, if any of or is equal to then (9) is equivalent with (since any congruence can have infinitely large or infinitely small solutions). Finally, if then the formula is equivalent with for , and . Now, is equivalent with the quantifierfree formula since by the division algorithm there are some and some such that . The existence of some such that is then equivalent with ().
Remark 3 (Infinite Axiomatizablity)
The theory of the structure cannot be axiomatized finitely, because , , , , , , , , and any finite number of the instances of cannot prove all the instances of . To see this take to be a sufficiently large prime number and put . Let us recall that the set of rational numbers is closed under addition and the operation for any . Let and define the structure by the following:

;

;

;

;

.
It is straightforward to see that satisfies the axioms , , , , , , , and ; but does not satisfy for since we have for any element (with ) implies that but . However, satisfies the finite number of the instances of (for any ): for any we have for some , , and for some with ; now, (where ) and so (where for times).
Remark 4 ()
Since is definable in the structure by , we do not study separately (see (enderton, , Theorem 32E)). In fact the decidability of implies the decidability of : relativization of a formula resulted from substituting any subformula of the form by and by has the following property: .
4 The Multiplicative Ordered Structures of Numbers
In this final section we consider the theories of the number sets and in the language .
4.1 Natural Numbers with Order and Multiplication
The theory of the structure is not decidable (and so no computably enumerable set of sentences can axiomatize this structure). This is because:

The addition operation is definable in , since

the successor operation is definable from order:

and the addition operation is definable from the successor and multiplication:
This identity was first introduced by Robinson robinson ; also see e.g. (bbj, , Chapter 24) or (enderton, , Exercise 2 on page 281).


Thus the structure can interpret the structure whose theory is undecidable (see e.g. (bbj, , Theorem 17.4), (enderton, , Corollary 35A), (hinman, , Theorem 4.1.7), (monk, , Chapter 15) or (smorynski, , Corollary 6.4 in Chapter III)).
4.2 Integer Numbers with Order and Multiplication
The undecidability of the theory of the structure also implies the undecidability of the theories of the structures and as follows:

By Lagrange’s Four Square Theorem (see e.g. (monk, , Theorem 16.6)) is definable in , and so has an undecidable theory (see e.g. (monk, , Theorem 16.7) or (smorynski, , Corollary 8.29 in Chapter III)).

The following numbers and operations are definable in the structure :

The number zero: .

The number one: .

The number 1: .

The additive inverse: .

The successor: .

The addition:
.
There is another beautiful definition for in terms of and in at (hinman, , p. 187):
.


Whence, the structure can interpret the undecidable structure .
4.3 Real Numbers with Order and Multiplication
The structure is decidable, since by a theorem of Tarski the (theory of the) structure can be completely axiomatized by the theory of real closed ordered fields, and so has a decidable theory; see e.g. (kk, , Theorem 7, Chapter 4), (marker, , Theorem 3.3.15) or (monk, , Theorem 21.36). Here, we prove the decidability of the theory of directly (without using Tarski’s theorem) and provide an explicit axiomatization for it. Before that let us make a little note about the theory (of the positive real numbers) which is isomorphic to by the mapping . Thus, we have the following immediate corollary of Theorem 3.1:
Proposition 2 (Axiomatizablity of )
The following infinite theory (of nontrivial ordered divisible abelian groups) completely axiomatizes the order and multiplicative theory of the positive real numbers and, moreover, admits quantifier elimination, and so its theory is decidable.
() 
() 
() 
() 
() 
() 
() 
() 
() 
() 
Proof
For the infinite axiomatizability it suffices to note that for a sufficiently large the set of positive real numbers (cf. Remark 2) satisfies all the axioms (, , , , , , , , ) and finitely many instances of the axiom (for ) but not all the instances of (for example when is a prime larger than ).
Theorem 4.1 (Axiomatizablity of )
The following infinite theory completely axiomatizes the order and multiplicative theory of the real numbers and, moreover, the structure admits quantifier elimination, and so its theory is decidable.
( 
Comments
There are no comments yet.