We show that the equational theory of the structure $\langle ω^ω: (x,y)\mapsto x+y, x\mapsto ω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.

Given a subset of $X\subseteq \mathbb{R}^{n}$ we can associate with every point $x\in \mathbb{R}^{n}$ a vector space $V$ of maximal dimension with the property that for some ball centered at $x$, the subset $X$ coincides inside the ball with a union of lines parallel with $V$. A point is singular if $V$ has dimension $0$. In an earlier paper we proved that a $(\mathbb{R}, +,< ,\mathbb{Z})$-definable relation $X$ is actually definable in $(\mathbb{R}, +,< ,1)$ if and only if the number of singular points is finite and every rational section of $X$ is $(\mathbb{R}, +,< ,1)$-definable, where a rational section is a set obtained from $X$ by fixing some component to a rational value. Here we show that we can dispense with the hypothesis of $X$ being $(\mathbb{R}, +,< ,\mathbb{Z})$-definable by assuming that the components of the singular points are rational numbers. This provides a topological characterization of first-order definability in the structure $(\mathbb{R}, +,< ,1)$. It also allows us to deliver a self-definable criterion (in Muchnik's terminology) of $(\mathbb{R}, +,< ,1)$- and $(\mathbb{R}, +,< ,\mathbb{Z})$-definability for a wide class of relations, which turns into an effective criterion provided that the corresponding theory is decidable. In particular these results apply to the class of $k-$recognizable relations on reals, and allow us to prove that it is decidable whether a $k-$recognizable relation (of any arity) is $l-$recognizable for every base $l \geq 2$.

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 [Formula: see text] for every ordinal λ. Moreover, we prove (by reduction from Hilbert Tenth Problem) that the ∃*∀ 6 -fragment of [Formula: see text] is undecidable for every ordinal λ.

We consider the first-order theory of the monoid P(A*) of languages over a finite or infinite alphabet A (with at least two letters) endowed solely with concatenation lifted to sets: no set theoretical predicate or function, no constant. Coding a word u by the submonoid u* it generates, we prove that the operation (u*, v*) → (uv)* and the predicate {(u*,X) | ε ∈ X, u ∈ X} are definable in 〈P(A*); ·,=〉. This allows to interpret the second-order theory of 〈A*; ·,=〉 in the first-order theory of 〈P(A*); ·,=〉 and prove the undecidability of the Π 8 fragment of this last theory. These results involve technical difficulties witnessed by the logical complexity of the obtained definitions: the above mentioned predicates are respectively Δ 5 and Δ 7 .

Eilenberg and al. introduced and studied in the late sixties the family of n-ary relations over the free monoid recognized by finite n-tape automata where the where the n reading heads tapes move simultaneously from left to right. We call these relations synchronous. In the eighties Angluin and Hoover and then Läuchli and Savioz introduced a proper subfamily which the first authors called regular prefix. Our main result shows that given a synchronous relation it is decidable whether or not it is regular prefix. Incidentally we also show that the family of regular prefix relations is uniformizable in the sense that all such relations contain a partial function with the same domain whose graph is a regular prefix relation.

The regular languages in the free monoid generated by a finite alphabet A are exactly the languages that are the models of some sentence of the second-order monadic logic of one successor and a unary predicate for each letter. For trace monoids the n

We consider the subfamilies of rational and pushdown transducers and corresponding translations (relations) which are most frequently encountered in the literature. We survey some of the known results on the characterization, factorization, closure properties, decision problems and comparisons of classes and give new results on these properties using either direct proofs or results from other theories such as homomorphic equivalence.