Abstract:
We develop a theory of (first-order) definability in the subword partial order in parallel with similar theories for the $h$-quasiorder of finite $k$-labeled forests and for the infix order. In particular, any element is definable (provided that the words of length 1 or 2 are taken as parameters), the first-order theory of the structure is atomic and computably isomorphic to the first-order arithmetic. We also characterize the automorphism group of the structure and show that every predicate invariant under the automorphisms of the structure is definable in the structure.
Keywords:subword, infix order, definability, automorphism, least fixed point, first-order theory, bi-interpretability.