Logic Colloquium: Elimination and consistency checking for difference equations (even though the theory is undecidable!)

Colloquium | September 14 | 4-5 p.m. | 60 Evans Hall

 Thomas Scanlon, UC Berkeley

 Department of Mathematics

In practice, an algebraic difference equation (of $N$ variables) is given by a set Σ of polynomials in the variables $\{ x_{i,j} ~:~ 1 \leq i \leq N, j \in \mathbb N \}$ and one looks for sequences of $N$-tuples of numbers $((a_{1,j})_{j=0}^\infty , …, (a_{N,j})_{j=0}^\infty )$ as solutions in the sense that for each $P \in \Sigma $, the equations $P(a_{1,j}, …, a_{n,j}; a_{1,j+1}, …, a_{N,j+1}; …; a_{1,d+j}, …, a_{N,d+j}) = 0$ hold for all $j \in \mathbb N$. Read more algebraically, difference equations may be understood as atomic formulae in the language of difference rings, the language of rings augmented by a function symbol for the difference operator, and we seek the solutions in the ring of sequences treated as a difference ring by interpreting the difference operator as a shift.

The theory of difference fields, that is, of fields equipped with a distinguished endomorphism, has a model companion and the theory of this model companion is known to be decidable and to admit quantifier elimination in a reasonable expansion of the language of difference rings. We set out to extend the model theory of difference fields to produce algorithms to test for the solvability of difference equations in sequence rings and to solve the elimination problem for such difference equations.

Remarkably, the theory of such difference rings is undecidable, already in low quantifier complexity. However, we were able to adapt the methods behind the axiomatization of the theory of difference closed fields to produce efficient algorithms to solve both the consistency checking and the elimination problems for difference equations in sequence rings. Even more remarkably, ultraproducts of Frobenius automorphisms play a crucial role in verifying the correctness of our algorithms,

(This is a report on joint work with Alexey Ovchinnikov and Gleb Pogudin [available at arXiv:1712.01412] and an on-going project with them joined by Wei Li.)