Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Ver (Logic/Modal/Standard/Kripke/Ver.lean)

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
⊢ Isolated (CanonicalFrame 𝓓).Rel
Tactic:
intro x y hxy
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
⊢ False
Tactic:
have : 𝓓 ⊢! □⊥ := ⟨Deduction.maxm (Set.mem_of_subset_of_mem hAx (by simp))⟩
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this : 𝓓 ⊢! □⊥
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this : 𝓓 ⊢! □⊥
⊢ False
Tactic:
have := iff_valid_on_canonicalModel_deducible.mpr this x y hxy
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this✝ : 𝓓 ⊢! □⊥
this : Satisfies (CanonicalModel 𝓓) y ⊥
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this✝ : 𝓓 ⊢! □⊥
this : Satisfies (CanonicalModel 𝓓) y ⊥
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
⊢ □⊥ ∈ 𝗩𝗲𝗿
Tactic:
simp
State after:
no goals