 Let the expressions \(\phi_{\tau}\) be  variables ranging over propositional functions of type \(\tau\). We read \(x_{\tau}\) as a metalinguistic variable ranging over variables of r-type \(\tau\). The subscript \(\tau\) will be indicated only with the initial quantifier which governs the variable.