The Kunen inconsistency theorem

This module proves the Kunen inconsistency theorem: there is no nontrivial elementary embedding of the universe of sets into itself.

def SetTheory.IsOmegaJonssonFunc {M₀ : Type 1} [ZFStructure M₀] [IsVonNeumannWithOmega M₀] (f κ : M₀) : Prop

The IsOmegaJonssonFunc declaration.

Equations

• SetTheory.IsOmegaJonssonFunc f κ = (f ∈ SetTheory.Func (SetTheory.Func SetTheory.ωₘ κ) κ ∧ ∀ X ⊆ κ, SetTheory.cardEq X κ → ∀ α ∈ κ, ∃ s ∈ SetTheory.Func SetTheory.ωₘ X, SetTheory.apply f s = α)

theorem SetTheory.IsOmegaJonssonFunc.to_realize {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumannWithOmega M] (x₁ x₂ : M) : IsOmegaJonssonFunc x₁ x₂ ↔ FirstOrder.Language.Formula.Realize formula ![x₁, x₂]

theorem SetTheory.IsOmegaJonssonFunc.elementarity {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumannWithOmega M] {N : Type 1} [sN : ZFStructure N] [cN₁ : IsVonNeumannWithOmega N] (x₁ x₂ : M) {F : Type u_1} [FunLike F M N] [ElementaryEmbeddingClass F M N] (j : F) : IsOmegaJonssonFunc (j x₁) (j x₂) ↔ IsOmegaJonssonFunc x₁ x₂

theorem SetTheory.IsOmegaJonssonFunc.realize_iff {M : Type 1} [sM : ZFStructure M] [cM₁ : IsVonNeumannWithOmega M] (v✝ : Fin 2 → M) : FirstOrder.Language.Formula.Realize formula v✝ ↔ IsOmegaJonssonFunc (v✝ 0) (v✝ 1)

class SetTheory.KunenBoundParams : Type 2

The KunenBoundParams type.

• M : Type 1

  The M declaration.

• structureM : ZFStructure M

  The structureM declaration.

• isVonNeumann : IsVonNeumann M

  The isVonNeumann declaration.

• j : NontrivialElementaryEmbedding M

  The j declaration.

• bddAbove_crit_iter : BddAbove (Set.range fun (x : ℕ) => (⇑j)^[x] (crit j))

@[implicit_reducible]

instance SetTheory.KunenBoundParams.instZFStructureM [KunenBoundParams] : ZFStructure M

Equations

• SetTheory.KunenBoundParams.instZFStructureM = SetTheory.KunenBoundParams.structureM

@[implicit_reducible]

instance SetTheory.KunenBoundParams.instIsVonNeumannWithOmegaM [KunenBoundParams] : IsVonNeumannWithOmega M

Equations

• SetTheory.KunenBoundParams.instIsVonNeumannWithOmegaM = SetTheory.hasOmegaOfNontrivialSelfEmbedding SetTheory.KunenBoundParams.j

noncomputable def SetTheory.KunenBoundParams.κ [KunenBoundParams] (n : ℕ) : M

The κ declaration.

Equations

• SetTheory.KunenBoundParams.κ n = (⇑SetTheory.KunenBoundParams.j)^[n] (SetTheory.crit SetTheory.KunenBoundParams.j)

noncomputable def SetTheory.KunenBoundParams.κω [KunenBoundParams] : M

The κω declaration.

Equations

• SetTheory.KunenBoundParams.κω = ⨆ (n : ℕ), SetTheory.KunenBoundParams.κ n

def SetTheory.KunenBoundParams.κωEquinumerousSubsets [KunenBoundParams] : Type 1

The κωEquinumerousSubsets declaration.

Equations

• SetTheory.KunenBoundParams.κωEquinumerousSubsets = { x : SetTheory.KunenBoundParams.M // x ⊆ SetTheory.KunenBoundParams.κω ∧ Cardinal.mk ↥x = Cardinal.mk ↥SetTheory.KunenBoundParams.κω }

noncomputable def SetTheory.KunenBoundParams.ν [KunenBoundParams] : Ordinal.{1}

The ν declaration.

Equations

• SetTheory.KunenBoundParams.ν = (Cardinal.mk (↥SetTheory.KunenBoundParams.κω × SetTheory.KunenBoundParams.κωEquinumerousSubsets)).ord

noncomputable def SetTheory.KunenBoundParams.γX [KunenBoundParams] : ν.ToType ≃ ↥κω × κωEquinumerousSubsets

The γX declaration.

Equations

• SetTheory.KunenBoundParams.γX = ⋯.some

noncomputable def SetTheory.KunenBoundParams.γ [KunenBoundParams] (α : ν.ToType) : M

The γ declaration.

Equations

• SetTheory.KunenBoundParams.γ α = ↑(SetTheory.KunenBoundParams.γX α).1

noncomputable def SetTheory.KunenBoundParams.X [KunenBoundParams] (α : ν.ToType) : M

The X declaration.

Equations

• SetTheory.KunenBoundParams.X α = ↑(SetTheory.KunenBoundParams.γX α).2

theorem SetTheory.KunenBoundParams.γ_mem_κω [KunenBoundParams] (α : ν.ToType) : γ α ∈ κω

theorem SetTheory.KunenBoundParams.X_subset_κω [KunenBoundParams] (α : ν.ToType) : X α ⊆ κω

theorem SetTheory.KunenBoundParams.card_X_eq_card_κω [KunenBoundParams] (α : ν.ToType) : Cardinal.mk ↥(X α) = Cardinal.mk ↥κω

theorem SetTheory.KunenBoundParams.card_ωₘ [KunenBoundParams] : Cardinal.mk ↥ωₘ = Cardinal.aleph0

def SetTheory.KunenBoundParams.injSubset [KunenBoundParams] {A B : M} (hsub : A ⊆ B) : ↥A ↪ ↥B

The injSubset declaration.

Equations

• SetTheory.KunenBoundParams.injSubset hsub = { toFun := fun (x : ↥A) => match x with | ⟨x, hx⟩ => ⟨x, ⋯⟩, inj' := ⋯ }

theorem SetTheory.KunenBoundParams.card_le_of_sub [KunenBoundParams] {A B : M} (hsub : A ⊆ B) : Cardinal.mk ↥A ≤ Cardinal.mk ↥B

theorem SetTheory.KunenBoundParams.bddAbove_ordinal_κ [KunenBoundParams] : BddAbove (Set.range fun (n : ℕ) => ⟨κ n, ⋯⟩)

theorem SetTheory.KunenBoundParams.κω_eq_ordinal_sSup [KunenBoundParams] : κω = ↑(⨆ (n : ℕ), ⟨κ n, ⋯⟩)

theorem SetTheory.KunenBoundParams.κ_mem_κω [KunenBoundParams] (n : ℕ) : κ n ∈ κω

theorem SetTheory.KunenBoundParams.κ_le_κω [KunenBoundParams] (n : ℕ) : κ n ≤ κω

theorem SetTheory.KunenBoundParams.aleph0_le_κω [KunenBoundParams] : Cardinal.aleph0 ≤ Cardinal.mk ↥κω

noncomputable def SetTheory.KunenBoundParams.i [KunenBoundParams] {n : ℕ} : ↥𝓟 (κ n) ↪ ↥κω

The i declaration.

Equations

• SetTheory.KunenBoundParams.i = ⋯.some

@[simp]

theorem SetTheory.KunenBoundParams.inter_sub_left [KunenBoundParams] {x y : M} : x ∩ y ⊆ x

@[simp]

theorem SetTheory.KunenBoundParams.inter_sub_right [KunenBoundParams] {x y : M} : x ∩ y ⊆ y

theorem SetTheory.KunenBoundParams.isOrdinal_κω [KunenBoundParams] : IsOrdinal κω

theorem SetTheory.KunenBoundParams.exists_lt_κ [KunenBoundParams] {α : M} (hα : α ∈ κω) : ∃ (n : ℕ), α < κ n

theorem SetTheory.KunenBoundParams.card_κωEquinumerousSubsets_le [KunenBoundParams] : Cardinal.mk κωEquinumerousSubsets ≤ Cardinal.mk ↥κω ^ Cardinal.aleph0

instance SetTheory.KunenBoundParams.instNonemptySubtypeMMemκω [KunenBoundParams] : Nonempty ↥κω

instance SetTheory.KunenBoundParams.instNonemptyκωEquinumerousSubsets [KunenBoundParams] : Nonempty κωEquinumerousSubsets

instance SetTheory.KunenBoundParams.instNonemptyToTypeν [KunenBoundParams] : Nonempty ν.ToType

@[irreducible]

def SetTheory.KunenBoundParams.s [KunenBoundParams] (α : ν.ToType) : ℕ → ↥κω

The s declaration.

Equations

• SetTheory.KunenBoundParams.s α = ⋯.some

theorem SetTheory.KunenBoundParams.injective_s [KunenBoundParams] : Function.Injective s

theorem SetTheory.KunenBoundParams.s_mem_X [KunenBoundParams] (α : ν.ToType) (n : ℕ) : ↑(s α n) ∈ X α

noncomputable def SetTheory.KunenBoundParams.f [KunenBoundParams] (x : ℕ → ↥κω) : ↥κω

The f declaration.

Equations

• SetTheory.KunenBoundParams.f x = ⟨SetTheory.KunenBoundParams.γ (Function.invFun SetTheory.KunenBoundParams.s x), ⋯⟩

noncomputable def SetTheory.KunenBoundParams.fSet [KunenBoundParams] : M

The fSet declaration.

Equations

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

theorem SetTheory.KunenBoundParams.fSet_mem [KunenBoundParams] : fSet ∈ Func (Func ωₘ κω) κω

theorem SetTheory.KunenBoundParams.funcToSet_subset [KunenBoundParams] {A B C : M} {f : ↥A → ↥B} (hsub : B ⊆ C) : funcToSet f = funcToSet (⇑(injSubset hsub) ∘ f)

theorem SetTheory.KunenBoundParams.funcToSet_mem_Func_of_subset [KunenBoundParams] {A B C : M} {f : ↥A → ↥B} (hsub : B ⊆ C) : funcToSet f ∈ Func A C

theorem SetTheory.KunenBoundParams.exists_γ_and_X_eq [KunenBoundParams] {β H : M} (hβ : β ∈ κω) (hH : H ⊆ κω) (card_eq : Cardinal.mk ↥H = Cardinal.mk ↥κω) : ∃ (α : ν.ToType), γ α = β ∧ X α = H

theorem SetTheory.KunenBoundParams.f_s_eq_γ [KunenBoundParams] {α : ν.ToType} : ↑(f (s α)) = γ α

theorem SetTheory.KunenBoundParams.is_omega_jonsson_fSet [KunenBoundParams] : IsOmegaJonssonFunc fSet κω

noncomputable def SetTheory.KunenBoundParams.κFunc [KunenBoundParams] (n : ℕ) : ↥κω

The κFunc declaration.

Equations

• SetTheory.KunenBoundParams.κFunc n = ⟨SetTheory.KunenBoundParams.κ n, ⋯⟩

noncomputable def SetTheory.KunenBoundParams.κFuncSet [KunenBoundParams] : M

The κFuncSet declaration.

Equations

• SetTheory.KunenBoundParams.κFuncSet = SetTheory.funcToSet (SetTheory.KunenBoundParams.κFunc ∘ ⇑SetTheory.omegaEquiv)

theorem SetTheory.KunenBoundParams.iUnion_κ_funcSet_eq [KunenBoundParams] : iUnion κFuncSet = κω

theorem SetTheory.KunenBoundParams.j_κFuncSet [KunenBoundParams] : j κFuncSet = funcToSet (κFunc ∘ Nat.succ ∘ ⇑omegaEquiv)

theorem SetTheory.KunenBoundParams.j_κω [KunenBoundParams] : j κω = κω

noncomputable def SetTheory.KunenBoundParams.H [KunenBoundParams] : M

The H declaration.

Equations

• SetTheory.KunenBoundParams.H = SetTheory.separate SetTheory.KunenBoundParams.κω fun (x : SetTheory.KunenBoundParams.M) => x ∈ Set.range ⇑SetTheory.KunenBoundParams.j

theorem SetTheory.KunenBoundParams.coeSort_H_iff [KunenBoundParams] : ↥H = ↑(⇑j '' ↑κω)

theorem SetTheory.KunenBoundParams.crit_in_range_j_f [KunenBoundParams] : ∃ x ∈ Func ωₘ H, apply (j fSet) x = κ 0

theorem SetTheory.KunenBoundParams.crit_not_in_range_j_f [KunenBoundParams] (x : M) : x ∈ Func ωₘ H → apply (j fSet) x ≠ κ 0

theorem SetTheory.KunenBoundParams.kunen_inconsistency [KunenBoundParams] : False

theorem SetTheory.kunen_inconsistency_vonNeumann (μ : Ordinal.{0}) [Fact (Order.IsSuccLimit μ)] (j : NontrivialElementaryEmbedding ↥(ZFSet.vonNeumann μ)) : ⨆ (n : ℕ), toOrdinal ⟨(⇑j)^[n] (crit j), ⋯⟩ = μ

theorem SetTheory.kunen_inconsistency_V (j : 𝓛ZF.ElementaryEmbedding V V) : j = FirstOrder.Language.ElementaryEmbedding.refl 𝓛ZF V