Decidability of the existential fragment of some infinitely generated trace monoids: an application to ordinals

TL;DR

This paper extends the decidability results of the existential first-order theory from finite to certain infinite trace monoids and applies this to show decidability for the multiplication of successor ordinals below epsilon_0.

Contribution

It generalizes decidability results to infinitely generated trace monoids and applies this to ordinal arithmetic.

Findings

Decidability of existential theory for certain infinite trace monoids

Decidability of multiplication of successor ordinals below epsilon_0

Extension of finite alphabet results to infinite generators

Abstract

Diekert, Matiyasevich and Muscholl proved that the existential first-order theory of a trace monoid over a finite alphabet is decidable. We extend this result to a natural class of trace monoids with infinitely many generators. As an application, we prove that for every ordinal $\lambda$ less than $\varepsilon_0$, the existential theory of the set of successor ordinals less than $\lambda$ equipped with multiplication is decidable.