Theorem: LO.Propositional.Superintuitionistic.Kripke.sound (Logic/Propositional/Superintuitionistic/Kripke/Soundness.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
⊢ 𝔽(Ax(𝓓)) ⊧ p
Tactic:
simp [-ValidOnFrame.models_iff]
State after:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
⊢ ∀ {F : Frame' α}, F ∈ 𝔽(Ax(𝓓)) → F ⊧ p

State before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
⊢ ∀ {F : Frame' α}, F ∈ 𝔽(Ax(𝓓)) → F ⊧ p
Tactic:
intro F hF
State after:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
⊢ F ⊧ p

State before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
⊢ F ⊧ p
Tactic:
induction d with
| eaxm h => exact validOnAxiomSetFrameClass_axiom h hF;
| mdp _ _ ihpq ihp => exact ValidOnFrame.mdp ihpq ihp;
| _ =>
  intros;
  first
  | apply ValidOnFrame.verum
  | apply ValidOnFrame.imply₁
  | apply ValidOnFrame.imply₂
  | apply ValidOnFrame.disj₁
  | apply ValidOnFrame.disj₂
  | apply ValidOnFrame.disj₃
  | apply ValidOnFrame.conj₁
  | apply ValidOnFrame.conj₂
  | apply ValidOnFrame.conj₃
State after:
no goals

State before:
case eaxm
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ : Formula α
h : p✝ ∈ Ax(𝓓)
⊢ F ⊧ p✝
Tactic:
exact validOnAxiomSetFrameClass_axiom h hF
State after:
no goals

State before:
case mdp
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
a✝¹ : Deduction 𝓓 (p✝ ⟶ q✝)
a✝ : Deduction 𝓓 p✝
ihpq : F ⊧ p✝ ⟶ q✝
ihp : F ⊧ p✝
⊢ F ⊧ q✝
Tactic:
exact ValidOnFrame.mdp ihpq ihp
State after:
no goals

State before:
case disj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ r✝ : Formula α
⊢ F ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
first
| apply ValidOnFrame.verum
| apply ValidOnFrame.imply₁
| apply ValidOnFrame.imply₂
| apply ValidOnFrame.disj₁
| apply ValidOnFrame.disj₂
| apply ValidOnFrame.disj₃
| apply ValidOnFrame.conj₁
| apply ValidOnFrame.conj₂
| apply ValidOnFrame.conj₃
State after:
no goals

State before:
case verum
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
⊢ F ⊧ ⊤
Tactic:
apply ValidOnFrame.verum
State after:
no goals

State before:
case imply₁
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply ValidOnFrame.imply₁
State after:
no goals

State before:
case imply₂
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ r✝ : Formula α
⊢ F ⊧ (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply ValidOnFrame.imply₂
State after:
no goals

State before:
case disj₁
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply ValidOnFrame.disj₁
State after:
no goals

State before:
case disj₂
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply ValidOnFrame.disj₂
State after:
no goals

State before:
case disj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ r✝ : Formula α
⊢ F ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply ValidOnFrame.disj₃
State after:
no goals

State before:
case conj₁
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply ValidOnFrame.conj₁
State after:
no goals

State before:
case conj₂
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply ValidOnFrame.conj₂
State after:
no goals

State before:
case conj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply ValidOnFrame.conj₃
State after:
no goals