Equivariant polynomial ideals

In this joint work with Sławek Lasota we study ideals of polynomials, where variables are elements of a countable logical structure. In this setting we allow structure-preserving embeddings to act on polynomials by renaming variables, and focus on ideals of polynomials which are equivariant, i.e., invariant under remaming. As our first result, we aim to identify logical structures that admit Hilbert's Basis Property: every equivariant ideal of polynomials is finitely generated. We conjecture that a structure admits Hilbert's basis property if and only if the class of its finite substructures labelled with natural numbers is well quasi ordered under the induced substructure relation. We show this condition is necessary, and a slightly stronger condition is sufficient. This shows that Hilbert's basis property holds for several structures such as the natural numbers with order, countable dense linear order and the countable dense tree, and does not hold for structures such as the random graph or natural numbers with the successor relation. As far as we know, equivalence of our necessary and sufficient conditions is an open problem. Furthermore, for several structures satisfying Hilbert's basis property, we extend the classical Buchberger's algorithm to compute a Groebner basis of a given equivariant ideal, which implies decidability of the membership problem for equivariant ideals. This result has various applications, for instance in deciding reachability of reversible Petri nets with data, or in solving orbit-finite systems of linear equations.