Undecidability in the Homomorphic Quasiorder of Finite Labelled Forests

We prove that the homomorphic quasiorder of finite k-labelledforests has a hereditary undecidable first-order theory fork 3, in contrast to the known decidability result for k = 2.We establish also hereditary undecidability (again for everyk 3) of first-order theories of two other relevant structures:the homomorphic quasiorder of finite k-labelled trees, and offinite k-labelled trees with a fixed label of the root element.Finally, all three first-order theories are shown to be computablyisomorphic to the first-order arithmetic.