Cardinal powers

Stream: Is there code for X?

[Mac Malone]

Does the following generally hold? If so, is there simple way to show it with Mathlib?

∀ a b, (2 : Cardinal) ^ a ≤ (2 : Cardinal) ^ b → a ≤ b

One of my thoughts is that the following might hold for infinite cardinals:

∀ a, ℵ₀ < a → ((2 : Cardinal) ^ a).ord = a.ord + 1

But I also could not find something like this in Mathlib. Thus, I may be completely confused and these properties just do not hold. That would also be nice to know.

[Daniel Weber]

The first one doesn't necessarily hold, it's consistent with ZFC that there exist sets A, B with |A| < |B| but 2^|B| = 2^|A| (https://mathoverflow.net/a/6594/498835).

[Mac Malone]

@Daniel Weber Doesn't the first still hold with |A| < |B| and 2^|B| = 2^|A|? That is, 2^|B| = 2^|A| -> 2^|A| <= 2^|B| and |A| < |B| -> |A| <= |B| so 2^|A| <= 2^|B| -> |A| <= |B| still hods.

[Mac Malone]

The math overflow case seems to be about <, not <=.

[Daniel Weber]

The second necessarily doesn't hold

import Mathlib

open Cardinal

example (h : ∀ a, ℵ₀ < a → ((2 : Cardinal) ^ a).ord = a.ord + 1) : False := by
  specialize h (2 ^ ℵ₀) (cantor _)
  apply le_of_eq at h
  rw [Cardinal.ord_le, two_power_aleph0, Ordinal.add_one_eq_succ, Ordinal.card_succ, card_ord, add_one_eq] at h
  · absurd h
    simp [cantor]
  · exact aleph0_le_continuum

[Daniel Weber]

Mac Malone said:

Daniel Weber Doesn't the first still hold with |A| < |B| and 2^|B| = 2^|A|? That is, 2^|B| = 2^|A| -> 2^|A| <= 2^|B| and |A| < |B| -> |A| <= |B| so 2^|A| <= 2^|B| -> |A| <= |B| still hods.

Swap A and B, so 2^|B| <= 2^|A|, therefore |B| <= |A|, but |A| < |B|, contradiction

[Mac Malone]

Daniel Weber said:

The second necessarily doesn't hold

Oops, I apparently confused myself on what ordinals are. I mistakingly though ω + 1 = ω₁.

[Mac Malone]

Upon reflection, I don't know why I thought that. (I think I mixed aleph n with ord a = n.)

[Mac Malone]

Ah, I think what I wanted for (2) was:

∀ (n : Ordinal), (2 : Cardinal) ^ Cardinal.aleph n = Cardinal.aleph (n + 1)

which I presume also doesn't hold for the same reason as (1)?

[Daniel Weber]

That's exactly the generalized continuum hypothesis (which is, indeed, independent of ZFC)

[Mac Malone]

Great! I thought there was a name for that.

[Mac Malone]

Thanks for your help!

[Kevin Buzzard]

In general ZFC has very little to say about the function F on cardinals sending x to 2^x. We have x<F(x) and x<=y implies F(x)<=F(y) and there is another result about cofinalities which says something about behaviour of F at aleph_t where t is a limit, but other than that you can use forcing to make F be pretty much anything. For example my understanding is that there will be a model of ZFC where 2^aleph0=2^aleph1=aleph37 and 2^aleph2=aleph42.

[Nir Paz]

Kevin Buzzard said:

In general ZFC has very little to say about the function F on cardinals sending x to 2^x. We have x<F(x) and x<=y implies F(x)<=F(y) and there is another result about cofinalities which says something about behaviour of F at aleph_t where t is a limit, but other than that you can use forcing to make F be pretty much anything. For example my understanding is that there will be a model of ZFC where 2^aleph0=2^aleph1=aleph37 and 2^aleph2=aleph42.

Powers of regular cardinals (like all the ℵ_n's for n∈ℕ) can be any F with only a few simple restrictions, but powers of singular cardinals actually have very nontrivial restrictions! For example if for every n∈ℕ it holds that 2 ^ ℵ_n = ℵ_m for some m∈ℕ (F doesn't "jump" over ℵ_ω), then 2 ^ ℵ_ω < ℵ_(ω₄).

[Kevin Buzzard]

Right! This was supposed to be covered by the comment about limit cardinals :-) (which I left vague because I couldn't remember the details :-) )