@[reducible, inline]

abbrev Model.toTail.World {κ : Type u_1} {α : Type u_2} [Nonempty κ] (M : Model κ α) : Type u_1

Worlds of the tail model: the original worlds plus a chain indexed by ℕ∞.

Equations

• Model.toTail.World M = (M.World ⊕ ℕ∞)

@[reducible, inline]

abbrev Model.toTail {κ : Type u_1} {α : Type u_2} [Nonempty κ] (M : Model κ α) (tail : M.World) : RootedModel (toTail.World M) α

Equations

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

@[reducible, inline]

abbrev Model.toTail.embed {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} (x : M.World) : (M.toTail tail).World

The embedding of a world of the original model M into the tail model M.toTail tail.

Equations

• Model.toTail.embed x = Sum.inl x

@[reducible, inline]

abbrev Model.toTail.chainPoint {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} (i : ℕ∞) : (M.toTail tail).World

The world in the chain attached above tail, indexed by i : ℕ∞ (⊤ is the tail model's own root).

Equations

• Model.toTail.chainPoint i = Sum.inr i

@[simp]

theorem Model.toTail.root_eq {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} : ↑(M.toTail tail).root = toTail.chainPoint ⊤

@[simp]

theorem Model.toTail.rel_embed_embed {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail x y : M.World} : toTail.embed x ≺ toTail.embed y ↔ x ≺ y

@[simp]

theorem Model.toTail.not_rel_embed_chainPoint {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail x : M.World} {i : ℕ∞} : ¬toTail.embed x ≺ toTail.chainPoint i

@[simp]

theorem Model.toTail.rel_chainPoint_embed {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} {i : ℕ∞} {x : M.World} : toTail.chainPoint i ≺ toTail.embed x

@[simp]

theorem Model.toTail.rel_chainPoint_chainPoint {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} {i j : ℕ∞} : toTail.chainPoint i ≺ toTail.chainPoint j ↔ j < i

instance Model.toTail.instIsTransWorldWorldRel {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} [IsTrans M.World Rel] : IsTrans (M.toTail tail).World Rel

instance Model.toTail.instIrreflWorldWorldRel {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} [Std.Irrefl Rel] : Std.Irrefl Rel

@[reducible, inline]

abbrev Model.toTail.chain {κ : Type u_1} {α : Type u_2} [Nonempty κ] (M : Model κ α) (tail : M.World) : ℕ+ → (M.toTail tail).World

The chain of ℕ∞-worlds attached above tail.

Equations

• Model.toTail.chain M tail n = Model.toTail.chainPoint ↑↑n

@[simp]

theorem Model.toTail.chain_isChain {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} {i j : ℕ+} (h : i < j) : toTail.chain M tail j ≺ toTail.chain M tail i

instance Model.toTail.instIsConverseWellFoundedWorldWorldRel {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} [IsConverseWellFounded M.World Rel] : IsConverseWellFounded (M.toTail tail).World Rel

instance Model.toTail.instIsGLWorld {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail : M.World} [M.IsGL] : (M.toTail tail).IsGL

def Model.toTail.pMorphismOriginal {κ : Type u_1} {α : Type u_2} [Nonempty κ] (M : Model κ α) (tail : M.World) : M →ₚ (M.toTail tail).toModel

The embedding of the original model into the tail model is a p-morphism.

Equations

• Model.toTail.pMorphismOriginal M tail = { toFun := Model.toTail.embed, forth := ⋯, back := ⋯, atomic := ⋯ }

theorem Model.toTail.modal_equivalent_original {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {tail x : M.World} : x ↭ toTail.embed x

theorem Model.toTail.forces_inl {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {A : Formula α} {tail x : M.World} : toTail.embed x ⊩[(M.toTail tail).toModel] A ↔ x ⊩[M] A

At an original-model world (embed x), forcing in the tail model agrees with forcing in the original model.

theorem Model.toTail.forces_nat_box_antitone {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {A : Formula α} {tail : M.World} {m n : ℕ} (hmn : m ≤ n) (h : toTail.chainPoint ↑n ⊩[(M.toTail tail).toModel] □A) : toTail.chainPoint ↑m ⊩[(M.toTail tail).toModel] □A

Forcing of □A is downward closed on the chain: if it holds at chainPoint n, it also holds at any chainPoint m below it.

theorem Model.toTail.forces_nat_eventually_stable {κ : Type u_2} {α : Type u_1} [Nonempty κ] {M : Model κ α} {tail : M.World} (A : Formula α) : ∃ (k : ℕ), ∀ (n : ℕ), k ≤ n → (toTail.chainPoint ↑n ⊩[(M.toTail tail).toModel] A ↔ toTail.chainPoint ↑k ⊩[(M.toTail tail).toModel] A)

Forcing at chain points (chainPoint n) eventually stabilizes as n grows.

theorem Model.toTail.forces_nat_eventually_root {κ : Type u_2} {α : Type u_1} [Nonempty κ] {M : Model κ α} {tail : M.World} (A : Formula α) : ∃ (k : ℕ), ∀ (n : ℕ), k ≤ n → (toTail.chainPoint ↑n ⊩[(M.toTail tail).toModel] A ↔ toTail.chainPoint ⊤ ⊩[(M.toTail tail).toModel] A)

Forcing at chain points (chainPoint n) eventually stabilizes, as n grows, to the forcing value at the tail model's own root (chainPoint ⊤).

theorem Model.toTail.tailLemma {κ : Type u_2} {α : Type u_1} [Nonempty κ] {M : Model κ α} {tail : M.World} (A : Formula α) : toTail.chainPoint ⊤ ⊩[(M.toTail tail).toModel] A ↔ ∃ (k : ℕ), ∀ (n : ℕ), k ≤ n → toTail.chainPoint ↑n ⊩[(M.toTail tail).toModel] A

Tail Lemma (Visser1984 Lemma 2.2): A is forced at the tail model's own root (chainPoint ⊤) iff A is eventually forced along the chain (chainPoint n for all sufficiently large n).

theorem Model.toTail.root_forces_iff_forces_nat {κ : Type u_2} {α : Type u_1} [Nonempty κ] [DecidableEq α] {M : RootedModel κ α} [IsTrans M.World Rel] {Γ : FormulaFinset α} (Γclosed : ∀ B ∈ Γ, B.subfmls ⊆ Γ) (hΓ : ∀ B ∈ Γ.prebox, ↑M.root ⊩[M.toModel] □B 🡒 B) (B : Formula α) : B ∈ Γ → ∀ (n : ℕ), ↑M.root ⊩[M.toModel] B ↔ toTail.chainPoint ↑n ⊩[(M.toTail ↑M.root).toModel] B

If Γ is closed under subformulas and the root forces □B 🡒 B for every □B ∈ Γ, then forcing of every formula in Γ at the root agrees with forcing at every chain point (chainPoint n).

theorem Model.forces_toTail_reindex_iff {κ : Type u_2} {α : Type u_3} [Nonempty κ] {M : Model κ α} {A : Formula α} {κ' : Type u_1} [Nonempty κ'] {tail : M.World} {e : κ ≃ κ'} {x : (M.toTail tail).World} : Sum.map (⇑e) id x ⊩[((M.reindex e).toTail (e tail)).toModel] A ↔ x ⊩[(M.toTail tail).toModel] A

Re-indexing the base model along e does not change the tail construction, up to transporting the worlds by Sum.map e id. This is routine infrastructure with no counterpart in the literature.

theorem Model.forces_toTail_reindex_chainPoint_iff {κ : Type u_3} {α : Type u_2} [Nonempty κ] {M : Model κ α} {A : Formula α} {κ' : Type u_1} [Nonempty κ'] {tail : M.World} {e : κ ≃ κ'} {i : ℕ∞} : toTail.chainPoint i ⊩[((M.reindex e).toTail (e tail)).toModel] A ↔ toTail.chainPoint i ⊩[(M.toTail tail).toModel] A

theorem Model.forces_toTail_reindex_root_iff {κ : Type u_3} {α : Type u_2} [Nonempty κ] {M : Model κ α} {A : Formula α} {κ' : Type u_1} [Nonempty κ'] {tail : M.World} {e : κ ≃ κ'} : ↑((M.reindex e).toTail (e tail)).root ⊩[((M.reindex e).toTail (e tail)).toModel] A ↔ ↑(M.toTail tail).root ⊩[(M.toTail tail).toModel] A