Trees as a tool for modelling undecidable problems

The paper proves undecidability and high undecidability (non-arithmeticity) of theories of trees (with various refinements of the concept of a tree and with various requirements for the properties of trees, including the finiteness of the number of vertices) in a language with a binary predicate letter corresponding to edges, equality, the transitive closure operator and congruence between pairs of vertices, which is defined as equality of the distance between the vertices of the first pair and the distance between the vertices of the second pair. It is shown that in many cases it is sufficient to apply the transitive closure operator only to the binary relation corresponding to edges, i.e., in fact, instead of the transitive closure operator, it is sufficient to consider the reachability relation; in some cases, we establish undecidability in a language without the transitive closure operator.