Деревья как средство моделирования неразрешимых проблем

Доказывается неразрешимость и сильная неразрешимость (неарифметичность) теорий классов деревьев (при различных уточнениях понятия дерева и при различных требованиях к свойствам деревьев, включая конечность числа вершин) в языке с бинарной предикатной буквой, соответствующей дугам, равенством, оператором транзитивного замыкания и конгруэнтностью между парами вершин, которая определяется как равенство расстояния между вершинами первой пары расстоянию между вершинами второй пары. Показано, что для получения неразрешимости (или неарифметичности) теорий некоторых классов деревьев оператор транзитивного замыкания достаточно применять лишь к бинарному отношению, соответствующему дугам, т.е. фактически вместо оператора транзитивного замыкания рассматривать отношение достижимости; также показано, что теории некоторых классов деревьев неразрешимы в языке без оператора транзитивного замыкания.