Интерпретации в слабых арифметических теориях тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Запрягаев Александр Александрович

• Запрягаев Александр Александрович
• кандидат наук
• 2023

Оглавление диссертации кандидат наук Запрягаев Александр Александрович

Contents

Introduction

0.1 Arithmetical theories

0.2 Interpretations

0.3 Reflexive theories and Visser's conjecture

0.4 Main Results of the Dissertation

0.5 Linear orders interpretable in PrA

0.6 Interpretations in PrA

0.7 Interpretations in BAn

0.8 Structure of the thesis

1 Interpretations

2 Linear Orders in PrA

2.1 Preliminaries on PrA

2.2 Presburger dimension

2.3 Ranks of linear orders

3 Interpretations in PrA

3.1 The one-dimensional case

3.2 The multi-dimensional case

4 Interpretations in BAn

4.1 Finite automata

4.2 The equivalence

4.3 Interpretations

4.4 Non-standard models of BAn

4.5 Proof of the main theorem

5 Conclusion 85 Publications 88 Conference Abstracts 89 References

Введение диссертации (часть автореферата) на тему «Интерпретации в слабых арифметических теориях»

Introduction

0.1 Arithmetical theories

This dissertation is devoted to the study of weak arithmetical theories and the problem posed by Albert Visser about interpretations of such arithmetical theories in themselves.

An arithmetical theory is a first order theory that has the natural numbers N with some operations on them as a model. According to Godel's first incompleteness theorem, Peano arithmetic PA, which contains both addition and multiplication in its language, is incomplete and undecidable. Hence, there is an interest in studying first order arithmetic theories in less expressive languages, for which completeness and decidability can be proven. These theories are called weak arithmetics. They include Presburger arithmetic (the theory of addition only), Skolem arithmetic (theory of multiplication only), as well as Biichi arithmetics,

a family of decidable extensions of Presburger arithmetic.

Presburger arithmetic (PrA) [7; 8] is the elementary theory of natural numbers with addition Th(N; =, +). It is complete by definition and is shown to be decidable. As proven by Presburger [7], in the language extended by congruence modulo n relations =n for all n > 2 Presburger arithmetic admits quantifier elimination.

PrA possesses an equivalent axiomatic definition, as the first order theory with equality given by the following recursive set of axioms [9, Appendix]:

1. x < y ^ 3z (x + (z + 1) = y)

2. x =n y ^ 3u (x = nu + y V y = nu + x)

3. x = 0 ^ Vy (x + y = x)

4. x = 1 ^ 0 < x A -3z (0 < z A z < x)

5. -(x + 1 = 0)

6. x + z = y + z ^ x = y

7. x + 0 = x

8. (x + y) + z = x + (y + z)

9. x = 0 V 3y (x = y + 1)

10. x + y = y + x

11. x < y V x = y V y < x

12. (x =n 0) V (x =n 1) V ... V (x =n n — 1) (for each n > 2)

Here n abbreviates 1 + ... + 1 n times.

PrA is not finitely axiomatizable [10, Theorem 1.2.4]. The quantifier elimination algorithm of Presburger arithmetic [11] can be performed in triply exponential time [12]. An N2-EXPTIME lower bound for the derivation problem complexity in Presburger arithmetic is established in [13]. The memory upper bound is 2-EXPSPACE [14]. The existential fragment of PrA is NP-complete [15].

A Buchi arithmetic BAn, n > 2, is the theory Th(N; =, +, Vn) where Vn is an additional unary functional symbol such that Vn(x) is the largest power of n that divides x. By convention, we put Vn(0) = 0.

These theories were proposed by J. Biichi [16] in order to describe the sets of natural numbers recognizable by finite automata through definability in some arithmetical language.

Let Digitn(x,y) be the digit corresponding to ny in the n-ary expansion of x. We consider automata over the alphabet {0,..., n — 1}m.

Assume that at step k-the automaton receives the input

(Digitn(xi, k),..., Digitn(xm, k)),

containing the digits corresponding to nk in the n-ary expansion of (x1,..., xm). We say the automaton accepts the tuple (x1,..., xm) if it accepts the corresponding sequence of tuples

(Digitn(x1, k),..., Digitn(xm, k))

where k ranges from 0 to the largest value such that the tuple is non-zero.

Then the following well-known result by V. Bruyere ([17],[18], Theorem 4.1) holds:

Statement 0.1.1. Let ^(x1,... ,xm) be a BAn-formula. Then there is an effectively constructed automaton A such that (a1,... , am) is accepted by A iff N |= ... ,am).

Contrariwise, let A be a finite automaton working on m-tuples of n-ary natural numbers. Then there is an effectively constructed BAn-formula ^(x1,..., xm) such that N == ..., am) iff (a1,..., am) is accepted by A.

Numbers n, m > 2 are called multiplicatively independent if the equation nk = m1 has no integer solutions beside k = l = 0. Cobham-Semenov theorem [19; 20] states that for multiplicatively independent

natural numbers n,m, any set definable simultaneously in BAn and BAm is actually definable in Presburger arithmetic PrA.

0.2 Interpretations

Let K, L be two first order languages. A non-parametric m-dimensional interpretation [21] from K to L (detailed definitions follow in Chapter 1) is formed by a syntactic translation i of the formulas of K into formulas of L with quantifiers relativized to a given L-formula Db (the domain formula).

Naturally, as long as we fix some model B of L such that the set {y | Dt(y)} is not empty and the translation =l of equality in K is a congruence, i defines a K-structure Bl with the support {x G Bm | D, (x)}/=1. Bl is called the internal model of i in B. Such i are called interpretations of a model Bl in a model B.

Given two theories, T in K and U in L, i is called an interpretation of T in U if the translation sends theorems of T into theorems of U. In other words, for each model B of U it holds that the internal model Bl is a model of T.

We say that an interpretation from T to U is unrelativized if the domain formula is trivial; it has absolute equality if = is interpreted as

the identity of tuples.

Interpretations naturally occur in many branches of mathematics. A classical example is the two-dimensional interpretation of the elementary plane geometry in the field of real numbers. Similarly, there is a two-dimensional interpretation of the field C in R obtained by defining a + bi ^ (a, b) and introducing addition and multiplication.

We call an m1-dimensional interpretation ¿1 and m2-dimensional interpretation ¿2 from T to U provably isomorphic, if in the language of U there is a formula F(x,y) expressing an isomorphism f between the corresponding internal models B11 and B12. Furthermore, the statement that f is an isomorphism must be provable in U.

In the dissertation, the interpretations in weak arithmetical theories are studied up to a provable isomorphism. We note that two interpretations into the elementary theory of a model B are provably isomorphic iff there is an L-definable isomorphism between their internal models in B. As PrA and BAn are the elementary theories of the models (N; =, +) and (N; =, +, Vn) respectively, when considering interpretations in them it suffices to study the interpretations in these models.

0.3 Reflexive theories and Visser's conjecture

A first order theory sufficiently strong to formalize consistency statements is called reflexive if it can prove the consistency of all its finitely axiomatizable subtheories. Well-known examples of reflexive theories include Peano arithmetic PA and Zermelo-Fraenkel set theory ZF.

Definition 1. Let Adjunctive set theory AS be the theory in the language {=, g} containing the following two axioms:

1. ElxVy (y G x) (existence of the empty set);

2. VxVy 3z Vu (u G z ^ (u G x V u = y)) (each set can be extended by any single object).

Definition 2. A theory T is called sequential [22, p. 402] if there is a one-dimensional, unrelativized interpretation with absolute equality of AS into T.

It is known that sequential theories (a broad and natural general class of theories) are able to encode tuples of objects of arbitrary finite length by a single object. All sequential theories that prove all instances of the induction scheme in their language are reflexive [23, p. 193]. Each theory

A that is both sequential and reflexive possesses the following property: A cannot be interpreted in any of its finite subtheories (*). Albert Visser has proposed to consider the interpretational-theoretic property (*) as a generalization of reflexivity for weaker theories that are unable to formalize syntax in their own language.

In particular, he conjectured that (*) holds for Presburger arithmetic. PrA satisfies full induction scheme in its own language but cannot formalize the consistency statement. Furthermore, Presburger arithmetic is not sequential, that is, cannot encode tuples of natural numbers by a single natural number. Hence, in the case of PrA it is important whether individual objects are interpreted by individual objects or by tuples of objects of length m.

Another related property can be stated: each interpretation of A in itself is provably isomorphic to the trivial one (**). The connection between (*) and (**) is given by the following statement:

Theorem 0.3.1 ([10, Theorem 2.3.3]). Let U be a theory with property (**) which is not finitely axiomatizable. Then U has property (*).

This motivates study of interpretations of weak arithmetical theories in themselves. Indeed, it is known that PrA is not finitely axiomatizable. If we show each interpretation of PrA in itself is provably isomorphic to the trivial one, then property (*), the weak analogue of reflexivity, holds

for PrA, hence, despite its limitations in syntax, it exhibits some of the properties pertaining to strong theories akin to PA.

A natural example of a weak arithmetical theory for which (**) does not hold is the theory Th(Z; =, S(x)) of integer numbers with successor (y = S(x) ^ y = x + 1). Indeed, consider the translation of y = S(x) as y = S(S(x)) and the trivial domain formula. The corresponding internal model is formed by two separate copies of Z. The fact that this is an interpretation of Th(Z;=,S(x)) is given by the following easy lemma. It is well-known, we give a proof for the sake of completeness.

Lemma 0.3.1. Structures (Z; =, S(x)) and (Z; =, S(S(x))) are elementarily equivalent.

Proof. We will show that the following set of first order formulas axiom-atizes Th(Z;=,S(x)):

1. VxVy (Sx = Sy ^ x = y);

2. Vy3x (Sx = y);

3. Vx (Snx = x), for all n = 1, 2,...

If this is established, the claim directly follows, as all of these axioms hold in (Z;=,S(S(x))).

It is clear that the theory T defined by all of the axioms above holds in (Z;=,S(x)). The axioms 1 and 2 state that the functional relation S(x) is, furthermore, injective (axiom 1) and surjective (axiom 2). The series of axioms 3 claims that S is not reflexive and, more generally, allows no cycles. Hence, given x, the elements in the sequence ..., S-1(S-1(x)), S-1(x), x, S(x), S(S(x)),... are all distinct. This means that any model of T separates into a number of isolated chains, each of them isomorphic to Z.

Thus, the models of T are distinguished by the cardinality of the set of their Z-chains. In particular, for each fixed uncountable cardinality, as the cardinality of the set of chains would equal the cardinality of the model itself, there is only one model of that cardinality up to an isomorphism. By applying Los-Vaught test, we establish the completeness of T. As it is a subtheory of a complete theory Th(Z;=,S(x)), it must coincide with Th(Z; =, S(x)), which concludes the proof.

□

The interpretations in PrA were previously studied by J. Zoethout [10], who established Theorem 0.3.1 and proved that a one-dimensional interpretation of PrA in (N;=, +) is always isomorphic to the trivial one (without the condition of definability).

0.4 Main Results of the Dissertation

In this dissertation, the following result in proven on one-dimensional and multi-dimensional interpretations of PrA:

Theorem 0.4.1. 1. Let i be a (one- or multi-dimensional) interpretation of PrA in (N; =, +). Then the internal model induced by i is isomorphic to the standard one.

2. This isomorphism can always be expressed by a PrA-formula.

In other words, property (**) is established for Presburger arithmetic. We note that statement 1 of the theorem in one-dimensional case was shown by J. Zoethout [10]; the same statement for multi-dimensional interpretations and statement 2 of the theorem were established by the author jointly with F. Pakhomov [1; 2].

For Biichi arithmetics, it is shown that each interpretation of BAn in itself is isomorphic to the trivial one [3] (whether it is always definable remains a problem for future research):

Theorem 0.4.2. Let i be an interpretation of PrA in the standard model N of BAn. Then the internal model induced by i is isomorphic to the standard one.

0.5 Linear orders interpretable in PrA

In order to show that all interpretations of PrA into itself (that is to say, into its own standard model (N; =, +), as PrA is the elementary theory of this structure) are provably isomorphic to the trivial one, it is necessary to show:

1. this isomorphism exists;

2. it is always definable by a PrA-formula.

The first statement means that the internal model for each interpretation of PrA in N is standard. The order types of non-standard models of PrA and BAn follow the classic result of Kemeny [24], which holds also for PA:

Theorem 0.5.1. Any non-standard model A of PrA (or BAn) has the order type N + Z • A, where (A, <a) is some dense linear order without endpoints.

In particular, each countable non-standard model of PrA has the order type isomorphic to N + Z • Q.

For PA, Tennenbaum's theorem [25] states:

Statement 0.5.1. A countable non-standard model PA cannot be recursive.

However, PrA allows explicit recursive examples of non-standard models.

Theorem 0.5.1 implies that if an interpretation of PrA in N has a non-standard internal model, its order type must be necessarily isomorphic to N + Z • Q.

In order to show the impossibility of that, we introduce the following notion. Consider the condensation operation which identifies the points with a finite distance between each other. For a linear order (L, <), its VD*-rank [26] rk(L, <) G Ord U {to} is the least ordinal a such that after a iterations of condensation the resulting order is finite, and to, taken to be larger than all ordinals, if no such a exists.

It is known that the scattered linear orders, that is, those not containing Q as a suborder, are exactly those with rank less than to.

In the dissertation, the following necessary condition is established:

Theorem 0.5.2. All linear orders m-dimensionally interpretable in the model (N; =, +) for m > 1 have rank m or below.

Hence, as N + Z • Q is not scattered, a non-standard model of PrA cannot be interpreted in N.

0.6 Interpretations in Presburger Arithmetic

In order to show that an isomorphism between the internal model and the external structure (N; =, +) is always definable, we study the structure of sets definable in Presburger arithmetic.

Definition 3. For vectors c,p1,... ,pn £ Zm we call the set {ch^ | hi £ N} a lattice (or a linear set) with generating vectors {pi}. If {pi} are linearly independent, we call the set a fundamental lattice.

The combination of classical results by Ginsburg and Spanier [27] and Ito [28] gives

Lemma 0.6.1. All subsets of Zk definable in (N;=, +) are exactly the disjoint unions of finitely many fundamental lattices.

Definition 4. Let A C Zn be a definable set. We call a function f: A ^ N piecewise polynomial if there is a decomposition of A into finitely many fundamental lattices J1,..., Jk that the restriction of f on each Ji is a rational polynomial.

The main technical instrument is provided by the following

Theorem 0.6.1. Suppose M is a m x n matrix of integer numbers. Let the function ^m : Zm ^ N U {H0} be defined as follows:

(u) = |{a g Nn | Ma = u}|.

Let, furthermore, the values of be always finite for all tuples U. Then is a piecewise polynomial function < n — rk(M).

From here, we derive Theorem 0.4.1.

0.7 Interpretations in Büchi Arithmetics

We note that if BAn (or even PrA) is interpreted in BAn by an interpretation ¿, it can be extended to an interpretation of an ordered abelian group such that the internal model of the original theory will correspond to the non-negative numbers.

By Statement 0.1.1, for algebraic structure is interpretable in BAn iff it has an automatic [29] presentation. We make use of a necessary condition for automatic abelian groups established by Braun and Strüngmann:

Theorem 0.7.1 ([30]). Let (A, +) be an automatic torsion-free abelian group. Then there exists a subgroup B of A isomorphic to Zm for some natural m such that the quotient C = A/B is a torsion group, and

the orders of the elements in C are only divisible by a finite number of different primes p1,... ,ps.

In order to prove Theorem 0.4.2 we argue as follows. Assume that there is an interpretation of BAn in N with a non-standard internal model. Let B be the extension of this internal model to an abelian group (with the order type Z • Q). It can be shown:

Lemma 0.7.1. Let Z be the subgroup of B containing the standard integer numbers. Then B/Z contains a subgroup Q isomorphic to (Q, +).

From here, we derive contradiction with Theorem 0.7.1.

0.8 Structure of the thesis