internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro
α : 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ᵍ
Tactic:
have h₁ : ∀ q v, Satisfies ⟨iF, iV, iV_hereditary⟩ v q ↔ (Modal.Standard.Formula.Kripke.Satisfies M v (qᵍ)) := by
  intro q v;
  induction q using Superintuitionistic.Formula.rec' generalizing v with
  | hatom a =>
    constructor;
    . intro _ _ h;
      simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies];
      exact iV_hereditary h (by assumption);
    . intro h;
      simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v;
  | _ => simp_all;
Proof state after:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
have : ¬(Modal.Standard.Formula.Kripke.Satisfies M w (pᵍ)) := (h₁ p w).not.mp h
Proof state after:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ¬𝐒𝟒 ⊢! pᵍ
Tactic:
apply not_imp_not.mpr $ Modal.Standard.Kripke.sound!_on_frameclass
Proof state after:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ¬𝔽(Ax(𝐒𝟒)) ⊧ pᵍ
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ¬𝔽(Ax(𝐒𝟒)) ⊧ pᵍ
Tactic:
simp [Formula.Kripke.ValidOnFrame, Formula.Kripke.ValidOnModel]
Proof state after:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ∃ x ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰), ∃ x_1 x_2, ¬Formula.Kripke.Satisfies { Frame := x, Valuation := x_1 } x_2 (pᵍ)
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro
α : 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ᵍ)
⊢ ∃ x ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰), ∃ x_1 x_2, ¬Formula.Kripke.Satisfies { Frame := x, Valuation := x_1 } x_2 (pᵍ)
Tactic:
existsi M.Frame
Proof state after:
case intro.intro.intro.intro.intro
α : 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 ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰) ∧ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro
α : 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 ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰) ∧ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Tactic:
constructor
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ᵍ)
⊢ M.Frame ∈ 𝔽(𝗞 ∪ 𝗧 ∪ 𝟰)

case intro.intro.intro.intro.intro.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ᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case intro.intro.intro.intro.intro.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ᵍ)
⊢ ∃ x x_1, ¬Formula.Kripke.Satisfies { Frame := M.Frame, Valuation := x } x_1 (pᵍ)
Tactic:
. use M.Valuation, w;
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
⊢ ?m.89406
Tactic:
simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr Superintuitionistic.Kripke.complete! h
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 }
⊢ ∀ (q : Superintuitionistic.Formula α) (v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World),
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
Tactic:
intro q v
Proof state after:
α : 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 }
q : Superintuitionistic.Formula α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
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 }
q : Superintuitionistic.Formula α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
Tactic:
induction q using Superintuitionistic.Formula.rec' generalizing v with
| hatom a =>
  constructor;
  . intro _ _ h;
    simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies];
    exact iV_hereditary h (by assumption);
  . intro h;
    simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v;
| _ => simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_S4_of_provable_efq
Proof state before:
case hatom
α : 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:
constructor
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
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a) →
    Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ)

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)
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ᵍ)

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;
  simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies];
  exact iV_hereditary h (by assumption);
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
⊢ Formula.Kripke.Satisfies M v (Superintuitionistic.Formula.atom aᵍ) →
    Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v (Superintuitionistic.Formula.atom a)