ZFC's properties

Stream: maths

[Jiatong Yang]

What properties do ZFC's model Set.{0} in mathlib have besides ZFC's axioms? (e.g. maybe CH)

[Kevin Buzzard]

IANAL but I don't see any reason why they should have any properties beyond what the ZFC axioms give you.

[Jiatong Yang]

I think so. Can this be proved?

[Jiatong Yang]

That is, if Lean is consistent, then all the provable properties (in FOL) of Set.{0} is provable in ZFC.

[Reid Barton]

This isn't quite right, because the existence of other universes implies Con(ZFC), which is just a statement about natural numbers. But I'm pretty sure CH will be independent.

[Eric Rodriguez]

is Type 1 genuinely bigger than Type 0? Or is that independent?

[Andrew Yang]

If one is restricted to Set.{0}, is it provable that there exists other universes?

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/The.20cardinal.20.60.23.28Type.20u.29.60/near/273266364 oh, we do have that #(Type u) < #(Type u + 1)

[Andrew Yang]

Type 0 is of type Type 1, so the latter is definitely bigger.

[Eric Rodriguez]

Andrew Yang said:

Type 0 is of type Type 1, so the latter is definitely bigger.

I don't think it's that simple, if you see the linked thread

[Andrew Yang]

Since Type 0 can be seen as a subtype of Type 1 by the embedding ulift, I interpreted your bigger as the inclusion being proper.

[Eric Rodriguez]

I meant that there's no surjective inclusion, full stop, not just the canonical inclusion