@[reducible, inline]
abbrev
RootedModel.extendRoot.World
{κ : Type u_1}
[Nonempty κ]
{α : Type u_2}
(M : RootedModel κ α)
(n : ℕ+)
:
Type u_1
Worlds of the root extension: the original worlds plus n fresh points below the new root.
Equations
- RootedModel.extendRoot.World M n = (M.World ⊕ Fin ↑n)
Instances For
@[reducible, inline]
abbrev
RootedModel.extendRoot
{κ : Type u_1}
[Nonempty κ]
{α : Type u_2}
(M : RootedModel κ α)
(n : ℕ+)
:
RootedModel (extendRoot.World M n) α
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
RootedModel.extendRoot.embed
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
(x : M.World)
:
(M.extendRoot n).World
Equations
Instances For
@[implicit_reducible]
instance
RootedModel.extendRoot.instCoeWorldWorld
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
:
Coe M.World (M.extendRoot n).World
Equations
theorem
RootedModel.extendRoot.rel_embed_embed_iff_rel
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
{x y : M.World}
:
theorem
RootedModel.extendRoot.relItr_embed_embed_iff_relItr
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
{x y : M.World}
{k : ℕ}
:
@[implicit_reducible]
instance
RootedModel.extendRoot.instFintypeWorldWorld
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
[Fintype M.World]
:
Fintype (M.extendRoot n).World
Equations
instance
RootedModel.extendRoot.instIsTransWorldWorldRel
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
[IsTrans M.World Model.Rel]
:
IsTrans (M.extendRoot n).World Model.Rel
instance
RootedModel.extendRoot.instIrreflWorldWorldRel
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
[Std.Irrefl Model.Rel]
:
instance
RootedModel.extendRoot.instIsConverseWellFoundedWorldWorldRel
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
[IsConverseWellFounded M.World Model.Rel]
:
instance
RootedModel.extendRoot.instIsGLWorld
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
[M.IsGL]
:
(M.extendRoot n).IsGL
@[simp]
theorem
RootedModel.extendRoot.not_rel_original_tail
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
{x : M.World}
{i : Fin ↑n}
:
theorem
RootedModel.extendRoot.exists_tail_of_not_original_world
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
{x : (M.extendRoot n).World}
(h : ∀ (x₀ : M.World), x ≠ extendRoot.embed x₀)
:
theorem
RootedModel.extendRoot.exists_original_of_embed_rel
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
{x : M.World}
{y : (M.extendRoot n).World}
:
extendRoot.embed x ≺ y → ∃ (y₀ : M.World), y = extendRoot.embed y₀
theorem
RootedModel.extendRoot.same_forces_embed
{κ : Type u_2}
{α : Type u_1}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
{A : Formula α}
{x : M.World}
:
def
RootedModel.extendRoot.tail
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
(M : RootedModel κ α)
(n : ℕ+)
:
List (M.extendRoot n).World
Chain of n-root extension of M
Equations
- RootedModel.extendRoot.tail M n = List.map (fun (x : Fin ↑n) => Sum.inr x) (List.finRange ↑n).reverse
Instances For
@[simp]
theorem
RootedModel.extendRoot.tail_length
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
:
@[simp]
theorem
RootedModel.extendRoot.tail_isChain
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
:
List.IsChain (fun (x1 x2 : (M.extendRoot n).World) => x1 ≺ x2) (extendRoot.tail M n)
theorem
RootedModel.extendRoot.Ext1.eq_original_or_eq_root
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
(x : (M.extendRoot 1).World)
:
theorem
RootedModel.extendRoot.Ext1.eq_original_of_rel_extendRoot_root
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
[Std.Irrefl Model.Rel]
{x : (M.extendRoot 1).World}
(h : ↑(M.extendRoot 1).root ≺ x)
:
∃ (x₀ : M.World), x = extendRoot.embed x₀
theorem
RootedModel.extendRoot.Ext1.eq_original_of_neq_extendRoot_root
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
[Std.Irrefl Model.Rel]
{x : (M.extendRoot 1).World}
(h : x ≠ ↑(M.extendRoot 1).root)
:
∃ (x₀ : M.World), x = extendRoot.embed x₀
Axiom T on a chain in an irreflexive transitive model #
theorem
atmost_one_not_forces_axiomT_in_chain
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : Model κ α}
{A : Formula α}
{l : List M.World}
[IsTrans M.World Model.Rel]
(l_chain : List.IsChain (fun (x1 x2 : M.World) => x1 ≺ x2) l)
:
In an irreflexive transitive model, at most one point on a chain refutes the axiom T
instance □A 🡒 A.
theorem
exists_forces_axiomT_set_in_chain
{κ : Type u_2}
{α : Type u_1}
[Nonempty κ]
{M : Model κ α}
{l : List M.World}
[DecidableEq α]
[IsTrans M.World Model.Rel]
[Std.Irrefl Model.Rel]
{Γ : FormulaFinset α}
(l_length : Finset.card Γ < l.length)
(l_chain : List.IsChain (fun (x1 x2 : M.World) => x1 ≺ x2) l)
:
On a chain in an irreflexive transitive model longer than Γ.card, there is a point
where the axiom T instance holds for every formula in Γ.
instance
RootedModel.extendRoot.instIsFiniteGLWorld
{κ : Type u_1}
{α : Type u_2}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
[M.IsFiniteGL]
:
(M.extendRoot n).IsFiniteGL
theorem
RootedModel.extendRoot.exists_tail_forces_forall_axiomT
{κ : Type u_2}
{α : Type u_1}
[Nonempty κ]
{M : RootedModel κ α}
{n : ℕ+}
[DecidableEq α]
[M.IsFiniteGL]
{Γ : FormulaFinset α}
(hn : Finset.card Γ < ↑n)
:
Extending the root by more than Γ.card points yields a chain containing a point
where the axiom T instance holds for every formula in Γ.