 Let \(\textrm{Th}({\mathcal{D}_T})\) be the first-order theory of the structure \(\mathcal{D}_T\) in the language with the with \(\equiv_T\) and \(\leq_T\). Not only is \(\textrm{Th}({\mathcal{D}_T})\) undecidable (Lachlan 1968), it is fact many-one equivalent to true second-order arithmetic (Simpson 1977).