Is anything known about the following construction? Fix a signature (function symbols with arities incl 0) Sigma and a Sigma-algebra A. Construct a new Sigma-algebra T(A) as follows: The carrier set of T(A) comprises possibly infinite trees whose nodes are labelled with function symbols in such a way that a node labelled with a k-ary function symbol has exactly k children. Thus, in particular, a leaf must be labelled with a constant symbol and if Sigma has no constant symbols then there will only be infinite trees. The carrier set T(A) is now understood modulo the largest equivalence relation ~ such that if t~t' then one can write t = u(t1,...tl) and t'=u'(t1',...,tl') for terms over Sigma in the standard sense u, u' with variables x1..xl and trees t1,...,tl,t1',...,tl'. Moreover, u=u' must hold in A and t1~t1', ..., tl~tl'. Of course, the witnessing terms u and u' should not just be x1, but rather something starting beginning with a proper function symbol.

anequivalence relation that identifies t and t' and satisfies the compatibility property mentioned in my original post. – Martin Hofmann Feb 27 '14 at 9:32