internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω.theory
Tactic:
intro p hp
Proof state after:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ Ω.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ Ω.theory
Tactic:
apply hΩ
Proof state after:
case succ.mpr.intro.right.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.right.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
. intro h p hp; exact multiframe_def_multibox.mp h hp;
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
. intro h; apply multiframe_def_multibox.mpr; assumption;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
Tactic:
intro h p hp
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ ≺^[n] Ω₂
p : Formula α
hp : p ∈ □''⁻¹^[n]Ω₁.theory
⊢ p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ ≺^[n] Ω₂
p : Formula α
hp : p ∈ □''⁻¹^[n]Ω₁.theory
⊢ p ∈ Ω₂.theory
Tactic:
exact multiframe_def_multibox.mp h hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n] Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n] Ω₂
Tactic:
apply multiframe_def_multibox.mpr
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox'
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory

case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
. intro h p hp; exact multiframe_def_multibox.mp h hp;
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
. intro h; apply multiframe_def_multibox.mpr; assumption;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
Tactic:
intro h p hp
Proof state after:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ ≺^[n] Ω₂
p : Formula α
hp : p ∈ □''⁻¹^[n]Ω₁.theory
⊢ p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ ≺^[n] Ω₂
p : Formula α
hp : p ∈ □''⁻¹^[n]Ω₁.theory
⊢ p ∈ Ω₂.theory
Tactic:
exact multiframe_def_multibox.mp h hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n] Ω₂
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n] Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n] Ω₂
Tactic:
apply multiframe_def_multibox.mpr
Proof state after:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox''
Proof state before:
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalModel.frame_def
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalModel L).Frame.World
⊢ (CanonicalModel L).Frame.Rel Ω₁ Ω₂ ↔ □''⁻¹Ω₁.theory ⊆ Ω₂.theory
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalModel.val_def
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
Ω : (CanonicalModel L).Frame.World
a : α
⊢ (CanonicalModel L).Valuation Ω a ↔ atom a ∈ Ω.theory
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Tactic:
induction p using Formula.rec' with
| hatom a => simp [Kripke.Satisfies];
| hbox p ih =>
  intro Ω;
  constructor;
  . intro h;
    apply iff_mem_box.mpr;
    intro Ω' hΩ';
    apply ih.mp;
    exact h Ω' hΩ';
  . intro h Ω' hΩ';
    apply ih.mpr;
    exact CanonicalFrame.frame_def_box.mp hΩ' h;
| hfalsum => simp [Formula.Kripke.Satisfies.bot_def (M := (CanonicalModel L))];
| hVerum => simp [Formula.Kripke.Satisfies.top_def (M := (CanonicalModel L))];
| _ => simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hatom
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
a : α
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ atom a ↔ atom a ∈ Ω.theory
Tactic:
simp [Kripke.Satisfies]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ □p ↔ □p ∈ Ω.theory
Tactic:
intro Ω
Proof state after:
case hbox
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ Ω ⊧ □p ↔ □p ∈ Ω.theory
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ Ω ⊧ □p ↔ □p ∈ Ω.theory
Tactic:
constructor
Proof state after:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ Ω ⊧ □p → □p ∈ Ω.theory

case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ □p ∈ Ω.theory → Ω ⊧ □p
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ Ω ⊧ □p → □p ∈ Ω.theory

case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ □p ∈ Ω.theory → Ω ⊧ □p
Tactic:
. intro h;
  apply iff_mem_box.mpr;
  intro Ω' hΩ';
  apply ih.mp;
  exact h Ω' hΩ';
Proof state after:
case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ □p ∈ Ω.theory → Ω ⊧ □p
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ □p ∈ Ω.theory → Ω ⊧ □p
Tactic:
. intro h Ω' hΩ';
  apply ih.mpr;
  exact CanonicalFrame.frame_def_box.mp hΩ' h;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ Ω ⊧ □p → □p ∈ Ω.theory
Tactic:
intro h
Proof state after:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
⊢ □p ∈ Ω.theory
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
⊢ □p ∈ Ω.theory
Tactic:
apply iff_mem_box.mpr
Proof state after:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
⊢ ∀ {Ω' : MCT L}, □''⁻¹Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
⊢ ∀ {Ω' : MCT L}, □''⁻¹Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
intro Ω' hΩ'
Proof state after:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
Ω' : MCT L
hΩ' : □''⁻¹Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
Ω' : MCT L
hΩ' : □''⁻¹Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory
Tactic:
apply ih.mp
Proof state after:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
Ω' : MCT L
hΩ' : □''⁻¹Ω.theory ⊆ Ω'.theory
⊢ Ω' ⊧ p
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : Ω ⊧ □p
Ω' : MCT L
hΩ' : □''⁻¹Ω.theory ⊆ Ω'.theory
⊢ Ω' ⊧ p
Tactic:
exact h Ω' hΩ'
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ □p ∈ Ω.theory → Ω ⊧ □p
Tactic:
intro h Ω' hΩ'
Proof state after:
case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : □p ∈ Ω.theory
Ω' : (CanonicalModel L).Frame.World
hΩ' : Ω ≺ Ω'
⊢ Kripke.Satisfies (CanonicalModel L) Ω' p
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : □p ∈ Ω.theory
Ω' : (CanonicalModel L).Frame.World
hΩ' : Ω ≺ Ω'
⊢ Kripke.Satisfies (CanonicalModel L) Ω' p
Tactic:
apply ih.mpr
Proof state after:
case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : □p ∈ Ω.theory
Ω' : (CanonicalModel L).Frame.World
hΩ' : Ω ≺ Ω'
⊢ p ∈ Ω'.theory
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hbox.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
h : □p ∈ Ω.theory
Ω' : (CanonicalModel L).Frame.World
hΩ' : Ω ≺ Ω'
⊢ p ∈ Ω'.theory
Tactic:
exact CanonicalFrame.frame_def_box.mp hΩ' h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hfalsum
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ ⊥ ↔ ⊥ ∈ Ω.theory
Tactic:
simp [Formula.Kripke.Satisfies.bot_def (M := (CanonicalModel L))]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof state before:
case hVerum
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ ⊤ ↔ ⊤ ∈ Ω.theory
Tactic:
simp [Formula.Kripke.Satisfies.top_def (M := (CanonicalModel L))]
Proof state after:
no goals