internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Tactic:
. intro h;
  simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v;
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a) →
    Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)
Tactic:
intro _ _ h
Proof state after:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
a✝ : Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
w'✝ : M.Frame.World
h : v ≺ w'✝
⊢ Formula.Kripke.Satisfies M w'✝ (Formula.atom a)
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
a✝ : Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
w'✝ : M.Frame.World
h : v ≺ w'✝
⊢ Formula.Kripke.Satisfies M w'✝ (Formula.atom a)
Tactic:
simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies]
Proof state after:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
w'✝ : M.Frame.World
a✝ : iV v a
h : v ≺ w'✝
⊢ iV w'✝ a
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hatom.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
w'✝ : M.Frame.World
a✝ : iV v a
h : v ≺ w'✝
⊢ iV w'✝ a
Tactic:
exact iV_hereditary h (by assumption)
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
w'✝ : M.Frame.World
a✝ : iV v a
h : v ≺ w'✝
⊢ iV v a
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Tactic:
intro h
Proof state after:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hatom.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝¹ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h✝ : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
a : α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)
Tactic:
simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hor
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
p✝ q✝ : Superintuitionistic.Formula α
a✝¹ :
  ∀ (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v p✝ ↔ Formula.Kripke.Satisfies M v (p✝ᵍ)
a✝ :
  ∀ (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q✝ ↔ Formula.Kripke.Satisfies M v (q✝ᵍ)
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (p✝ ⋎ q✝) ↔ Formula.Kripke.Satisfies M v ((p✝ ⋎ q✝)ᵍ)
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ M.Frame ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰)
Tactic:
apply Modal.Standard.Kripke.iff_definability_memAxiomSetFrameClass
  (show Kripke.Definability _ (λ F => Reflexive F.Rel ∧ Transitive F.Rel) by simpa using instGeachDefinability (L := 𝐒𝟒))
  |>.mpr
Proof state after:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel ∧ Transitive M.Frame.Rel
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel ∧ Transitive M.Frame.Rel
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel

case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel

case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Tactic:
. exact iF.Rel_refl;
Proof state after:
case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Tactic:
. exact iF.Rel_trans;
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Kripke.Definability (𝗞 ∪ 𝗧 ∪ 𝟰) fun F => Reflexive F.Rel ∧ Transitive F.Rel
Tactic:
simpa using instGeachDefinability (L := 𝐒𝟒)
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Reflexive M.Frame.Rel
Tactic:
exact iF.Rel_refl
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
h₁ :
  ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
this : ¬Formula.Kripke.Satisfies M w (pᵍ)
⊢ Transitive M.Frame.Rel
Tactic:
exact iF.Rel_trans
Proof state after:
no goals