Бесконечные ветви в разрешимых деревьях

Мы рассматриваем структуру $\mathcal{M} = \langle \mathbb{N}, \{\mathit{Tr}, <\}\rangle$, где отношение $Tr(a, x, y)$ с параметром a задаёт семейство деревьев на $\mathbb{N}$ и < – стандартный порядок на $\mathbb{N}$. Утверждается, что если элементарная теория структуры $\mathcal{M}$ разрешима, то (1) отношение $Q(a) \leftrightharpoons$ ”существует бесконечная ветвь в дереве $Tr(a, x, y)$” определимо в $\mathcal{M}$, и (2) если существует бесконечная ветвь в дереве $Tr(a, x, y)$, то существует определимая бесконечная ветвь в дереве $Tr(a, x, y)$.
Подробное изложение: https://arxiv.org/abs/1801.00423