internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.truthlemma
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ CanonicalModel L ⊧ p ↔ L ⊢! p
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ CanonicalModel L ⊧ p → L ⊢! p

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ CanonicalModel L ⊧ p → L ⊢! p

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p
Tactic:
. contrapose;
  intro h;
  have : (L)-Consistent ({~p}) := by
    simp [ParametricConsistent];
    intro Γ hΓ;
    by_contra hC;
    have : L ⊢! p := dne'! $ replace_imply_left_conj'! hΓ hC;
    contradiction;
  obtain ⟨Ω, hΩ⟩ := lindenbaum this;
  simp [Kripke.ValidOnModel];
  existsi Ω;
  exact truthlemma.not.mpr $ iff_mem_neg.mp (show ~p ∈ Ω.theory by simp_all);
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p
Tactic:
. intro h Ω;
  suffices p ∈ Ω.theory by exact truthlemma.mpr this;
  by_contra hC;
  have := MaximalParametricConsistentTheory.maximal' hC;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Theory.iff_insert_notParametricConsistent.mp this;
  exact Ω.consistent hΓ₁ $ andImplyIffImplyImply'!.mp hΓ₂ ⨀ h;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ CanonicalModel L ⊧ p → L ⊢! p
Tactic:
contrapose
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ ¬L ⊢! p → ¬CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ ¬L ⊢! p → ¬CanonicalModel L ⊧ p
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
⊢ ¬CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
⊢ ¬CanonicalModel L ⊧ p
Tactic:
have : (L)-Consistent ({~p}) := by
  simp [ParametricConsistent];
  intro Γ hΓ;
  by_contra hC;
  have : L ⊢! p := dne'! $ replace_imply_left_conj'! hΓ hC;
  contradiction;
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
⊢ ¬CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
⊢ ¬CanonicalModel L ⊧ p
Tactic:
obtain ⟨Ω, hΩ⟩ := lindenbaum this
Proof state after:
case mp.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ¬CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ¬CanonicalModel L ⊧ p
Tactic:
simp [Kripke.ValidOnModel]
Proof state after:
case mp.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ∃ x, ¬Kripke.Satisfies (CanonicalModel L) x p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ∃ x, ¬Kripke.Satisfies (CanonicalModel L) x p
Tactic:
existsi Ω
Proof state after:
case mp.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ¬Kripke.Satisfies (CanonicalModel L) Ω p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mp.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ¬Kripke.Satisfies (CanonicalModel L) Ω p
Tactic:
exact truthlemma.not.mpr $ iff_mem_neg.mp (show ~p ∈ Ω.theory by simp_all)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
⊢ (L)-Consistent {~p}
Tactic:
simp [ParametricConsistent]
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
⊢ ∀ {Γ : List (Formula α)}, (∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥) → L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
⊢ ∀ {Γ : List (Formula α)}, (∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro Γ hΓ
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
⊢ L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! p := dne'! $ replace_imply_left_conj'! hΓ hC
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! p
⊢ False
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
this : (L)-Consistent {~p}
Ω : MCT L
hΩ : {~p} ⊆ Ω.theory
⊢ ~p ∈ Ω.theory
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p
Tactic:
intro h Ω
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
⊢ Ω ⊧ p
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
⊢ Ω ⊧ p
Tactic:
suffices p ∈ Ω.theory by exact truthlemma.mpr this;
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
⊢ p ∈ Ω.theory
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
⊢ p ∈ Ω.theory
Tactic:
by_contra hC
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
⊢ False
Tactic:
have := MaximalParametricConsistentTheory.maximal' hC
Proof state after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Theory.iff_insert_notParametricConsistent.mp this
Proof state after:
case mpr.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ Ω.theory
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
case mpr.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ Ω.theory
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
exact Ω.consistent hΓ₁ $ andImplyIffImplyImply'!.mp hΓ₂ ⨀ h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
this : p ∈ Ω.theory
⊢ Ω ⊧ p
Tactic:
exact truthlemma.mpr this
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.realize_axiomset_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ CanonicalModel L ⊧* Ax(L)
Tactic:
apply Semantics.realizeSet_iff.mpr
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ ⦃f : Formula α⦄, f ∈ Ax(L) → CanonicalModel L ⊧ f
Theorem: LO.Modal.Standard.Kripke.realize_axiomset_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ ⦃f : Formula α⦄, f ∈ Ax(L) → CanonicalModel L ⊧ f
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.realize_axiomset_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ CanonicalModel L ⊧ p
Tactic:
apply iff_valid_on_canonicalModel_deducible.mpr
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p
Theorem: LO.Modal.Standard.Kripke.realize_axiomset_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p
Tactic:
exact ⟨Deduction.maxm hp⟩
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.realize_theory_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ CanonicalModel L ⊧* System.theory L
Tactic:
apply Semantics.realizeSet_iff.mpr
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ ⦃f : Formula α⦄, f ∈ System.theory L → CanonicalModel L ⊧ f
Theorem: LO.Modal.Standard.Kripke.realize_theory_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ ⦃f : Formula α⦄, f ∈ System.theory L → CanonicalModel L ⊧ f
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ System.theory L
⊢ CanonicalModel L ⊧ p
Theorem: LO.Modal.Standard.Kripke.realize_theory_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ System.theory L
⊢ CanonicalModel L ⊧ p
Tactic:
apply iff_valid_on_canonicalModel_deducible.mpr
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ System.theory L
⊢ L ⊢! p
Theorem: LO.Modal.Standard.Kripke.realize_theory_of_self_canonicalModel
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ System.theory L
⊢ L ⊢! p
Tactic:
simpa [System.theory] using hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ 𝔽(Ax(L)) ⊧ p → L ⊢! p
Tactic:
simp [Kripke.ValidOnFrameClass, Kripke.ValidOnFrame]
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ (∀ F ∈ 𝔽(Ax(L)), ∀ (V : Valuation F.World α), Kripke.ValidOnModel { Frame := F, Valuation := V } p) → L ⊢! p
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ (∀ F ∈ 𝔽(Ax(L)), ∀ (V : Valuation F.World α), Kripke.ValidOnModel { Frame := F, Valuation := V } p) → L ⊢! p
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ ¬L ⊢! p → ¬∀ F ∈ 𝔽(Ax(L)), ∀ (V : Valuation F.World α), Kripke.ValidOnModel { Frame := F, Valuation := V } p
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ ¬L ⊢! p → ¬∀ F ∈ 𝔽(Ax(L)), ∀ (V : Valuation F.World α), Kripke.ValidOnModel { Frame := F, Valuation := V } p
Tactic:
push_neg
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ ¬L ⊢! p → ∃ F ∈ 𝔽(Ax(L)), ∃ V, ¬Kripke.ValidOnModel { Frame := F, Valuation := V } p
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ ¬L ⊢! p → ∃ F ∈ 𝔽(Ax(L)), ∃ V, ¬Kripke.ValidOnModel { Frame := F, Valuation := V } p
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ F ∈ 𝔽(Ax(L)), ∃ V, ¬Kripke.ValidOnModel { Frame := F, Valuation := V } p
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ F ∈ 𝔽(Ax(L)), ∃ V, ¬Kripke.ValidOnModel { Frame := F, Valuation := V } p
Tactic:
use (CanonicalFrame L)
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ CanonicalFrame L ∈ 𝔽(Ax(L)) ∧ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ CanonicalFrame L ∈ 𝔽(Ax(L)) ∧ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ CanonicalFrame L ∈ 𝔽(Ax(L))

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ CanonicalFrame L ∈ 𝔽(Ax(L))

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
Tactic:
. apply Canonical.realize;
Proof state after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
Tactic:
. existsi (CanonicalModel L).Valuation;
  exact iff_valid_on_canonicalModel_deducible.not.mpr h;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ CanonicalFrame L ∈ 𝔽(Ax(L))
Tactic:
apply Canonical.realize
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical
Proof state before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ∃ V, ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := V } p
Tactic:
existsi (CanonicalModel L).Valuation
Proof state after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
h : ¬L ⊢! p
⊢ ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := (CanonicalModel L).Valuation } p