FOM: Re: completeness theorem for stratification?
T.Forster at dpmms.cam.ac.uk
Thu Apr 13 06:37:28 EDT 2000
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!)
More information about the FOM