What fragments of ZF are consistent with a set being equal in size to its power set?

Question

What examples of fragments of ZF are consistent with: $$\exists x \exists f\, (f\colon x \to P(x) \wedge f \text{ is bijective})$$ and are not too weak, ideally with at least the consistency strength of PA?

• The fragment that I know of is the theory axiomatized by Extensionality, Singletons, Boolean union, Power, Predicative stratified instances of Separation, and Infinity (in the form $\exists x\, (x \text{ is infinite})$)

• Another theory has the same axioms above plus set union, but with separation restricted to stratified formulas with three types.

• Another theory has all the above axioms and allows all stratified instances of separation, but asserts Extensionality only for non-empty objects. This theory is not known to prove a set that is equal to its power in size, but is consistent with all types of inequality of size between a set and its power. The references for this are known to people working with NF(U).

What other known fragments of ZF are not too weak, and yet are consistent with a set being equal to its power set in size?

Answer 1

Your question is related to Lawvere's fixed point theorem, about which I wrote a blog post a while ago. It takes next to nothing to prove the following theorem:

Theorem (Lawvere): If $e : A \to B^A$ be a surjection. Then every map $f : B \to B$ has a fixed point.

Proof. Consider the map $g : A \to B$ defined by $g(x) = f(e(x)(x))$. Because $e$ is a surjection, there is $a \in A$ such that $e(a) = g$. Now we have $e(a)(a) = g(a) = f(e(a)(a))$, therefore $e(a)(a)$ is a fixed point of $f$. QED.

It will be difficult to find a set theory which admits sets of functions but does not allow you to prove the above theorem. The point is that the theorem immediately implies Cantor's theorem.

Corollary: There is no surjection $A \to 2^A$.

Proof. The map $f : 2 \to 2$ defined by $f(0) = 1$ and $f(1) = 0$ has no fixed points, therefore we cannot have a surjection $A \to 2^A$. QED.

Observe that all of what we have said so far is intuitionistically valid, so it applies to classical as well as intuitionistic set theory. (Caveat: intuitionistically the powerset of $A$ is not $2^A$ but $\Omega^A$ where $\Omega = \mathcal{P}(1)$, the powerset of the singleton; nevertheless, the corollary still works because the complement/negation map $\Omega \to \Omega$ has no fixed points.)

The above arguments can be made as soon as we have the ability to form sets of functions. So I wonder how you manage to prove that there is a bijection between a set and its power-set in your fragments. Are you quite sure you can speak about functions in a normal way? Or to put it another way, which part of the proof of Lawvere's theorem doesn't work in your fragments of set theory?

As far as I am concerned, Lawvere's and Cantor's theorems are completely independent of set theory. They are basic facts about functions.