Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∈ Ω.theory ↔ ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]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) → □^[n]p ∈ Ω.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]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) → □^[n]p ∈ Ω.theory
Tactic:
. intro hp Ω' hΩ'; apply hΩ'; simpa;
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) → □^[n]p ∈ Ω.theory

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) → □^[n]p ∈ Ω.theory
Tactic:
. contrapose;
  push_neg;
  intro hp;
  obtain ⟨Ω', hΩ'⟩ := lindenbaum (L := L) (T := insert (~p) (□''⁻¹^[n]Ω.theory)) (by
    apply unprovable_iff_insert_neg_ParametricConsistent.mp;
    by_contra hC;
    obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp hC;
    have : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p := imply_multibox_distribute'! $ implyLeft_conj_eq_conj'!.mp hΓ₂;
    have : L ⊬! □^[n]Γ.conj' ⟶ □^[n]p := by
      have := Context.provable_iff.not.mp $ membership_iff.not.mp hp;
      push_neg at this;
      have : L ⊬! (□'^[n]Γ : List (Formula α)).conj' ⟶ □^[n]p := implyLeft_conj_eq_conj'!.not.mp $ FiniteContext.provable_iff.not.mp $ this (□'^[n]Γ) (by
        intro q hq;
        obtain ⟨r, hr₁, hr₂⟩ := by simpa using hq;
        subst hr₂;
        simpa using hΓ₁ r hr₁;
      );
      revert this;
      contrapose;
      simp [neg_neg];
      exact imp_trans! collect_multibox_conj'!;
    contradiction;
  );
  existsi Ω';
  constructor;
  . exact Set.Subset.trans (by simp_all) hΩ';
  . apply iff_mem_neg.mp;
    apply hΩ';
    simp only [Set.mem_insert_iff, true_or]
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∈ Ω.theory → ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
intro hp Ω' hΩ'
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∈ Ω.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∈ Ω.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory
Tactic:
apply hΩ'
State after:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∈ Ω.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ □''⁻¹^[n]Ω.theory

State before:
case mp.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∈ Ω.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ □''⁻¹^[n]Ω.theory
Tactic:
simpa
State after:
no goals

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) → □^[n]p ∈ Ω.theory
Tactic:
contrapose
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∉ Ω.theory → ¬∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∉ Ω.theory → ¬∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
push_neg
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∉ Ω.theory → ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∉ Ω.theory → ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory
Tactic:
intro hp
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
⊢ ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
⊢ ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory
Tactic:
obtain ⟨Ω', hΩ'⟩ := lindenbaum (L := L) (T := insert (~p) (□''⁻¹^[n]Ω.theory)) (by
  apply unprovable_iff_insert_neg_ParametricConsistent.mp;
  by_contra hC;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp hC;
  have : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p := imply_multibox_distribute'! $ implyLeft_conj_eq_conj'!.mp hΓ₂;
  have : L ⊬! □^[n]Γ.conj' ⟶ □^[n]p := by
    have := Context.provable_iff.not.mp $ membership_iff.not.mp hp;
    push_neg at this;
    have : L ⊬! (□'^[n]Γ : List (Formula α)).conj' ⟶ □^[n]p := implyLeft_conj_eq_conj'!.not.mp $ FiniteContext.provable_iff.not.mp $ this (□'^[n]Γ) (by
      intro q hq;
      obtain ⟨r, hr₁, hr₂⟩ := by simpa using hq;
      subst hr₂;
      simpa using hΓ₁ r hr₁;
    );
    revert this;
    contrapose;
    simp [neg_neg];
    exact imp_trans! collect_multibox_conj'!;
  contradiction;
)
State after:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory

State before:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory
Tactic:
existsi Ω'
State after:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory

State before:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory
Tactic:
constructor
State after:
case mpr.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ □''⁻¹^[n]Ω.theory ⊆ Ω'.theory

case mpr.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ p ∉ Ω'.theory

State before:
case mpr.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ □''⁻¹^[n]Ω.theory ⊆ Ω'.theory

case mpr.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ p ∉ Ω'.theory
Tactic:
. exact Set.Subset.trans (by simp_all) hΩ';
State after:
case mpr.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ p ∉ Ω'.theory

State before:
case mpr.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ p ∉ Ω'.theory
Tactic:
. apply iff_mem_neg.mp;
  apply hΩ';
  simp only [Set.mem_insert_iff, true_or]
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
⊢ (L)-Consistent insert (~p) (□''⁻¹^[n]Ω.theory)
Tactic:
apply unprovable_iff_insert_neg_ParametricConsistent.mp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
⊢ (□''⁻¹^[n]Ω.theory) *⊬[L]! p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
⊢ (□''⁻¹^[n]Ω.theory) *⊬[L]! p
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
⊢ False
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp hC
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
⊢ False
Tactic:
have : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p := imply_multibox_distribute'! $ implyLeft_conj_eq_conj'!.mp hΓ₂
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
⊢ False
Tactic:
have : L ⊬! □^[n]Γ.conj' ⟶ □^[n]p := by
  have := Context.provable_iff.not.mp $ membership_iff.not.mp hp;
  push_neg at this;
  have : L ⊬! (□'^[n]Γ : List (Formula α)).conj' ⟶ □^[n]p := implyLeft_conj_eq_conj'!.not.mp $ FiniteContext.provable_iff.not.mp $ this (□'^[n]Γ) (by
    intro q hq;
    obtain ⟨r, hr₁, hr₂⟩ := by simpa using hq;
    subst hr₂;
    simpa using hΓ₁ r hr₁;
  );
  revert this;
  contrapose;
  simp [neg_neg];
  exact imp_trans! collect_multibox_conj'!;
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : L ⊬! □^[n]Γ.conj' ⟶ □^[n]p
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : L ⊬! □^[n]Γ.conj' ⟶ □^[n]p
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
⊢ L ⊬! □^[n]Γ.conj' ⟶ □^[n]p
Tactic:
have := Context.provable_iff.not.mp $ membership_iff.not.mp hp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ¬∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! □^[n]p
⊢ L ⊬! □^[n]Γ.conj' ⟶ □^[n]p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ¬∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! □^[n]p
⊢ L ⊬! □^[n]Γ.conj' ⟶ □^[n]p
Tactic:
push_neg at this
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ L ⊬! □^[n]Γ.conj' ⟶ □^[n]p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ L ⊬! □^[n]Γ.conj' ⟶ □^[n]p
Tactic:
have : L ⊬! (□'^[n]Γ : List (Formula α)).conj' ⟶ □^[n]p := implyLeft_conj_eq_conj'!.not.mp $ FiniteContext.provable_iff.not.mp $ this (□'^[n]Γ) (by
  intro q hq;
  obtain ⟨r, hr₁, hr₂⟩ := by simpa using hq;
  subst hr₂;
  simpa using hΓ₁ r hr₁;
)
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝¹ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this✝ : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
this : L ⊬! (□'^[n]Γ).conj' ⟶ □^[n]p
⊢ L ⊬! □^[n]Γ.conj' ⟶ □^[n]p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝¹ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this✝ : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
this : L ⊬! (□'^[n]Γ).conj' ⟶ □^[n]p
⊢ L ⊬! □^[n]Γ.conj' ⟶ □^[n]p
Tactic:
revert this
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ L ⊬! (□'^[n]Γ).conj' ⟶ □^[n]p → L ⊬! □^[n]Γ.conj' ⟶ □^[n]p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ L ⊬! (□'^[n]Γ).conj' ⟶ □^[n]p → L ⊬! □^[n]Γ.conj' ⟶ □^[n]p
Tactic:
contrapose
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ ¬L ⊬! □^[n]Γ.conj' ⟶ □^[n]p → ¬L ⊬! (□'^[n]Γ).conj' ⟶ □^[n]p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ ¬L ⊬! □^[n]Γ.conj' ⟶ □^[n]p → ¬L ⊬! (□'^[n]Γ).conj' ⟶ □^[n]p
Tactic:
simp [neg_neg]
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ L ⊢! □^[n]Γ.conj' ⟶ □^[n]p → L ⊢! (□'^[n]Γ).conj' ⟶ □^[n]p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ L ⊢! □^[n]Γ.conj' ⟶ □^[n]p → L ⊢! (□'^[n]Γ).conj' ⟶ □^[n]p
Tactic:
exact imp_trans! collect_multibox_conj'!
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
⊢ ∀ q ∈ □'^[n]Γ, q ∈ Ω.theory
Tactic:
intro q hq
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
q : Formula α
hq : q ∈ □'^[n]Γ
⊢ q ∈ Ω.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
q : Formula α
hq : q ∈ □'^[n]Γ
⊢ q ∈ Ω.theory
Tactic:
obtain ⟨r, hr₁, hr₂⟩ := by simpa using hq;
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
q : Formula α
hq : q ∈ □'^[n]Γ
r : Formula α
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop true)^[n] r = q
⊢ q ∈ Ω.theory

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
q : Formula α
hq : q ∈ □'^[n]Γ
r : Formula α
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop true)^[n] r = q
⊢ q ∈ Ω.theory
Tactic:
subst hr₂
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
r : Formula α
hr₁ : r ∈ Γ
hq : (UnaryModalOperator.mop true)^[n] r ∈ □'^[n]Γ
⊢ (UnaryModalOperator.mop true)^[n] r ∈ Ω.theory

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
r : Formula α
hr₁ : r ∈ Γ
hq : (UnaryModalOperator.mop true)^[n] r ∈ □'^[n]Γ
⊢ (UnaryModalOperator.mop true)^[n] r ∈ Ω.theory
Tactic:
simpa using hΓ₁ r hr₁
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
hC : { ctx := □''⁻¹^[n]Ω.theory } ⊢! p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ □''⁻¹^[n]Ω.theory
hΓ₂ : Γ ⊢[L]! p
this✝ : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p
this : ∀ (Δ : List (Formula α)), (∀ q ∈ Δ, q ∈ Ω.theory) → ¬Δ ⊢[L]! □^[n]p
q : Formula α
hq : q ∈ □'^[n]Γ
⊢ ?m.263209
Tactic:
simpa using hq
State after:
no goals

State before:
case mpr.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
Tactic:
exact Set.Subset.trans (by simp_all) hΩ'
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ □''⁻¹^[n]Ω.theory ⊆ insert (~p) (□''⁻¹^[n]Ω.theory)
Tactic:
simp_all
State after:
no goals

State before:
case mpr.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ p ∉ Ω'.theory
Tactic:
apply iff_mem_neg.mp
State after:
case mpr.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ ~p ∈ Ω'.theory

State before:
case mpr.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ ~p ∈ Ω'.theory
Tactic:
apply hΩ'
State after:
case mpr.intro.right.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ ~p ∈ insert (~p) (□''⁻¹^[n]Ω.theory)

State before:
case mpr.intro.right.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ ~p ∈ insert (~p) (□''⁻¹^[n]Ω.theory)
Tactic:
simp only [Set.mem_insert_iff, true_or]
State after:
no goals