 The syntax of predicative TST is the same as that of the original system. The axioms of extensionality are also the same. The axioms of comprehension of predicative TST take the form (for any choice of a type \(n\), a formula \(\phi\), and a variable \(A^{n+1}\) not free in \(\phi\), satisfying the restriction that no parameter of type \(n + 2\) or greater appears in \(\phi\), nor does any quantifier over type \(n + 1\) or higher appear in \(\phi)\)