Permutations and stratified formulae a preservation theorem
Thomas Förster · Mathematical logic quarterly · 1990
It is shown that the sentences (in the language of Set Theory) preserved by the construction usually used to prove the independence of the axiom of foundation can be characterised syntactically: they are precisely the formulae naturally expressible in the language of simple type theory. The permutation construction that concerns us here is familiar to students of ZF as the technique used in the standard proof of the independence of the axiom of foundation. The technique is originally due to Rieger [1957] and Bernays [1954]. If we have a model 〈V,∈ 〉 of ZF and let σ be the transposition exchanging the empty set and its singleton. Then we define x ∈σ y by x ∈ σ(y). It turns out that in the model V σ consisting of the old universe and the new membership relation ∈σ the “old ” empty set has become an object identical to its own singleton, and foundation has failed. As it happens all the other axioms of ZF are preserved.