  where ‘\(x\)’ is not free in \(\Phi\) and \(\Phi\) is (weakly) stratified. This last condition requires that there should be a function \(\sigma\) (a “stratification”) from the bound variables in \(\Phi\) to an initial segment of the natural numbers such that if ‘\(u \in v\)’ is a subformula of \(\Phi\) then \(\sigma(`v\rsquo) = \sigma(`u\rsquo) + 1\) and if \(`u = v\rsquo\) is a subformula of \(\Phi\) then \(\sigma(`v\rsquo) = \sigma(`u\rsquo)\). The origins of this constraint will be explained below.