 Suppose that the set of atomic propositions of TL is \({PROP}=\left\{p_{0},p_{1},...\right\}\), and let \(L_{1}\) be a first-order language with \(=,\) a binary predicate symbol \(R,\) and a denumerable set of unary predicate symbols \(\mathcal{P}=\left\{P_{0},P_{1},...\right\}\), one for each atomic proposition of TL. The standard translation \(ST\) of TL into \(L_{1}\) is defined as follows, where \(\theta[y/x]\) is the result of substituting \(y\) for all free occurrences of \(x\) in \(\theta\):