 The rejection of (T3) and (T3′) is not the only problem related to a TRL-semantics defined in this way. It should also be pointed out that it is somewhat complicated to state the semantics of modal expressions if we follow this procedure, since it may involve the quantification over possible TRL-functions. This approach has been further investigated in (Braüner et al. 1998).