On elementary theories of weighted and labelled trees

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.