Universe levels and Russels Paradox

Stream: new members

[Jasper Ganten]

Hi everyone! I'm new to type theory and struggling to understand when and how Lean steps up universe levels beyond the basic maximum rule.
What I understand so far:

1. Generally, the universe of a type is the maximum of all universe levels in its construction

2. Type : Type is not allowed

3. Type u : Type (u+1)

4. Strict positivity prevents paradoxes in inductive types

What I'm confused about:

• Is Type u : Type (u+1) the only universe stepping rule, or are there others?

• How exactly does Lean detect when the simple "maximum rule" isn't sufficient (like with Russell's paradox)?

• When I define an inductive type, how does Lean determine it needs universe stepping beyond just looking at constructor argument types?

def Russell : Type (u+1) := {S : Type u // S ∉ S} still produces an error because of the 'membership relation' not being given...

[Matt Diamond]

I can't speak to the rest of your questions, but the problem with your Russell definition is that types don't have "members"... sets do

[Mr Proof]

Extra information:
In Lean we have:
Type u : Type (u+1)
and Prop:Type

but in other languages they use (I'm told) Agada/Idris?:
Type u : Type (u+1)
and Prop u : Prop (u+1)

and there's lots of other ways. So I think there is more than one way to have an infinite tower of types to avoid Russell Paradox.

[Matt Diamond]

@Jasper Ganten btw, Lean has an implementation of ZFC that allows you to define the Russell "set", but it's a Class (and in fact it's the universal Class):

import Mathlib

def Russell : Class := { S : ZFSet | S ∉ S }

example : ¬∃ (S : ZFSet), S = Russell :=
by
  intro ⟨S, hS⟩
  have not_mem_self : S ∉ S := S.mem_irrefl
  have mem_self : S ∈ S := by rwa [← Class.coe_apply, hS]
  exact not_mem_self mem_self

example : Russell = Class.univ := Class.eq_univ_of_forall ZFSet.mem_irrefl

[Jasper Ganten]

Thanks a lot - I think this already helps to build the intuition!