Provability in predicate product logic

We sharpen Hájek’s Completeness Theorem for theories extending predicate product logic, ${Piforall}$ . By relating provability in this system to embedding properties of ordered abelian groups we construct a universal BL-chain L in the sense that a sentence is provable from ${Piforall}$ if and only if it is an L-tautology. As well we characterize the class of lexicographic sums that have this universality property.