Abstract We introduce two weak first-order theories of weighted and labelled finite trees, T*† and T*‡, respectively. It is proved that T*† and T*‡ are mutually interpretable with other previously studied elementary theories of ‘undecorated’ finite trees, as well as with Robinson Arithmetic, Q, and a host of other weak first-order theories of numbers, strings, sets and sequences.
Zlatan Damnjanovic (Mon,) studied this question.