theorem RootedModel.not_rel_root {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} [IsTrans M.World Model.Rel] [Std.Irrefl Model.Rel] {x : M.World} : ¬x ≺ ↑M.root

@[reducible, inline]

abbrev RootedModel.graft.World {κ : Type u_1} {α : Type u_2} [Nonempty κ] (M : RootedModel κ α) (k : ℕ) : Type u_1

Worlds of the grafted model: the original worlds plus a chain of length k.

Equations

• RootedModel.graft.World M k = (M.World ⊕ Fin k)

@[reducible, inline]

abbrev RootedModel.graft {κ : Type u_1} {α : Type u_2} [Nonempty κ] (M : RootedModel κ α) (a : M.NonRoot) (k : ℕ) : RootedModel (graft.World M k) α

The rooted model obtained by grafting a chain of length k between the root and a (root ≺ chain ≺ a and its cone): a "bone lengthening" construction. Hanging the chain directly below the root keeps the rank of every world other than the root unchanged, so that the height is exactly max M.height (a.rank + k + 1).

• [AB05, Lemma 12]

Equations

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

theorem RootedModel.graft.ne_root_of_rel {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} [IsTrans M.World Model.Rel] [Std.Irrefl Model.Rel] (_Rra : ↑M.root ≺ ↑a) : ↑a ≠ ↑M.root

@[reducible]

def RootedModel.graft.isFiniteGL {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} [M.IsFiniteGL] (Rra : ↑M.root ≺ ↑a) : (M.graft a k).IsFiniteGL

Equations

• ⋯ = ⋯

theorem RootedModel.graft.relItr_inl {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} {x y : M.World} {n : ℕ} (h : x ≺^[n] y) : Sum.inl x ≺^[n] Sum.inl y

inl preserves relItr.

theorem RootedModel.graft.relItr_from_inl {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} [M.IsGL] {x : M.World} {n : ℕ} {w : (M.graft a k).World} (hx : x ≠ ↑M.root) (h : Sum.inl x ≺^[n] w) : ∃ (y : M.World), w = Sum.inl y ∧ x ≺^[n] y ∧ y ≠ ↑M.root

A chain starting from a non-root inl world stays inside inl and projects to a chain in M.

theorem RootedModel.graft.relItr_from_inr_le {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} [Fintype M.World] [M.IsGL] (_Rra : ↑M.root ≺ ↑a) {i : Fin k} {n : ℕ} {w : (M.graft a k).World} (h : Sum.inr i ≺^[n] w) : n ≤ ↑i + 1 + (↑a).rank

The length of a chain starting from a grafted world is bounded by i + 1 + a.rank.

theorem RootedModel.graft.inr_relItr_inl_a {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} {i : Fin k} : Sum.inr i ≺^[↑i + 1] Sum.inl ↑a

There is a chain of length i + 1 from the grafted world inr i down to inl a.

theorem RootedModel.graft.relItr_from_root_le {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} [Fintype M.World] [M.IsGL] (Rra : ↑M.root ≺ ↑a) {n : ℕ} {w : (M.graft a k).World} (h : Sum.inl ↑M.root ≺^[n] w) : n ≤ max M.height ((↑a).rank + k + 1)

The length of a chain starting from the root is bounded by max M.height (a.rank + k + 1).

theorem RootedModel.graft.height_eq {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} [Fintype M.World] [M.IsGL] (Rra : ↑M.root ≺ ↑a) [Fintype (M.graft a k).World] [(M.graft a k).IsGL] : (M.graft a k).height = max M.height ((↑a).rank + k + 1)

Height formula: (M.graft a k).height = max M.height (a.rank + k + 1). Note that Foundation's axiom boneLengthening.eq_height (claiming M.height + k) is false in general when some other branch is higher; this max form holds exactly.

• [AB05, Lemma 12]

theorem RootedModel.graft.rank_inl {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} [Fintype M.World] [M.IsGL] [Fintype (M.graft a k).World] [(M.graft a k).IsGL] {x : M.World} (hx : x ≠ ↑M.root) : Model.World.rank (Sum.inl x) = x.rank

inl preserves the rank of non-root worlds.

theorem RootedModel.graft.rank_inr {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {a : M.NonRoot} {k : ℕ} [Fintype M.World] [M.IsGL] [Fintype (M.graft a k).World] [(M.graft a k).IsGL] (Rra : ↑M.root ≺ ↑a) {i : Fin k} : Model.World.rank (Sum.inr i) = ↑i + 1 + (↑a).rank

The rank of the grafted world inr i is exactly i + 1 + a.rank.

theorem RootedModel.graft.mainlemma {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} {k : ℕ} [DecidableEq α] {A : Formula α} [IsTrans M.World Model.Rel] [Std.Irrefl Model.Rel] (a : M.ReflexiveWorldOf A.subfmls) (Rra : ↑M.root ≺ ↑a) {C : Formula α} (hC : C ∈ A.subfmls) : (∀ (i : Fin k), Sum.inr i ⊩[(M.graft ⟨↑a, ⋯⟩ k).toModel] C ↔ Sum.inl ↑a ⊩[(M.graft ⟨↑a, ⋯⟩ k).toModel] C) ∧ ∀ (x : M.World), Sum.inl x ⊩[(M.graft ⟨↑a, ⋯⟩ k).toModel] C ↔ x ⊩[M.toModel] C

Main lemma (forcing-preservation): if a forces every axiom T instance for the boxed subformulas of A, then for every subformula C of A, forcing at the grafted chain worlds agrees with a, and forcing at the inl worlds agrees with the original model.

• [AB05, Lemma 12]