Rank and height

theorem FFL.ProvabilityLogic.Kripke.Model.exists_chain_of_relItr {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {x y : M.World} {n : ℕ} (h : RelItr n x y) : ∃ (c : ℕ → M.World), c 0 = x ∧ c n = y ∧ ∀ i < n, Rel (c i) (c (i + 1))

theorem FFL.ProvabilityLogic.Kripke.Model.rel_of_chain {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {n : ℕ} [IsTrans M.World Rel] {c : ℕ → M.World} (hc : ∀ i < n, Rel (c i) (c (i + 1))) {i j : ℕ} (hij : i < j) (hj : j ≤ n) : Rel (c i) (c j)

def FFL.ProvabilityLogic.Kripke.Model.World.IsReflexiveOf {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} (X : FormulaFinset α) (x : M.World) : Prop

Called Σ-reflexivity in the source.

• [KK23]

Equations

• FFL.ProvabilityLogic.Kripke.Model.World.IsReflexiveOf X x = ∀ A ∈ X, FFL.ProvabilityLogic.Kripke.Model.World.Forces M x (□A 🡒 A)

theorem FFL.ProvabilityLogic.Kripke.Model.World.forces_axiomT_of_rel {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} {y z : M.World} {B : Formula α} (Ryz : Rel y z) (hy : ¬Forces M y (□B 🡒 B)) : Forces M z (□B 🡒 B)

noncomputable def FFL.ProvabilityLogic.Kripke.Model.World.rank {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [Fintype M.World] [M.IsGL] (x : M.World) : ℕ

Equations

• x.rank = cwfHeight (fun (x1 x2 : M.World) => FFL.ProvabilityLogic.Kripke.Model.Rel x1 x2) x

theorem FFL.ProvabilityLogic.Kripke.Model.rank_lt_of_rel {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [Fintype M.World] [M.IsGL] {x y : M.World} (h : Rel x y) : y.rank < x.rank

theorem FFL.ProvabilityLogic.Kripke.Model.exists_rel_rank_eq_of_lt {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [Fintype M.World] [M.IsGL] {x : M.World} {n : ℕ} (h : n < x.rank) : ∃ (y : M.World), Rel x y ∧ y.rank = n

theorem FFL.ProvabilityLogic.Kripke.Model.rank_lt_iff {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [Fintype M.World] [M.IsGL] {x : M.World} {n : ℕ} : x.rank < n ↔ ∀ (y : M.World), NotRelItr n x y

theorem FFL.ProvabilityLogic.Kripke.Model.forces_boxItr_bot_iff {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [Fintype M.World] [M.IsGL] {x : M.World} {n : ℕ} : World.Forces M x (□^[n]⊥) ↔ x.rank < n

theorem FFL.ProvabilityLogic.Kripke.Model.rank_pos_of_forces_dia {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [Fintype M.World] [M.IsGL] {x : M.World} {A : Formula α} (h : World.Forces M x (◇A)) : 0 < x.rank

theorem FFL.ProvabilityLogic.Kripke.Model.exists_isReflexiveOf_of_card_lt_rank {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} [Fintype M.World] [M.IsGL] {x : M.World} {X : FormulaFinset α} (h : Finset.card X < x.rank) : ∃ (y : M.World), Rel x y ∧ World.IsReflexiveOf X y

• [AB05, Lemma 26]

noncomputable def FFL.ProvabilityLogic.Kripke.RootedModel.height {κ : Type u_1} {α : Type u_2} [Nonempty κ] (M : RootedModel κ α) [Fintype M.World] [M.IsGL] : ℕ

Equations

• M.height = M.root.rank

theorem FFL.ProvabilityLogic.Kripke.RootedModel.rank_lt_height {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} [Fintype M.World] [M.IsGL] {x : M.World} (h : Model.Rel M.root x) : x.rank < M.height

theorem FFL.ProvabilityLogic.Kripke.RootedModel.rank_le_height {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} [Fintype M.World] [M.IsGL] {x : M.World} : x.rank ≤ M.height

theorem FFL.ProvabilityLogic.Kripke.RootedModel.root_forces_boxItr_bot_iff {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : RootedModel κ α} [Fintype M.World] [M.IsGL] {n : ℕ} : Model.World.Forces M.toModel M.root (□^[n]⊥) ↔ M.height < n