Complexity and (un)decidability of fragments of $\langle \omega^{\omega^\lambda}; \times \rangle$

TL;DR

This paper explores the computational complexity and decidability boundaries of fragments of the first-order theory of ordinal multiplication, establishing lower bounds and undecidability results for various fragments.

Contribution

It provides the first NEXPTIME lower bound for the existential fragment and proves undecidability of a specific fragment via reduction from Hilbert's Tenth Problem.

Findings

NEXPTIME lower bound for the existential fragment

Undecidability of the * ^6 fragment

Decidability frontier for fragments of ordinal multiplication theory

Abstract

We specify the frontier of decidability for fragments of the first-order theory of ordinal multiplication. We give a NEXPTIME lower bound for the complexity of the existential fragment of $\langle \omega^{\omega^\lambda}; \times, \omega, \omega+1, \omega^2+1 \rangle$ for every ordinal $\lambda$. Moreover, we prove (by reduction from Hilbert Tenth Problem) that the $\exists^*\forall^{6}$-fragment of $\langle \omega^{\omega^\lambda}; \times \rangle$ is undecidable for every ordinal $\lambda$.