internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
Tactic:
. assumption;
Proof state after:
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
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
Tactic:
. apply iff_mem_imp.not.mpr; simp [hpY, hqY];
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
Tactic:
apply iff_mem_imp.not.mpr
Proof state after:
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 ∈ Y.theory → q ∈ Y.theory)
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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 ∈ Y.theory → q ∈ Y.theory)
Tactic:
simp [hpY, hqY]
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □(□q ⟶ p) ∉ 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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □q ⟶ p ∈ Ω'.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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □q ⟶ p ∈ Ω'.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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □q ⟶ p ∉ Ω'.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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □q ⟶ p ∉ Ω'.theory
Tactic:
use Z
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory ∧ □q ⟶ p ∉ Z.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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory ∧ □q ⟶ p ∉ Z.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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Tactic:
. assumption;
Proof state after:
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Tactic:
. apply iff_mem_imp.not.mpr; simp [hpZ, hqZ];
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Tactic:
apply iff_mem_imp.not.mpr
Proof state after:
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬(□q ∈ Z.theory → p ∈ Z.theory)
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3
Proof state before:
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
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬(□q ∈ Z.theory → p ∈ Z.theory)
Tactic:
simp [hpZ, hqZ]
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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
Tactic:
apply iff_mem_or.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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ ¬(□(□p ⟶ q) ∈ X.theory ∨ □(□q ⟶ p) ∈ X.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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ ¬(□(□p ⟶ q) ∈ X.theory ∨ □(□q ⟶ p) ∈ X.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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ∉ X.theory ∧ □(□q ⟶ p) ∉ X.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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ∉ X.theory ∧ □(□q ⟶ p) ∉ X.theory
Tactic:
exact ⟨hpqX, hqpX⟩
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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory
Tactic:
apply subset_axiomset _
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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ Ax(𝓓)
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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ Ax(𝓓)
Tactic:
exact hAx (by aesop)
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
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ .𝟯
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameterRules.nec_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hNec : R₁.nec = true
⊢ R₂.nec = true
Tactic:
apply h.1
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hNec : R₁.nec = true
⊢ R₁.nec = true
Theorem: LO.Modal.Standard.DeductionParameterRules.nec_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hNec : R₁.nec = true
⊢ R₁.nec = true
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameterRules.loeb_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hLoeb : R₁.loeb = true
⊢ R₂.loeb = true
Tactic:
apply h.2.1
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hLoeb : R₁.loeb = true
⊢ R₁.loeb = true
Theorem: LO.Modal.Standard.DeductionParameterRules.loeb_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hLoeb : R₁.loeb = true
⊢ R₁.loeb = true
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameterRules.henkin_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hHenkin : R₁.henkin = true
⊢ R₂.henkin = true
Tactic:
apply h.2.2
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hHenkin : R₁.henkin = true
⊢ R₁.henkin = true
Theorem: LO.Modal.Standard.DeductionParameterRules.henkin_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hHenkin : R₁.henkin = true
⊢ R₁.henkin = true
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.normal_rule
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := true, loeb := false, henkin := false }
Tactic:
nth_rw 1 [←(normal_has_nec (𝓓 := 𝓓))]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := 𝓓.rules.nec, loeb := false, henkin := false }
Theorem: LO.Modal.Standard.DeductionParameter.normal_rule
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := 𝓓.rules.nec, loeb := false, henkin := false }
Tactic:
nth_rw 1 [←(notmal_not_has_loeb (𝓓 := 𝓓))]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := 𝓓.rules.nec, loeb := 𝓓.rules.loeb, henkin := false }
Theorem: LO.Modal.Standard.DeductionParameter.normal_rule
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝ : 𝓓.Normal
⊢ 𝓓.rules = { nec := 𝓓.rules.nec, loeb := 𝓓.rules.loeb, henkin := false }
Tactic:
nth_rw 1 [←(notmal_not_has_henkin (𝓓 := 𝓓))]
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.normal_rules
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
⊢ 𝓓₁.rules = 𝓓₂.rules
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.union_left_rules
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
h : 𝓓₁.rules = 𝓓₂.rules
⊢ ((𝓓₁ ⊔ 𝓓₂) h).rules = 𝓓₁.rules
Tactic:
cases 𝓓₁
Proof state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₂ : DeductionParameter α
axiomSet✝ : AxiomSet α
rules✝ : DeductionParameterRules
h : { axiomSet := axiomSet✝, rules := rules✝ }.rules = 𝓓₂.rules
⊢ (({ axiomSet := axiomSet✝, rules := rules✝ } ⊔ 𝓓₂) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
Theorem: LO.Modal.Standard.DeductionParameter.union_left_rules
Proof state before:
case mk
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₂ : DeductionParameter α
axiomSet✝ : AxiomSet α
rules✝ : DeductionParameterRules
h : { axiomSet := axiomSet✝, rules := rules✝ }.rules = 𝓓₂.rules
⊢ (({ axiomSet := axiomSet✝, rules := rules✝ } ⊔ 𝓓₂) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.union_right_rules
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
h : 𝓓₁.rules = 𝓓₂.rules
⊢ ((𝓓₁ ⊔ 𝓓₂) h).rules = 𝓓₂.rules
Tactic:
cases 𝓓₂
Proof state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ : DeductionParameter α
axiomSet✝ : AxiomSet α
rules✝ : DeductionParameterRules
h : 𝓓₁.rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
⊢ ((𝓓₁ ⊔ { axiomSet := axiomSet✝, rules := rules✝ }) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
Theorem: LO.Modal.Standard.DeductionParameter.union_right_rules
Proof state before:
case mk
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ : DeductionParameter α
axiomSet✝ : AxiomSet α
rules✝ : DeductionParameterRules
h : 𝓓₁.rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
⊢ ((𝓓₁ ⊔ { axiomSet := axiomSet✝, rules := rules✝ }) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.union_left_rules_normal
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
⊢ ((𝓓₁ ⊔ 𝓓₂) ⋯).rules = 𝓓₁.rules
Tactic:
apply union_left_rules
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.union_right_rules_normal
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
⊢ ((𝓓₁ ⊔ 𝓓₂) ⋯).rules = 𝓓₂.rules
Tactic:
apply union_right_rules
Proof state after:
no goals
Theorem: LO.Modal.Standard.Deduction.reducible_of_subset
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
hNec : 𝓓₁.rules ≤ 𝓓₂.rules
hAx : autoParam (Ax(𝓓₁) ⊆ Ax(𝓓₂)) _auto✝
⊢ 𝓓₁ ≤ₛ 𝓓₂
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
hNec : 𝓓₁.rules ≤ 𝓓₂.rules
hAx : autoParam (Ax(𝓓₁) ⊆ Ax(𝓓₂)) _auto✝
p : Formula α
hp : p ∈ System.theory 𝓓₁
⊢ p ∈ System.theory 𝓓₂
Theorem: LO.Modal.Standard.Deduction.reducible_of_subset
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
hNec : 𝓓₁.rules ≤ 𝓓₂.rules
hAx : autoParam (Ax(𝓓₁) ⊆ Ax(𝓓₂)) _auto✝
p : Formula α
hp : p ∈ System.theory 𝓓₁
⊢ p ∈ System.theory 𝓓₂
Tactic:
apply maxm_subset! hNec hAx hp
Proof state after:
no goals