[thesz]

They used LTL as non-reduced binary decision diagrams (BDDs, binary trees in essence) to prove that transformers are exponentially more succinct that LTL. Should they allow reductions in LTL expressions, that exponential advantage of transformers would vanish in a puff of smoke, because reduced ordered decision diagrams (ROBDDs) of addition circuits (used to construct their exponential LTL example) are polynomially sized.

How to add reductions to LTL? Allow (parametric) definitions of subformulas. E.g., "let p = ... in xUp/\yUp".

Also, note that they construct transformers, transformers are not trained. Training on any truth table is as hard as one can imagine.