Existential Theory of Polynomial Rings with Divisibility

Definitions and mathematical statement

Let $q=p^r$, where $p$ is prime and $r\geq 1$, and let $R_q=\mathbb F_q[t]$ be the polynomial ring in one indeterminate over the field with $q$ elements. Addition has its usual meaning, and divisibility is the binary relation \[ a\mid b\quad\Longleftrightarrow\quad (\exists c\in R_q)\ b=ac. \] Thus $0\mid b$ holds exactly when $b=0$.

The source asks whether the existential theory of $R_q$, with addition, divisibility, and a unary predicate for powers of $t$, is decidable. To describe the decision problem precisely under the minimal signature reading, put $L=\{+,\mid,P\}$, with equality available as a logical symbol. Interpret $+$ and $\mid$ as above. Under the nonnegative-exponent convention, interpret \[ P(f)\quad\Longleftrightarrow\quad f=t^n\text{ for some integer }n\geq 0. \] An existential $L$-sentence is a sentence \[ \exists x_1\cdots\exists x_m\,\varphi(x_1,\ldots,x_m), \] where $m\geq 0$ and $\varphi$ is quantifier-free; all variables range over $R_q$. Its quantifier-free part may use arbitrary Boolean combinations of atomic formulas. The existential theory is the set of these sentences that hold in the specified structure.

Question, subject to the qualifications below. For a fixed prime power $q$, is there an algorithm that, on every input existential sentence in the intended language, terminates and correctly decides whether that sentence holds in the intended structure on $\mathbb F_q[t]$?

Unresolved source qualifications. The supplied record does not explicitly specify any constant symbols or named parameters. Consequently, the minimal signature above is a conditional interpretation; adding names for $0$, $1$, $t$, or field elements must not be assumed without source clarification. Likewise, the record does not explicitly say whether the powers predicate includes $t^0=1$; if only positive powers are intended, its interpretation is instead $\{t^n:n\geq 1\}$. The record also does not distinguish decidability separately for each fixed $q$ from a uniform algorithm taking a description of the finite field as additional input. No equivalence between these alternative formulations is asserted here.

The supplied dated assessment labels the problem partially solved and reports decidability of the one-existential-quantifier fragment while describing the full existential theory as open. These are supplied literature claims, not independently verified conclusions of this draft.

Short English statement

The question asks for an algorithm deciding existential statements about polynomials over a finite field using addition, divisibility, and a predicate selecting powers of $t$. The exact signature, whether the predicate includes $1=t^0$, and whether the algorithm must work uniformly across finite fields remain unspecified. The supplied partial-solution assessment requires independent review.

Sources

• Local UnsolvedMath registry, supplied source record with permanent ID $30003249$, title Existential Theory of Polynomial Rings with Divisibility, source problem code catalogue entry, in the Oberwolfach Reports Open Problems collection. No individual proposer is identified; the supplied proposed year is 2016.
• Supplied report citation: Definability and Decidability Problems in Number Theory (2017), Oberwolfach Reports, DOI 10.4171/owr/2016/49, pp. 2793--2866. https://doi.org/10.4171/owr/2016/49. The background describes this collection as drawn from workshop reports and their open-problem discussions.
• Supplied literature source: Sirokofskich, Weak Divisibility. https://jaf.lacl.fr/JAF27/alla.pdf.
• Supplied literature source: Oberwolfach Reports 2017. https://ems.press/content/serial-article-files/46652.
• Literature assessment dated exactly 2026-08-21: the record labels the problem partially_solved and states that the one-existential-quantifier fragment is decidable while the full existential theory in the stated language remains open. This is supplied dated curation derived from the OWR material, not an independently verified assessment. Its time-sensitive status and cited claims require independent verification.
• The supplied statement status is corrected_verified; its accompanying verification note reports a manual semantic, typographic, and LaTeX review. This is a source-record annotation and does not constitute mathematical or bibliographic verification by this draft.