Model parameters

In this file, we define the parameters that we will use to construct our model of tangled type theory.

Parameters and examples

class ConNF.Params : Type (u + 1)

The type of model parameters. Specifically, we have:

• a nonempty type Λ with a relation < that well-orders it, and gives it no maximal element;
• a type κ whose cardinality is regular and strictly greater than ℵ₀;
• a type μ whose cardinality is a strong limit, strictly greater than κ, and has cofinality at least the cardinality of κ and at least the order type of Λ.

We write #α for the cardinality of any type α.

Λ will become our sort of type indices in the final model we build. That is, in our type hierarchy, each inhabitant α : Λ will give rise to a type TSet α (read "tangled sets of type α"). The element-of relation will be of type {α : Λ} → {β : Λ} → β < α → TSet β → TSet α → Prop; that is, given a proof that β < α, and given sets x : TSet β and y : TSet α, we have a proposition that asks if x is an element of y.

κ will be a type that delimits "small" sets from "large" sets. By manipulating "large" data, but only allowing sufficiently "small" things in our model, we will be able to control what the model is able to know about itself.

μ will be the size of each of our type levels TSet α. The main technical challenge of the proof will be to prove this cardinality bound on the sizes of our types. We will not be able to construct TSet α until we have already verified that TSet β has cardinality #μ for every β < α.

Our model parameters are not just cardinals (or ordinals): they are types with the given cardinalities and properties. By doing this, the set-theoretic elements of (for example) #μ correspond directly to inhabitants of the type μ.

Note that we use a capital Λ instead of a lowercase λ as the latter is reserved for anonymous functions in Lean's syntax.

This structure is registered as a typeclass. This means that, at the start of a file, we can write variable [Params.{u}] to parametrise definitions in our file by a choice of model parameters, and whenever a definition or theorem involving model parameters is mentioned, Lean will implicitly assume that we intended this particular set of model parameters without having to write it ourselves.

Finally, note that our model parameters are parametric over a universe u. We will almost never deal with universe levels in the proof (and in fact we can set u = 0 without issue), but this gives us greater generality for almost no cost.

• Λ : Type u
• κ : Type u
• μ : Type u
• Λ_nonempty : Nonempty ConNF.Λ
• ΛWellOrder : LtWellOrder ConNF.Λ
• Λ_noMaxOrder : NoMaxOrder ConNF.Λ
• aleph0_lt_κ : Cardinal.aleph0 < Cardinal.mk ConNF.κ
• κ_isRegular : (Cardinal.mk ConNF.κ).IsRegular
• μ_isStrongLimit : (Cardinal.mk ConNF.μ).IsStrongLimit
• κ_lt_μ : Cardinal.mk ConNF.κ < Cardinal.mk ConNF.μ
• κ_le_μ_ord_cof : Cardinal.mk ConNF.κ ≤ (Cardinal.mk ConNF.μ).ord.cof
• Λ_type_le_μ_ord_cof : (Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2) ≤ (Cardinal.mk ConNF.μ).ord.cof.ord

def ConNF.Params.minimal : ConNF.Params

The smallest collection of model parameters that we can prove to exist. Importantly, ZFC (with no inaccessibles) proves that this is a set of model parameters. We take Λ = ω, κ = ω₁, μ = ב_ω₁ (of course, up to identification of cardinals and ordinals with their representative types).

Equations

• One or more equations did not get rendered due to their size.

def ConNF.Params.inaccessible : ConNF.Params

We can also instantiate our model parameters with Λ = μ. To do this, both #Λ and #μ will need to be inaccessible cardinals. We simply pick κ = ω₁ for convenience.

Equations

• One or more equations did not get rendered due to their size.

We now inform Lean that our model parameters should be accessible from the names Λ, κ, etc. instead of the longer Params.Λ and so on.

Assume a set of model parameters.

Elementary properties

We now establish the most basic elementary properties about Λ, κ, and μ. In particular, we will use choice to create well-orderings on κ and μ whose order types are initial, and then prove some basic facts about these orders.

theorem ConNF.instNonemptyΛ [ConNF.Params] : Nonempty ConNF.Λ

instance ConNF.instLtWellOrderΛ [ConNF.Params] : LtWellOrder ConNF.Λ

Equations

• ConNF.instLtWellOrderΛ = ConNF.Params.ΛWellOrder

theorem ConNF.instNoMaxOrderΛ [ConNF.Params] : NoMaxOrder ConNF.Λ

instance ConNF.instWellFoundedRelationΛ [ConNF.Params] : WellFoundedRelation ConNF.Λ

This gadget allows us to use termination_by clauses with Λ, which gives us access to more complicated recursion and induction along Λ.

Equations

• ConNF.instWellFoundedRelationΛ = { rel := fun (x1 x2 : ConNF.Λ) => x1 < x2, wf := ⋯ }

Basic cardinal inequalities between ℵ₀, Λ, κ, μ.

theorem ConNF.aleph0_lt_μ [ConNF.Params] : Cardinal.aleph0 < Cardinal.mk ConNF.μ

theorem ConNF.aleph0_lt_μ_ord_cof [ConNF.Params] : Cardinal.aleph0 < (Cardinal.mk ConNF.μ).ord.cof

theorem ConNF.Λ_type_le_μ_ord [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2) ≤ (Cardinal.mk ConNF.μ).ord

theorem ConNF.Λ_le_cof_μ [ConNF.Params] : Cardinal.mk ConNF.Λ ≤ (Cardinal.mk ConNF.μ).ord.cof

theorem ConNF.Λ_le_μ [ConNF.Params] : Cardinal.mk ConNF.Λ ≤ Cardinal.mk ConNF.μ

theorem ConNF.κ_le_μ [ConNF.Params] : Cardinal.mk ConNF.κ ≤ Cardinal.mk ConNF.μ

We now construct the aforementioned well-orders on κ and μ.

@[irreducible]

def ConNF.κEquiv [ConNF.Params] : ConNF.κ ≃ ↑(Set.Iio (Cardinal.mk ConNF.κ).ord)

Equations

• ConNF.κEquiv = Equiv.ulift.symm.trans ⋯.some

@[irreducible]

def ConNF.μEquiv [ConNF.Params] : ConNF.μ ≃ ↑(Set.Iio (Cardinal.mk ConNF.μ).ord)

Equations

• ConNF.μEquiv = Equiv.ulift.symm.trans ⋯.some

instance ConNF.instLtWellOrderκ [ConNF.Params] : LtWellOrder ConNF.κ

Equations

• ConNF.instLtWellOrderκ = ConNF.κEquiv.ltWellOrder

theorem ConNF.instNoMaxOrderκ [ConNF.Params] : NoMaxOrder ConNF.κ

instance ConNF.instOfNatκ [ConNF.Params] (n : ℕ) : OfNat ConNF.κ n

We overload Lean's numeric literal syntax so that numbers such as 0 can also be interpreted as particular inhabitants of κ. We could do this for the other cardinal parameters as well, but we don't need it.

Equations

• ConNF.instOfNatκ n = ConNF.κEquiv.ofNat n

instance ConNF.instLtWellOrderμ [ConNF.Params] : LtWellOrder ConNF.μ

Equations

• ConNF.instLtWellOrderμ = ConNF.μEquiv.ltWellOrder

theorem ConNF.instNoMaxOrderμ [ConNF.Params] : NoMaxOrder ConNF.μ

theorem ConNF.instInfiniteΛ [ConNF.Params] : Infinite ConNF.Λ

theorem ConNF.instInfiniteκ [ConNF.Params] : Infinite ConNF.κ

theorem ConNF.instInfiniteμ [ConNF.Params] : Infinite ConNF.μ

theorem ConNF.Λ_type_isLimit [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2).IsLimit

@[simp]

theorem ConNF.κ_type [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.κ) => x1 < x2) = (Cardinal.mk ConNF.κ).ord

The order type on κ really is the initial ordinal for the cardinal #κ.

@[simp]

theorem ConNF.μ_type [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.μ) => x1 < x2) = (Cardinal.mk ConNF.μ).ord

instance ConNF.instAddMonoidκ [ConNF.Params] : AddMonoid ConNF.κ

We define a monoid structure on κ, denoted +, by passing to the collection of ordinals below (#κ).ord and then computing their sum.

Equations

• ConNF.instAddMonoidκ = ConNF.κEquiv.addMonoid

instance ConNF.instSubκ [ConNF.Params] : Sub ConNF.κ

Equations

• ConNF.instSubκ = ConNF.κEquiv.sub

Basic properties about the order and operations on κ.

theorem ConNF.κ_ofNat_def [ConNF.Params] (n : ℕ) : OfNat.ofNat n = ConNF.κEquiv.symm (OfNat.ofNat n)

theorem ConNF.κ_add_def [ConNF.Params] (x y : ConNF.κ) : x + y = ConNF.κEquiv.symm (ConNF.κEquiv x + ConNF.κEquiv y)

theorem ConNF.κ_sub_def [ConNF.Params] (x y : ConNF.κ) : x - y = ConNF.κEquiv.symm (ConNF.κEquiv x - ConNF.κEquiv y)

theorem ConNF.κEquiv_ofNat [ConNF.Params] (n : ℕ) : ↑(ConNF.κEquiv (OfNat.ofNat n)) = ↑n

theorem ConNF.κEquiv_add [ConNF.Params] (x y : ConNF.κ) : ↑(ConNF.κEquiv (x + y)) = ↑(ConNF.κEquiv x) + ↑(ConNF.κEquiv y)

theorem ConNF.κEquiv_sub [ConNF.Params] (x y : ConNF.κ) : ↑(ConNF.κEquiv (x - y)) = ↑(ConNF.κEquiv x) - ↑(ConNF.κEquiv y)

theorem ConNF.κEquiv_lt [ConNF.Params] (x y : ConNF.κ) : x < y ↔ ConNF.κEquiv x < ConNF.κEquiv y

theorem ConNF.κEquiv_le [ConNF.Params] (x y : ConNF.κ) : x ≤ y ↔ ConNF.κEquiv x ≤ ConNF.κEquiv y

theorem ConNF.κ_zero_le [ConNF.Params] (x : ConNF.κ) : 0 ≤ x

theorem ConNF.instCovariantClassκHAddLe [ConNF.Params] : CovariantClass ConNF.κ ConNF.κ (fun (x1 x2 : ConNF.κ) => x1 + x2) fun (x1 x2 : ConNF.κ) => x1 ≤ x2

theorem ConNF.instCovariantClassκHAddLt [ConNF.Params] : CovariantClass ConNF.κ ConNF.κ (fun (x1 x2 : ConNF.κ) => x1 + x2) fun (x1 x2 : ConNF.κ) => x1 < x2

theorem ConNF.instCovariantClassκSwapHAddLe [ConNF.Params] : CovariantClass ConNF.κ ConNF.κ (Function.swap fun (x1 x2 : ConNF.κ) => x1 + x2) fun (x1 x2 : ConNF.κ) => x1 ≤ x2

theorem ConNF.κ_le_add [ConNF.Params] (x y : ConNF.κ) : x ≤ x + y

theorem ConNF.instIsLeftCancelAddκ [ConNF.Params] : IsLeftCancelAdd ConNF.κ

theorem ConNF.κ_typein [ConNF.Params] (x : ConNF.κ) : (Ordinal.typein fun (x1 x2 : ConNF.κ) => x1 < x2).toRelEmbedding x = ↑(ConNF.κEquiv x)

theorem ConNF.κ_card_Iio_eq [ConNF.Params] (x : ConNF.κ) : Cardinal.mk ↑{y : ConNF.κ | y < x} = (↑(ConNF.κEquiv x)).card

theorem ConNF.μ_card_Iio_lt [ConNF.Params] (ν : ConNF.μ) : Cardinal.mk ↑{ξ : ConNF.μ | ξ < ν} < Cardinal.mk ConNF.μ

theorem ConNF.μ_card_Iic_lt [ConNF.Params] (ν : ConNF.μ) : Cardinal.mk ↑{ξ : ConNF.μ | ξ ≤ ν} < Cardinal.mk ConNF.μ

theorem ConNF.μ_bounded_lt_of_lt_μ_ord_cof [ConNF.Params] (s : Set ConNF.μ) (h : Cardinal.mk ↑s < (Cardinal.mk ConNF.μ).ord.cof) : Set.Bounded (fun (x1 x2 : ConNF.μ) => x1 < x2) s

A set in μ that is smaller than the cofinality of μ is bounded.

theorem ConNF.card_lt_of_μ_bounded [ConNF.Params] (s : Set ConNF.μ) (h : Set.Bounded (fun (x1 x2 : ConNF.μ) => x1 < x2) s) : Cardinal.mk ↑s < Cardinal.mk ConNF.μ

A partial converse to the previous theorem: a bounded set in μ must have cardinality smaller than μ itself.