Theorem: LO.Modal.Standard.Kripke.truthlemma (Logic/Modal/Standard/Kripke/Completeness.lean)

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
State after:
no goals

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]
State after:
no goals

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 Ω
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

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

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Ω';
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

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;
State after:
no goals

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

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

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Ω'
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

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

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Ω'
State after:
no goals

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Ω'
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

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

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
State after:
no goals

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))]
State after:
no goals

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))]
State after:
no goals

State before:
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p✝ q✝ : Formula α
a✝¹ : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p✝ ↔ p✝ ∈ Ω.theory
a✝ : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ q✝ ↔ q✝ ∈ Ω.theory
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p✝ ⋎ q✝ ↔ p✝ ⋎ q✝ ∈ Ω.theory
Tactic:
simp_all
State after:
no goals