On Non-Wellfounded Sets as Fixed Points of Substitutions

Matti Pauna

(Joint work with Tapani Hyttinen)

We work in set theory with urelements, denoted by U, and without the foundation axiom, ZF C^{−}. In [1] non-wellfounded sets and the antifoundation axiom, AF A are studied. We denote by V_{afa}[U] ∪ U the model of ZF C^{−} + AF A. Substitution operations sub(s, b), also denoted by b[s], are studied in [1]. Here s is a function, called substitution, such that dom(s) ⊆ U, and b ∈ V_{afa}[U] ∪ U, such that the following conditions hold: (i) If x ∈ dom(s), then sub(s, x) = s(x). (ii) If x ∈ U − dom(s), then sub(s, x) = x. (iii) For all sets b, sub(s, b) = {sub(s, p) | p ∈ b}. There is a unique substitution operation sub(s, b) defined for all substitutions s and b ∈ V_{afa}[U] ∪ U.

Substitutions can be composed in the following way. A substitution s is proper if for all x ∈ dom(s), s(x) ∈ V_{afa}[U] whenever s(x) ≠ x. If s and t are substitutions, then t⋆s is the substitution whose domain is dom(s) and for every x ∈ dom(s), (t ⋆ s)(x) = s(x)[t]. Now AF A is equivalent to: for every proper substitution e there is a unique proper substitution s such that s = s ⋆ e.

We study the non-wellfounded sets as fixed points of substitutions. If f is a function, let f^{∗} be the class function such that if x ∈ dom(f), f^{∗}(x) = f(x), otherwise f^{∗}(x) = x. If f and g are functions, let f[g] be the function such that dom(f[g]) = dom(g) and f[g](x) = f^{∗}(x), if x is an urelement, and otherwise f[g](x) = {g^{∗}(y) | y ∈ f^{∗}(x)}. Note that if f(x) is a set, then g(x) = {g(y) | y ∈ f(x)}. We say that g is a fixed point of f, (F P (g, f)), if dom(f) ∪ ⋃ f^{∗}[dom(g)] ⊆ dom(g) and g = f[g]. The fixed point axiom, FA is: every function has a fixed point. We have shown that assuming the strong extensionality axiom, F A and AF A are equivalent. In ZF C, let X be a set and f : X → P(X), be such that f(x) = x ∩ X. Then f has a unique fixed point g, namely the Mostowski collapse of X. We will show that from the F A it follows that for every substitution f there is g such that g = g ⋆ f. However, g is not necessarily unique, and for arbitrary f, g does not necessarily exist.

[1] Jon Barwise and Lawrence Moss, Vicious Circles, CSLI Lecture Notes, Number 60, CSLI Publications, Stanford, 1996.

Address: Department of Mathematics, University of Helsinki, Finland

E-mail: pauna@cs.helsinki.fi