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. The chain hangs directly below the root, so the rank of every world other than the root is unchanged.

• [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

theorem 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

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

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

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

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

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)

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)

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

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

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

Forcing preservation: if a forces every axiom T instance for the boxed subformulas of A, then for every subformula 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]