Attempt functions

def LO.FirstOrder.SetTheory.IsAttempt {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α f : V) : Prop

f is an attempt of length α for the function F, meaning that the domain of f is α, and for all β < α, it holds that f(β) = F (f ↾ β). The "attempt" terminology may be due to Paul Taylor.

Equations

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

theorem LO.FirstOrder.SetTheory.IsAttempt.definable {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} (hF : ℒₛₑₜ-function₁ F) : ℒₛₑₜ-relation IsAttempt F

Uniqueness of attempt functions

theorem LO.FirstOrder.SetTheory.IsAttempt.isAttempt_coherent {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) {α β : Ordinal V} {f g : V} [IsFunction f] [IsFunction g] (hf : IsAttempt F (↑α) f) (hg : IsAttempt F (↑β) g) (γ : Ordinal V) : ↑γ ⊆ ↑α ∧ ↑γ ⊆ ↑β → restrict f ↑γ = restrict g ↑γ

Any two attempt functions restrict to the same function.

Also see lemma 3.7 in chapter 2 of Frank Drake's Set Theory: An Introduction to Large Cardinals (Studies in Logic and the Foundations of Mathematics vol. 76, 1974).

theorem LO.FirstOrder.SetTheory.IsAttempt.isAttempt_unique {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {α : Ordinal V} {f g : V} [IsFunction f] [IsFunction g] (hf : IsAttempt F (↑α) f) (hg : IsAttempt F (↑α) g) : f = g

An attempt function of length α, if existing, is unique.

theorem LO.FirstOrder.SetTheory.IsAttempt.isAttempt_restrict_eq_of_le {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) {α β : Ordinal V} {f g : V} [IsFunction f] [IsFunction g] (hβα : β ≤ α) (hf : IsAttempt F (↑α) f) (hg : IsAttempt F (↑β) g) : restrict f ↑β = g

If β ≤ α, then an attempt function on α restricts to the attempt function on β.

Existence and choices of attempt functions

def LO.FirstOrder.SetTheory.IsAttempt.Exists {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α : V) : Prop

Existence of an attempt function of a given length.

Equations

• LO.FirstOrder.SetTheory.IsAttempt.Exists F α = ∃ (f : V), LO.FirstOrder.SetTheory.IsAttempt F α f

theorem LO.FirstOrder.SetTheory.IsAttempt.existsUnique_of_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α : V) (hex : Exists F α) : ∃! f : V, IsAttempt F α f

Exists implies ∃!.

theorem LO.FirstOrder.SetTheory.attemptOrEmpty_existsUnique {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α : V) : ∃! y : V, IsAttempt.Exists F α ∧ IsAttempt F α y ∨ ¬IsAttempt.Exists F α ∧ y = ∅

This lemma is originally by tosiaki.

noncomputable def LO.FirstOrder.SetTheory.attemptOrEmpty {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α : V) : V

An attempt of length α, or ∅ if one doesn't exist. This definition is by tosiaki.

Equations

• LO.FirstOrder.SetTheory.attemptOrEmpty F α = Classical.choose! ⋯

noncomputable def LO.FirstOrder.SetTheory.pairValueAttempt {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α : V) : V

A pair ⟨α, F f⟩ₖ of an ordinal α and the value of F on attemptOrEmpty F α. This is a technical definition needed for the proof of the transfinite recursion theorem.

Equations

• LO.FirstOrder.SetTheory.pairValueAttempt F α = ⟨α, F (LO.FirstOrder.SetTheory.attemptOrEmpty F α)⟩ₖ

theorem LO.FirstOrder.SetTheory.kpair_eq_pairValueAttempt_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {α x y : V} : ⟨x, y⟩ₖ = pairValueAttempt F α ↔ x = α ∧ y = F (attemptOrEmpty F α)

theorem LO.FirstOrder.SetTheory.eq_of_kpair_eq_pairValueAttempt {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {α x y : V} (h : ⟨x, y⟩ₖ = pairValueAttempt F α) : x = α

Constructing attempt functions using replacement

noncomputable def LO.FirstOrder.SetTheory.Replacement.replAttemptOrEmpty {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) : V → V

Function that outputs an attempt of length α, subject to the assumption that for all β < α, there is an attempt of length β. This is a big function constructed using replacement.

Equations

• LO.FirstOrder.SetTheory.Replacement.replAttemptOrEmpty F hF = LO.FirstOrder.SetTheory.repl (LO.FirstOrder.SetTheory.pairValueAttempt F) ⋯

@[simp]

theorem LO.FirstOrder.SetTheory.Replacement.mem_replAttemptOrEmpty_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α p : V) : p ∈ replAttemptOrEmpty F hF α ↔ ∃ β ∈ α, p = pairValueAttempt F β

@[simp]

theorem LO.FirstOrder.SetTheory.Replacement.kpair_mem_replAttemptOrEmpty_iff {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) {α : Ordinal V} {β y : V} : ⟨β, y⟩ₖ ∈ replAttemptOrEmpty F hF ↑α ↔ β ∈ ↑α ∧ ⟨β, y⟩ₖ = pairValueAttempt F β

theorem LO.FirstOrder.SetTheory.Replacement.domain_replAttemptOrEmpty_eq {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : domain (replAttemptOrEmpty F hF ↑α) = ↑α

instance LO.FirstOrder.SetTheory.Replacement.instIsFunctionReplAttemptOrEmptyVal {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : IsFunction (replAttemptOrEmpty F hF ↑α)

theorem LO.FirstOrder.SetTheory.Replacement.replAttemptOrEmpty_aux {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : IsAttempt F (↑α) (replAttemptOrEmpty F hF ↑α)

An auxiliary lemma about replAttemptOrEmpty.

theorem LO.FirstOrder.SetTheory.Replacement.attempt_function_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : IsAttempt.Exists F ↑α

For any ordinal α, there exists an attempt function of length α.

theorem LO.FirstOrder.SetTheory.Replacement.attemptOrEmpty_eq_replAttemptOrEmpty {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : attemptOrEmpty F ↑α = replAttemptOrEmpty F hF ↑α

noncomputable def LO.FirstOrder.SetTheory.Replacement.transfiniteRec {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : V) : V

Equations

• LO.FirstOrder.SetTheory.Replacement.transfiniteRec F hF α = if LO.FirstOrder.SetTheory.IsOrdinal α then F (LO.FirstOrder.SetTheory.Replacement.replAttemptOrEmpty F hF α) else ∅

instance LO.FirstOrder.SetTheory.Replacement.transfiniteRec_definable {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] {F : V → V} (hF : ℒₛₑₜ-function₁ F) : ℒₛₑₜ-function₁ transfiniteRec F hF

The transfinite recursion function is definable.

Characterization of the transfinite recursion: $R_F \alpha = F (R_F \upharpoonright \alpha)$

theorem LO.FirstOrder.SetTheory.Replacement.transfiniteRec_spec {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : transfiniteRec F hF ↑α = F (repl (fun (β : V) => ⟨β, transfiniteRec F hF β⟩ₖ) ⋯ ↑α)

theorem LO.FirstOrder.SetTheory.Replacement.transfiniteRec_spec_of_not_isOrdinal {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) {x : V} (hx : ¬IsOrdinal x) : transfiniteRec F hF x = ∅

The transfinite recursion function is empty outside the ordinals.