Theorem: LO.Modal.Standard.Kripke.complete!_on_frameclass_of_canonical (Logic/Modal/Standard/Kripke/Completeness.lean)

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

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

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

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

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

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

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

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

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

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

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
⊢ ¬Kripke.ValidOnModel { Frame := CanonicalFrame L, Valuation := (CanonicalModel L).Valuation } p
Tactic:
exact iff_valid_on_canonicalModel_deducible.not.mpr h
State after:
no goals