Attempt functions

def FFL.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

• FFL.FirstOrder.SetTheory.IsAttempt F f = (FFL.FirstOrder.SetTheory.Seq f ∧ ∀ β ∈ FFL.FirstOrder.SetTheory.lh f, ∀ (y : V), ⟨β, y⟩ₖ ∈ f ↔ y = F (FFL.FirstOrder.SetTheory.restrict f β))

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

Uniqueness of attempt functions

theorem FFL.FirstOrder.SetTheory.IsAttempt.isAttempt_coherent {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {α β : Ordinal V} {f g : V} (hf : IsAttempt F f) (hg : IsAttempt F g) (hdomf : lh f = ↑α) (hdomg : lh 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 FFL.FirstOrder.SetTheory.IsAttempt.isAttempt_unique {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {α : Ordinal V} {f g : V} (hf : IsAttempt F f) (hg : IsAttempt F g) (hlhf : lh f = ↑α) (hlhg : lh g = ↑α) : f = g

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

theorem FFL.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} (hβα : β ≤ α) (hf : IsAttempt F f) (hg : IsAttempt F g) (hlhf : lh f = ↑α) (hlhg : lh g = ↑β) : restrict f ↑β = g

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

theorem FFL.FirstOrder.SetTheory.IsAttempt.eq_of_isAttempt {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {f g : V} (hf : IsAttempt F f) (hg : IsAttempt F g) {γ : Ordinal V} {y₁ y₂ : V} : ⟨↑γ, y₁⟩ₖ ∈ f → ⟨↑γ, y₂⟩ₖ ∈ g → y₁ = y₂

Various facts about attempt functions

theorem FFL.FirstOrder.SetTheory.IsAttempt.initial {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {f : V} (hf : IsAttempt F f) (hlh : ∅ ∈ lh f) : ⟨∅, F ∅⟩ₖ ∈ f

theorem FFL.FirstOrder.SetTheory.IsAttempt.successor {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] {F : V → V} {f : V} (hf : IsAttempt F f) : IsAttempt F (f ⁀' F f)

Existence and choices of attempt functions

def FFL.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

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

theorem FFL.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 ∧ lh f = α

Exists implies ∃!.

theorem FFL.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 ∧ lh y = α) ∧ (¬IsAttempt.Exists F α → y = ∅)

This lemma is originally by tosiaki.

noncomputable def FFL.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

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

theorem FFL.FirstOrder.SetTheory.isAttempt_attemptOrEmpty_of_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α : V) (hexists : IsAttempt.Exists F α) : IsAttempt F (attemptOrEmpty F α)

theorem FFL.FirstOrder.SetTheory.lh_attemptOrEmpty_eq_of_exists {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] (F : V → V) (α : V) (hexists : IsAttempt.Exists F α) : lh (attemptOrEmpty F α) = α

noncomputable def FFL.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

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

theorem FFL.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 FFL.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 FFL.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

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

@[simp]

theorem FFL.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 FFL.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 β

@[simp]

theorem FFL.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 FFL.FirstOrder.SetTheory.Replacement.isFunction_replAttemptOrEmpty {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : IsFunction (replAttemptOrEmpty F hF ↑α)

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

@[simp]

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

theorem FFL.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 FFL.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 FFL.FirstOrder.SetTheory.Replacement.isAttempt_attemptOrEmpty {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : Ordinal V) : IsAttempt F (attemptOrEmpty F ↑α)

@[simp]

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

theorem FFL.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 FFL.FirstOrder.SetTheory.Replacement.transfiniteRec {V : Type u_1} [SetStructure V] [Nonempty V] [V↓[ℒₛₑₜ] ⊧* 𝗭] [V↓[ℒₛₑₜ] ⊧* 𝗭𝗙] (F : V → V) (hF : ℒₛₑₜ-function₁ F) (α : V) : V

Equations

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

instance FFL.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 FFL.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 FFL.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.