Theorem: LO.Modal.Standard.Kripke.iff_valid_on_canonicalModel_deducible (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 ⊧ p ↔ L ⊢! p
Tactic:
constructor
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

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

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

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

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

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

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

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

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

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

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]
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' ⟶ ⊥

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Γ
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' ⟶ ⊥

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

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

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

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

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

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

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

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

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

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

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