internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
rzy : F.Rel z y
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
Tactic:
simp [Satisfies.box_def, Satisfies.imp_def]
Proof state after:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
rzy : F.Rel z y
⊢ (∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q) →
    Satisfies { Frame := F, Valuation := V } z p
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
rzy : F.Rel z y
⊢ (∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q) →
    Satisfies { Frame := F, Valuation := V } z p
Tactic:
intro hq
Proof state after:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
⊢ Satisfies { Frame := F, Valuation := V } z p
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
⊢ Satisfies { Frame := F, Valuation := V } z p
Tactic:
have hyp := hq y rzy
Proof state after:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp✝ : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
hyp : Satisfies { Frame := F, Valuation := V } y q
⊢ Satisfies { Frame := F, Valuation := V } z p
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp✝ : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
hyp : Satisfies { Frame := F, Valuation := V } y q
⊢ Satisfies { Frame := F, Valuation := V } z p
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
⊢ Connected (CanonicalFrame 𝓓).Rel
Tactic:
dsimp only [Connected]
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
⊢ ∀ ⦃x y z : MCT 𝓓⦄,
    □''⁻¹x.theory ⊆ y.theory ∧ □''⁻¹x.theory ⊆ z.theory → □''⁻¹y.theory ⊆ z.theory ∨ □''⁻¹z.theory ⊆ y.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
⊢ ∀ ⦃x y z : MCT 𝓓⦄,
    □''⁻¹x.theory ⊆ y.theory ∧ □''⁻¹x.theory ⊆ z.theory → □''⁻¹y.theory ⊆ z.theory ∨ □''⁻¹z.theory ⊆ y.theory
Tactic:
intro X Y Z ⟨hXY, hXZ⟩
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
⊢ □''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
⊢ □''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory
Tactic:
by_contra hC
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬(□''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory)
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬(□''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory)
⊢ False
Tactic:
push_neg at hC
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Tactic:
have ⟨nhYZ, nhZY⟩ := hC
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Tactic:
clear hC
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Tactic:
simp only [Set.not_subset] at nhYZ nhZY
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ∃ a ∈ □''⁻¹Y.theory, a ∉ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ∃ a ∈ □''⁻¹Y.theory, a ∉ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
⊢ False
Tactic:
obtain ⟨p, hpY, hpZ⟩ := nhYZ
Proof state after:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpY : p ∈ □''⁻¹Y.theory
hpZ : p ∉ Z.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpY : p ∈ □''⁻¹Y.theory
hpZ : p ∉ Z.theory
⊢ False
Tactic:
replace hpY : □p ∈ Y.theory := hpY
Proof state after:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
⊢ False
Tactic:
obtain ⟨q, hqZ, hqY⟩ := nhZY
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqZ : q ∈ □''⁻¹Z.theory
hqY : q ∉ Y.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqZ : q ∈ □''⁻¹Z.theory
hqY : q ∉ Y.theory
⊢ False
Tactic:
replace hqZ : □q ∈ Z.theory := hqZ
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ False
Tactic:
have hpqX : □(□p ⟶ q) ∉ X.theory := by
  apply iff_mem_box.not.mpr; push_neg;
  use Y;
  constructor;
  . assumption;
  . apply iff_mem_imp.not.mpr; simp [hpY, hqY];
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ False
Tactic:
have hqpX : □(□q ⟶ p) ∉ X.theory := by
  apply iff_mem_box.not.mpr; push_neg;
  use Z;
  constructor;
  . assumption;
  . apply iff_mem_imp.not.mpr; simp [hpZ, hqZ];
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ False
Tactic:
have : (□(□p ⟶ q) ⋎ □(□q ⟶ p)) ∉ X.theory := by
  apply iff_mem_or.not.mpr; push_neg; exact ⟨hpqX, hqpX⟩;
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ False
Tactic:
have : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory := by
  apply subset_axiomset _
  exact hAx (by aesop);
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this✝ : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this✝ : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □(□p ⟶ q) ∉ X.theory
Tactic:
apply iff_mem_box.not.mpr
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □p ⟶ q ∈ Ω'.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □p ⟶ q ∈ Ω'.theory
Tactic:
push_neg
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □p ⟶ q ∉ Ω'.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □p ⟶ q ∉ Ω'.theory
Tactic:
use Y
Proof state after:
case h
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory ∧ □p ⟶ q ∉ Y.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
case h
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory ∧ □p ⟶ q ∉ Y.theory
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory

case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □p ⟶ q ∉ Y.theory