internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω₁.theory = Ω₂.theory
⊢ Ω₁ = Ω₂
Tactic:
cases Ω₁
Proof state after:
case mpr.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₂ : MCT L
p : Formula α
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h : { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory = Ω₂.theory
⊢ { theory := theory✝, consistent := consistent✝, maximal := maximal✝ } = Ω₂
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
case mpr.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₂ : MCT L
p : Formula α
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h : { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory = Ω₂.theory
⊢ { theory := theory✝, consistent := consistent✝, maximal := maximal✝ } = Ω₂
Tactic:
cases Ω₂
Proof state after:
case mpr.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω : MCT L
p : Formula α
theory✝¹ : Theory α
consistent✝¹ : (L)-Consistent theory✝¹
maximal✝¹ : ∀ {U : Theory α}, theory✝¹ ⊂ U → ¬(L)-Consistent U
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h :
  { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ }.theory =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory
⊢ { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ } =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
case mpr.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω : MCT L
p : Formula α
theory✝¹ : Theory α
consistent✝¹ : (L)-Consistent theory✝¹
maximal✝¹ : ∀ {U : Theory α}, theory✝¹ ⊂ U → ¬(L)-Consistent U
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h :
  { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ }.theory =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory
⊢ { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ } =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
⊢ Ω₁ = Ω₂
Tactic:
exact equality_def.mpr $ Set.eq_of_subset_of_subset
  (by intro p hp; exact h p hp)
  (by
    intro p;
    contrapose;
    intro hp;
    apply iff_mem_neg.mp;
    apply h;
    apply iff_mem_neg.mpr hp;
  )
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
⊢ Ω₁.theory ⊆ Ω₂.theory
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∈ Ω₁.theory
⊢ p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∈ Ω₁.theory
⊢ p ∈ Ω₂.theory
Tactic:
exact h p hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
⊢ Ω₂.theory ⊆ Ω₁.theory
Tactic:
intro p
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∈ Ω₂.theory → p ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∈ Ω₂.theory → p ∈ Ω₁.theory
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∉ Ω₁.theory → p ∉ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∉ Ω₁.theory → p ∉ Ω₂.theory
Tactic:
intro hp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ p ∉ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ p ∉ Ω₂.theory
Tactic:
apply iff_mem_neg.mp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₂.theory
Tactic:
apply h
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.intro_equality
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₁.theory
Tactic:
apply iff_mem_neg.mpr hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.neg_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
⊢ ~p ∈ Ω₁.theory → ~q ∈ Ω₂.theory
Tactic:
contrapose
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
⊢ ~q ∉ Ω₂.theory → ~p ∉ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.neg_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
⊢ ~q ∉ Ω₂.theory → ~p ∉ Ω₁.theory
Tactic:
intro hq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ ~p ∉ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.neg_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ ~p ∉ Ω₁.theory
Tactic:
apply iff_mem_neg.mp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ ~~p ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.neg_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ ~~p ∈ Ω₁.theory
Tactic:
apply mem_dn_iff.mp
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ p ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.neg_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ p ∈ Ω₁.theory
Tactic:
apply h
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ q ∈ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.neg_imp
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
h : q ∈ Ω₂.theory → p ∈ Ω₁.theory
hq : ~q ∉ Ω₂.theory
⊢ q ∈ Ω₂.theory
Tactic:
exact mem_dn_iff.mpr $ iff_mem_neg.mpr hq
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n](~~p) ∈ Ω.theory ↔ □^[n]p ∈ Ω.theory
Tactic:
simp only [iff_mem_multibox]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory) ↔
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory) ↔
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory
Tactic:
. intro h Ω hΩ; exact iff_mem_negneg.mp $ h hΩ;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory
Tactic:
. intro h Ω hΩ; exact iff_mem_negneg.mpr $ h hΩ;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
intro h Ω hΩ
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω✝.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory
Ω : MCT L
hΩ : □''⁻¹^[n]Ω✝.theory ⊆ Ω.theory
⊢ p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω✝.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory
Ω : MCT L
hΩ : □''⁻¹^[n]Ω✝.theory ⊆ Ω.theory
⊢ p ∈ Ω.theory
Tactic:
exact iff_mem_negneg.mp $ h hΩ
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory
Tactic:
intro h Ω hΩ
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω✝.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Ω : MCT L
hΩ : □''⁻¹^[n]Ω✝.theory ⊆ Ω.theory
⊢ ~~p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_dn_iff
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω✝.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Ω : MCT L
hΩ : □''⁻¹^[n]Ω✝.theory ⊆ Ω.theory
⊢ ~~p ∈ Ω.theory
Tactic:
exact iff_mem_negneg.mpr $ h hΩ
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∈ Ω.theory ↔ ~(◇^[n](~p)) ∈ Ω.theory
Tactic:
simp [membership_iff]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p ↔ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p ↔ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p → Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p → Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p
Tactic:
. intro h;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h;
  apply Context.provable_iff.mpr;
  existsi Γ;
  constructor;
  . assumption;
  . exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₁'! multiboxDuality!);
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p
Tactic:
. intro h;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h;
  apply Context.provable_iff.mpr;
  existsi Γ;
  constructor;
  . assumption;
  . exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₂'! multiboxDuality!);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p → Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h
Proof state after:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
apply Context.provable_iff.mpr
Proof state after:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
existsi Γ
Proof state after:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ (∀ q ∈ Γ, q ∈ Ω.theory) ∧ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ (∀ q ∈ Γ, q ∈ Ω.theory) ∧ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
constructor
Proof state after:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∀ q ∈ Γ, q ∈ Ω.theory

case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∀ q ∈ Γ, q ∈ Ω.theory

case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
. assumption;
Proof state after:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
. exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₁'! multiboxDuality!);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∀ q ∈ Γ, q ∈ Ω.theory
Tactic:
assumption
Proof state after:
no goals