Equational theory of ordinals with addition and left multiplication by $\omega$

TL;DR

This paper establishes a finite axiomatization for the equational theory of a structure involving ordinals with addition and left multiplication by omega, providing a decision algorithm for term equality.

Contribution

It introduces a finite axiomatization and a linear-time decision algorithm for the equational theory of ordinals with addition and omega-multiplication.

Findings

Finite axiomatization of the theory

Linear-time decision algorithm for term equality

Simplified axiom schema for transfinite ordinals

Abstract

We show that the equational theory of the structure $\langle \omega^{\omega}: (x,y)\mapsto x+y, x\mapsto \omega x \rangle $ is finitely axiomatizable and give a simple axiom schema when the domain is the set of transfinite ordinals. We give an algorithm that given a pair of terms $(E,F)$ decides in linear time with respect of their common length whether or not $E=F$ is a consequence of the axioms.