Supervisors

Suitable for

Abstract

Presburger arithmetic – that is, the first order theory of the natural numbers with addition – is decidable, meaning that there exists a procedure to determine if a given sentence in the language of this theory is true or false. In contrast, Peano arithmetic – which also includes multiplication – is undecidable. This naturally leads to the much-studied question: Which extensions of Presburger arithmetic are decidable? For instance, adding the square function allows us to define multiplication and hence leads to an undecidable theory. The same applies to other polynomials. But what about more general functions? We recently noticed that for a number of simple generalised polynomials – that is, expressions built up from the usual polynomials using addition, multiplication and the integer part function – the corresponding extensions are also undecidable. The idea behind this project is to investigate more broadly the question of decidability of extensions of the Presburger arithmetic by generalised polynomials.

The purpose of this project is to apply existing techniques to show in concrete cases that the extension of the Presburger arithmetic by a given generalised polynomial is undecidable. More generally, one can consider other classes of sequences which have polynomial-like behaviour in a suitable sense.

The goal is to show undecidability of the extension of the Presburger arithmetic by at least one generalised polynomial which was not previously covered. More ambitious variants correspond to dealing with wider classes of generalised polynomials.

Background on generalised polynomials can be found in (the introductory sections of) the papers:

A canonical form and the distribution of values of generalized polynomials by A. Leibman

Distribution of values of bounded generalized polynomials by V. Bergelson and A. Leibman

Pre-requisites: A course in logic, some analysis preferred but not required