internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory) → ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
. intro H p;
  contrapose;
  intro h;
  apply iff_mem_neg.mp;
  apply (neg_iff $ mem_multibox_dual).mpr;
  apply iff_mem_negneg.mpr;
  apply H;
  exact iff_mem_neg.mpr h;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
Tactic:
intro H p
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
⊢ p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
⊢ p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
Tactic:
contrapose
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
⊢ ◇^[n]p ∉ Ω₁.theory → p ∉ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
⊢ ◇^[n]p ∉ Ω₁.theory → p ∉ Ω₂.theory
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 : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ p ∉ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ p ∉ Ω₂.theory
Tactic:
apply iff_mem_neg.mp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ ~p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ ~p ∈ Ω₂.theory
Tactic:
apply H
Proof state after:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ □^[n](~p) ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ □^[n](~p) ∈ Ω₁.theory
Tactic:
apply mem_dn_iff.mpr
Proof state after:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ ~~(□^[n](~p)) ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ ~~(□^[n](~p)) ∈ Ω₁.theory
Tactic:
apply (neg_iff $ mem_multidia_dual).mp
Proof state after:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ ~(◇^[n]p) ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
p : Formula α
h : ◇^[n]p ∉ Ω₁.theory
⊢ ~(◇^[n]p) ∈ Ω₁.theory
Tactic:
exact iff_mem_neg.mpr h
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory) → ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
intro H p
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
⊢ □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
⊢ □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
contrapose
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
⊢ p ∉ Ω₂.theory → □^[n]p ∉ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
⊢ p ∉ Ω₂.theory → □^[n]p ∉ Ω₁.theory
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ □^[n]p ∉ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ □^[n]p ∉ Ω₁.theory
Tactic:
apply iff_mem_neg.mp
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ~(□^[n]p) ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ~(□^[n]p) ∈ Ω₁.theory
Tactic:
apply (neg_iff $ mem_multibox_dual).mpr
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ~~(◇^[n](~p)) ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ~~(◇^[n](~p)) ∈ Ω₁.theory
Tactic:
apply iff_mem_negneg.mpr
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ◇^[n](~p) ∈ Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ◇^[n](~p) ∈ Ω₁.theory
Tactic:
apply H
Proof state after:
case mpr.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ~p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
case mpr.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
n : ℕ
H : ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory
p : Formula α
h : p ∉ Ω₂.theory
⊢ ~p ∈ Ω₂.theory
Tactic:
exact iff_mem_neg.mpr h
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_conj'
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
⊢ Γ.conj' ∈ Ω.theory ↔ ∀ p ∈ Γ, p ∈ Ω.theory
Tactic:
simp [membership_iff, iff_provable_list_conj]
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ □^[n]Γ.conj' ∈ Ω.theory ↔ ∀ p ∈ Γ, □^[n]p ∈ Ω.theory
Tactic:
simp only [iff_mem_multibox, iff_mem_conj']
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) ↔
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) ↔
    ∀ p ∈ Γ, ∀ {Ω' : 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 α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) →
    ∀ p ∈ Γ, ∀ {Ω' : 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 α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) →
    ∀ p ∈ Γ, ∀ {Ω' : 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 α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Tactic:
. intro h p hp Ω' hΩ';
  exact (h hΩ') p hp;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Tactic:
. intro h Ω' hΩ' p hp;
  exact @h p hp Ω' hΩ';
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) →
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
intro h p hp Ω' hΩ'
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
p : Formula α
hp : p ∈ Γ
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
p : Formula α
hp : p ∈ Γ
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory
Tactic:
exact (h hΩ') p hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Tactic:
intro h Ω' hΩ' p hp
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
p : Formula α
hp : p ∈ Γ
⊢ p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox_conj'
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
p : Formula α
hp : p ∈ Γ
⊢ p ∈ Ω'.theory
Tactic:
exact @h p hp Ω' hΩ'
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.frame_def_box
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (CanonicalFrame L).Rel Ω₁ Ω₂ ↔ ∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
induction n generalizing Ω₁ Ω₂ with
| zero =>
  simp_all;
  constructor;
  . intro h; subst h; tauto;
  . intro h; apply intro_equality; simpa;
| succ n ih =>
  constructor;
  . simp;
    intro Ω₃ h₁₃ h₃₂ p h;
    exact ih.mp h₃₂ $ h₁₃ h;
  . intro h;
    obtain ⟨Ω, hΩ⟩ := lindenbaum (L := L) (T := (□''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory)) $ by
      apply intro_union_ParametricConsistent;
      intro Γ Δ hΓ hΔ hC;
      replace hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory := by simpa using hΓ;
      have dΓconj : Ω₁.theory *⊢[L]! □Γ.conj' := membership_iff.mp $ iff_mem_box_conj'.mpr hΓ;
      have hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory := by
        intro p hp;
        simpa using hΔ (◇^[n]p) (by simp_all);
      have hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory := iff_mem_conj'.mpr hΔ₂;
      have : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj') := imp_trans! (andImplyIffImplyImply'!.mp hC)
        $ contra₂'! $ imp_trans! (conj₂'! multidiaDuality!)
        $ imp_trans! iff_conj'multidia_multidiaconj'! $ by
          apply conj'conj'_subset;
          intro q hq;
          obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
          subst_vars;
          simpa;
      have : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj') := by simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this;
      have : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory := iff_mem_neg.mp $ h $ membership_iff.mpr $ (Context.of! this) ⨀ dΓconj;
      contradiction;
    existsi Ω;
    constructor;
    . intro p hp;
      apply hΩ;
      simp_all;
    . apply ih.mpr;
      apply multibox_multidia.mpr;
      intro p hp;
      apply hΩ;
      simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[0] Ω₂ ↔ ∀ {p : Formula α}, □^[0]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
simp_all
Proof state after:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ ↔ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ ↔ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
constructor
Proof state after:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ → ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory

case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ → ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory

case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂
Tactic:
. intro h; subst h; tauto;
Proof state after:
case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂
Tactic:
. intro h; apply intro_equality; simpa;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ → ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
intro h
Proof state after:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ = Ω₂
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ = Ω₂
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
subst h
Proof state after:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ : (CanonicalFrame L).World
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₁.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ : (CanonicalFrame L).World
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₁.theory
Tactic:
tauto
Proof state after:
no goals