An infinite branch in a decidable tree

TL;DR

This paper proves that in a certain decidable structure involving trees on natural numbers, the existence of infinite branches is both definable and guaranteed to be definable if they exist.

Contribution

It establishes that in a decidable structure with tree relations, the property of having an infinite branch is itself definable within that structure.

Findings

The relation indicating an infinite branch is definable in the structure.

If an infinite branch exists, it can be explicitly defined within the structure.

The structure's decidability implies definability of infinite branches.

Abstract

We consider a structure $\mathcal {M} = \langle \mathbb N, \{Tr,<\} \rangle$, where the relation $Tr(a,x,y)$ with a parameter $ a$ defines a family of trees on $\mathbb N$ and $<$ is the usual order on $\mathbb N$. We show that if the elementary theory of $\mathcal M$ is decidable then (1) the relation $Q( a) \rightleftharpoons$ "there is an infinite branch in the tree $Tr( a,x,y)$" is definable in $\mathcal M$, and (2) if there is an infinite branch in the tree $Tr( a,x,y)$, then there is a definable in $\mathcal M$ infinite branch.