Presburger's essay on the completeness and decidability of arithmetic with integer addition but without multiplication is a milestone in the history of mathematical logic and formal metatheory. The proof is constructive, using Tarski-style quantifier elimination and a four-part recursive comprehension principle for axiomatic consequence characterization. Presburger's proof for the completeness of first order arithmetic with identity and addition but without multiplication, in light of the restrictive formal metatheorems of Gödel, Church, and Rosser, takes the foundations of arithmetic in (...) mathematical logic to the limits of completeness and decidability. (shrink)

The life and work of Moj?esz Presburger (1904?1943?) are summarised in this article. Although his production in logic was small, it had considerable impact, both his own researches and his editions of lecture notes of Adjukiewicz and ?ukasiewicz. In addition, the surviving records of his student time at Warsaw University provide information on a little-studied topic.

Presburger arithmetic is the first-order theory of the natural numbers with addition. We characterize sets that can be defined by a Presburger formula as exactly the sets whose characteristic functions can be represented by rational generating functions; a geometric characterization of such sets is also given. In addition, ifp= are a subset of the free variables in a Presburger formula, we can define a counting functiong to be the number of solutions to the formula, for a givenp. (...) We show that every counting function obtained in this way may be represented as, equivalently, either a piecewise quasi-polynomial or a rational generating function. Finally, we translate known computational complexity results into this setting and discuss open directions. (shrink)

We prove a cell decomposition theorem for Presburger sets and introduce a dimension theory for Z-groups with the Presburger structure. Using the cell decomposition theorem we obtain a full classification of Presburger sets up to definable bijection. We also exhibit a tight connection between the definable sets in an arbitrary p-minimal field and Presburger sets in its value group. We give a negative result about expansions of Presburger structures and prove uniform elimination of imaginaries for (...) Presburger structures within the Presburger language. (shrink)

We begin by proving that any Presburger-definable image of one or more sets of powers has zero natural density. Then, by adapting the proof of a dichotomy result on o-minimal structures by Friedman and Miller, we produce a similar dichotomy for expansions of Presburger arithmetic on the integers. Combining these two results, we obtain that the expansion of the ordered group of integers by any number of sets of powers does not define multiplication.

Let be the set of nonnegative integers. We show the two following facts about Presburger's arithmetic:1. 1. Let . If L is not definable in , + then there is an definable in , such that there is no bound on the distance between two consecutive elements of L′. and2. 2. is definable in , + if and only if every subset of which is definable in is definable in , +. These two Theorems are of independent interest but (...) we will get from them new proofs of Cobham's and Semenov's Theorems ; Semenov's Theorem is:Let k and l be multiplicatively independent . If is definable in and in then L is recognizable . Here Vm is the function which sends a nonzero natural number to the greatest power of m dividing it. (shrink)

We give a simple proof characterizing the complexity of Presburger arithmetic augmented with additional predicates. We show that Presburger arithmetic with additional predicates is Π 1 1 complete. Adding one unary predicate is enough to get Π 1 1 hardness, while adding more predicates (of any arity) does not make the complexity any worse.

Let G be a model of Presburger arithmetic. Let be an expansion of the language of Presburger. In this paper, we prove that the ‐theory of G is ‐minimal iff it has the exchange property and is definably complete (i.e., any bounded definable set has a maximum). If the ‐theory of G has the exchange property but is not definably complete, there is a proper definable convex subgroup H. Assuming that the induced theories on H and are definable (...) complete and o‐minimal respectively, we prove that any definable set of G is ‐definable. (shrink)

We present a description of rigid models of Presburger arithmetic (i.e., ‐groups). In particular, we show that Presburger arithmetic has rigid models of all infinite cardinalities up to the continuum, but no larger.

This paper is devoted to understand groups definable in Presburger Arithmetic. We prove the following theorems: Theorem 1. Every group definable in a model of Presburger Arithmetic is abelian-by-finite. Theorem 2. Every bounded abelian group definable in a model of (Z, +, <) Presburger Arithmetic is definably isomorphic to (Z, +)^n mod out by a lattice.

This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing (...) translation of the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)

We show that if a first-order structure${\cal M}$, with universe ℤ, is an expansion of (ℤ,+,0) and a reduct of (ℤ,+,<,0), then${\cal M}$must be interdefinable with (ℤ,+,0) or (ℤ,+,<,0).

Generalizing Cooper’s method of quantifier elimination for Presburger arithmetic, we give a new proof that all parametric Presburger families \ [as defined by Woods ] are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f for every polynomial \. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic by multiplication by scalars \: \alpha \in R, t \in X\}\) where R is any ring of (...) functions from X into \. (shrink)

We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are well-designed to specify and verify systems that can be modelled with counter systems. The paper recalls the general framework of LTL over concrete domains and presents the main decidability and complexity results related to fragments of Presburger LTL. Related formalisms are also briefly presented.

oris, 1986, 17-34, Seminarberichte 86, Humboldt University, Berlin, where, with G. Cherlin, we gave a detailed proof of a result of Alexei L. Semenov that the theory of (N, +, 2x) is decidable and admits quantifier elimination in an expansion of the language containing the Presburger..

We carry out a study of definability issues in the standard models of Presburger and Skolem arithmetics (henceforth referred to simply as Presburger and Skolem arithmetics, for short, because we only deal with these models, not the theories, thus there is no risk of confusion) supplied with free unary predicates—which are strongly related to definability in the monadic SOA (second-order arithmetic) without × or + , respectively. As a consequence, we obtain a very direct proof for ${\Pi^1_1}$ -completeness (...) of Presburger, and also Skolem, arithmetic with a free unary predicate, generalize it to all ${\Pi^1_n}$ -levels, and give an alternative description of the analytical hierarchy without × or + . Here ‘direct’ means that one explicitly m-reduces the truth of ${\Pi^1_1}$ -formulae in SOA to the truth in the extended structures. Notice that for the case of Presburger arithmetic, the ${\Pi^1_1}$ -completeness was already known, but the proof was indirect and exploited some special ${\Pi^1_1}$ -completeness results on so-called recurrent nondeterministic Turing machines—for these reasons, it was hardly able to shed any light on definability issues or possible generalizations. (shrink)

Alfred Tarski was one of the greatest logicians of the twentieth century. His influence comes not merely through his own work but from the legion of students who pursued his projects, both in Poland and Berkeley. This chapter focuses on three key areas of Tarski's research, beginning with his groundbreaking studies of the concept of truth. Tarski's work led to the creation of the area of mathematical logic known as model theory and prefigured semantic approaches in the philosophy of language (...) and philosophical logic, such as Kripke's possible worlds semantics for modal logic. We also examine the paradoxical decomposition of the sphere known as the Banach–Tarski paradox. Finally we examine Tarski's work on decidable and undecidable theories, which he carried out in collaboration with students such as Mostowski, Presburger, Robinson and others. (shrink)

In a famous paper of 1931, Gödel proved that any formalization of elementary Arithmetic is incomplete, in the sense that it contains statements which are neither provable nor disprovable. Some two years before this, Presburger proved that a mutilated system of Arithmetic, employing only addition but not multiplication, is complete. This essay is partly an exposition of a system such as Presburger's, and partly an attempt to gain insight into the source of the incompleteness of Arithmetic, by linking (...) Presburger's result with Gödel's. Chapter 1, p. 1. (shrink)

We prove that the set of all recursive functions cannot be inferred using first-order queries in the query language containing extra symbols $\lbrack +, . The proof of this theorem involves a new decidability result about Presburger arithmetic which is of independent interest. Using our machinery, we show that the set of all primitive recursive functions cannot be inferred with a bounded number of mind changes, again using queries in $\lbrack +, . Additionally, we resolve an open question in (...) [7] about passive versus active learning. (shrink)

Linear arithmetics are extensions of Presburger arithmetic () by one or more unary functions, each intended as multiplication by a fixed element (scalar), and containing the full induction schemes for their respective languages. In this paper, we construct a model of the 2‐linear arithmetic (linear arithmetic with two scalars) in which an infinitely long initial segment of “Peano multiplication” on is ‐definable. This shows, in particular, that is not model complete in contrast to theories and that are known to (...) satisfy quantifier elimination up to disjunctions of primitive positive formulas. As an application, we show that, as a discretely ordered module over the discretely ordered ring generated by the two scalars, does not have the NIP, answering negatively a question of Chernikov and Hils. (shrink)

We study here equiformity, the standard identity criterion for sentences. This notion was put forward by Lesniewski, mentioned by Tarski and defined explicitly by Presburger. At the practical level this criterion seems workable but if the notion of sentence is taken as a fundamental basis for logic and mathematics, it seems that this principle cannot be maintained without vicious circle. It seems also that equiformity has some semantical features ; maybe this is not so clear for individual signs but (...) sentences are often considered as meaningful combinations of signs. If meaning has to play a role, we are thus maybe in no better position than when dealing with identity criterion for propositions. In formal logic, one speaks rather about well-formed formulas, but closed formulas are called sentences because they are meaningful in the sense that they can be true or false. Formulas look better like mathematical objects than material inscriptions and equiformity does not seem to apply to them. Various congruencies can be considered as identities between formulas and in particular "to have the same logical form". One can say that the objects of study of logic are rather logical forms than sentences conceived as material inscriptions. (shrink)

We prove that for every Scott set S there are S-saturated real closed fields and S-saturated models of Presburger arithmetic.

We study Fermat's last theorem and Catalan's conjecture in the context of weak arithmetics with exponentiation. We deal with expansions of models of arithmetical theories (in the language ) by a binary (partial or total) function e intended as an exponential. We provide a general construction of such expansions and prove that it is universal for the class of all exponentials e which satisfy a certain natural set of axioms. We construct a model and a substructure with e total and (...) (Presburger arithmetic) such that in both and Fermat's last theorem for e is violated by cofinally many exponents n and (in all coordinates) cofinally many pairwise linearly independent triples. On the other hand, under the assumption of ABC conjecture (in the standard model), we show that Catalan's conjecture for e is provable in (even in a weaker theory) and thus holds in and. Finally, we also show that Fermat's last theorem for e is provable (again, under the assumption of ABC in ) in “coprimality for e”. (shrink)

In this paper the modal operator "x is provable in Peano Arithmetic" is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

In this work a double exponential time inseparability result is proven for a finitely axiomatizable first order theory Q₊. The theory, subset of Presburger theory of addition S₊, is the additive fragment of Robinson system Q. We prove that every set that separates Q₊` from the logically false sentences of addition is not recognizable by any Turing machine working in double exponential time. The lower bound is given both in the non-deterministic and in the linear alternating time models. The (...) result implies also that any theory of addition that is consistent with Q₊—in particular any theory contained in S₊—is at least double exponential time difficult. Our inseparability result is an improvement on the known lower bounds for arithmetic theories. Our proof uses a refinement and adaptation of the technique that Fischer and Rabin used to prove the difficulty of S₊. Our version of the technique can be applied to any incomplete finitely axiomatizable system in which all of the necessary properties of addition are provable. (shrink)

Van den Dries, L. and J. Holly, Quantifier elimination for modules with scalar variables, Annals of Pure and Applied Logic 57 161–179. We consider modules as two-sorted structures with scalar variables ranging over the ring. We show that each formula in which all scalar variables are free is equivalent to a formula of a very simple form, uniformly and effectively for all torsion-free modules over gcd domains . For the case of Presburger arithmetic with scalar variables the result takes (...) a still simpler form, and we derive in this way the polynomial-time decidability of the sets defined by such formulas. (shrink)

Biró, B. and I. Sain, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, Annals of Pure and Applied Logic 63 201-225. We show that one can prove the partial correctness of more programs using Peano's axioms for the time frames of three-sorted time models than using only Presburger's axioms, that is it is useful to allow multiplication of time points at program verification and in dynamic and temporal logics. We organized the (...) paper as follows: 1. Preliminaries, 2. The main result, 3. Peano arithmetic with bounded multiplication, 4. Connections with temporal logics and dynamic logics, Acknowledgements, References. (shrink)

We present an elementary three-pass algorithm for computing addition in Ostrowski numeration systems. When a is quadratic, addition in the Ostrowski numeration system based on a is recognizable by a finite automaton. We deduce that a subset of X⊆Nn is definable in, where Va is the function that maps a natural number x to the smallest denominator of a convergent of a that appears in the Ostrowski representation based on a of x with a nonzero coefficient if and only if (...) the set of Ostrowski representations of elements of X is recognizable by a finite automaton. The decidability of the theory of follows. (shrink)