FOM: Re: completeness theorem for stratification?

[Thomas Forster]

A formula of set theory is typed if one can assign integers to all
its vbls (all occurrences of the same vbl get the same integer) in
such a way that if x \in y is a subformula then the integer assigned
to x is one lower than the integer assigned to y.

Rieger-Bernays permutation models (not to be confused with FM permutation)
models are the following device.  Let V, \in  be a model of some sort of
set theory, and \pi a permutation of V.   In the new model we believe
that x is a member of y if the old model thinks that x \in \pi(y).  This
construction preserves stratified formulae.   In fact a formula is
(equivlent to a) stratified formula iff the class of its models is closed
under this construction.  A bit of good old-fashioned model theory! There
is a similar concept of stratification in lambda-calculus and a similar 
completeness theorem.   See ZML 1990 pp 385-388 (for set theory) and
Theoretical Computer science 1993 pp 405-418.  I have a pile of offprints   
of these two that i would be only too happy to send to interested parties.
(we are about to move to new, smaller premisses!)
           Thomas Forster