3
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ It will have to be weak to keep from forming the set of members y of x which do not belong to f(y), while still having the power to express your notion. Gerhard "Not Sure Of The Utility" Paseman, 2018.08.23. $\endgroup$ – Gerhard Paseman Aug 23 '18 at 19:52
  • $\begingroup$ @GerhardPaseman if for example Con(NF) is proved then we can have a fragment that can interpret $\omega$_order arithmetic and yet be consistent with this notion. To me any fragment near the strength of $PA$ is not to be considered weak. $\endgroup$ – Zuhair Al-Johar Aug 23 '18 at 21:26
  • $\begingroup$ You really should use the lo.logic tag, this is the second time I've added it to a question you asked in this area. Also, use \text as a wrapper for when you want text inside a math environment $\endgroup$ – David Roberts Aug 23 '18 at 22:29
  • $\begingroup$ @DavidRoberts thanks $\endgroup$ – Zuhair Al-Johar Aug 23 '18 at 23:25
  • 1
    $\begingroup$ @MattF. your comment is not correct. An injection form P(N) to N is not consistent with IZF. The statement that there can be no injection from P(A) to A for any A follows from Cantor's argument, which is purely constructive. Perhaps, you have confused P(N) with $N^N$, or $2^N$... $\endgroup$ – Michal R. Przybylek Aug 24 '18 at 22:29
9
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Note that this is true even in NF as long as you look at it categorically. The reason you can have $V=\mathcal{P}(V)$ is because $\mathcal{P}(V)$ is not a categorical power object of $V$; it's a power object of $\{\{x\}:x\in V\}$. NF's stratification requirement prevents us from forming the necessary universal maps to make it the power object of $V$. Something similar will probably be going on in any such fragment: your "power sets" will lack a certain universal property. $\endgroup$ – Malice Vidrine Aug 25 '18 at 22:30
  • $\begingroup$ The definition of map $g$ is not stratified, you have $e(x)(x)$ so $x$ will receive the same type as $e(x)$ since $e(x)$ is the image of $x$ under $e$ and also $x$ appears one type lower than $e(x)$ since it is the argument of $e(x)$, so that won't work in the stratified fragments that I've mentioned. $\endgroup$ – Zuhair Al-Johar Aug 26 '18 at 2:55
  • $\begingroup$ as about the ability of the fragments that I've mentioned, the last one which is the one having non-extensionals is as strong as $\omega$-order arithmetic. I think (I'm not sure) that we can have much stronger fragments and yet compatible with existence of a set that is equipotent with its power. $\endgroup$ – Zuhair Al-Johar Aug 26 '18 at 3:00
  • $\begingroup$ I am not familiar with NF, so thanks for explaining where things fail to work. From a category-theoretic point of view I find it odd that we'd still call something "function space" or "powerset" if it does not behave like one. $\endgroup$ – Andrej Bauer Aug 26 '18 at 8:53
2
$\begingroup$

The set theory IZF, for intuitionist set theory, is equiconsistent with ZF, and also consistent with an injection from $2^\mathbf{N}$ to $\mathbf{N}$.

As a reference, see Michael Beeson, Foundations of Constructive Mathematics (1985) chapter VIII. Section 1 defines IZF. Corollary 3.4 gives the equiconsistency. Theorem 8 gives the consistency with the variant of Church’s thesis saying that “for every function $f: \mathbf{N} \rightarrow \mathbf{N}$, there is an integer $m$ such that $f$ is the $m^{th}$ recursive function.” Note that this version of Church’s thesis is incompatible with excluded middle.

In this context $2^\mathbf{N}$ only has functions for which $f(n)=0$ or $f(n)=1$, while $\mathbf{P(N)}$ also includes sets for which we can neither prove $n \in x$ nor prove $n \notin x$. Similarly the injection from $2^\mathbf{N}$ to $\mathbf{N}$ does not provide a surjection from $\mathbf{N}$ to $2^\mathbf{N}$. So in both ways this result is slightly less than what you asked for, but it still provides a good example where the set-power set inequality is almost reversed.

$\endgroup$
  • 4
    $\begingroup$ The theory actually proves that no surjection $\mathbb N\to2^{\mathbb N}$ exists. $\endgroup$ – Emil Jeřábek Aug 25 '18 at 7:11
  • 3
    $\begingroup$ You don't get an injection using Church's thesis, you only get a subquotient, i.e., $2^\mathbb{N}$ is a quotient of a subset of $\mathbb{N}$. And in any case, $2^\mathbb{N}$ is not the powerset in intuitionistic set theory. $\endgroup$ – Andrej Bauer Aug 25 '18 at 9:44
  • $\begingroup$ @AndrejBauer, you’re right that CT provides the injection only with a subquotient, but I wonder if we can still show the consistency with the existence of an injection. $\endgroup$ – Matt F. Aug 25 '18 at 9:57
  • $\begingroup$ Can you clarify the statement of the CT variant? Is it asserting the existence of a set expressing the graph of a surjection $\mathbf{N} \to \mathbf{N}^\mathbf{N}$, or is it a metatheorem about the possible logical formulas defining relations that are provably functions? (or something else?) $\endgroup$ – Hurkyl Aug 25 '18 at 10:00
  • 1
    $\begingroup$ Well, there is my paper An injection from Baire space and natural numbers which explains that you get an injection in realizability over infinite time Turing machines (but not ordinary Turing machines). $\endgroup$ – Andrej Bauer Aug 25 '18 at 10:15

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.