Theorem: LO.Propositional.Superintuitionistic.Kripke.disjunctive_int
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝¹ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
Fq : Frame' α
left✝ : Fq ∈ 𝔽(𝗘𝗙𝗤)
Vq : Valuation Fq.World α
hVq : ∀ {w₁ w₂ : Fq.World}, w₁ ≺ w₂ → ∀ {a : α}, Vq w₁ a → Vq w₂ a
wq : { Frame := Fq, Valuation := Vq, hereditary := ⋯ }.World
hq : ¬Satisfies { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wq q
M : Model α :=
  IntDPCounterexampleModel { Frame := Fp, Valuation := Vp, hereditary := ⋯ }
    { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wp wq
⊢ M.Frame ∈ 𝔽(𝗘𝗙𝗤)

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝¹ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
Fq : Frame' α
left✝ : Fq ∈ 𝔽(𝗘𝗙𝗤)
Vq : Valuation Fq.World α
hVq : ∀ {w₁ w₂ : Fq.World}, w₁ ≺ w₂ → ∀ {a : α}, Vq w₁ a → Vq w₂ a
wq : { Frame := Fq, Valuation := Vq, hereditary := ⋯ }.World
hq : ¬Satisfies { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wq q
M : Model α :=
  IntDPCounterexampleModel { Frame := Fp, Valuation := Vp, hereditary := ⋯ }
    { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wp wq
⊢ ∃ x,
    ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ∃ x_1,
        ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q
Tactic:
. apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr;
  trivial;
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝¹ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
Fq : Frame' α
left✝ : Fq ∈ 𝔽(𝗘𝗙𝗤)
Vq : Valuation Fq.World α
hVq : ∀ {w₁ w₂ : Fq.World}, w₁ ≺ w₂ → ∀ {a : α}, Vq w₁ a → Vq w₂ a
wq : { Frame := Fq, Valuation := Vq, hereditary := ⋯ }.World
hq : ¬Satisfies { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wq q
M : Model α :=
  IntDPCounterexampleModel { Frame := Fp, Valuation := Vp, hereditary := ⋯ }
    { Frame := Fq, Valuation := Vq, hereditary := ⋯ } wp wq
⊢ ∃ x,
    ∃ (h : ∀ {w₁ w₂ : M.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ∃ x_1,
        ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 p ∧
          ¬Satisfies { Frame := M.Frame, Valuation := x, hereditary := ⋯ } x_1 q