internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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Γ₂
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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'!;
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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₁;
)
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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]
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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'!
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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;
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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₂
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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₁
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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Ω'
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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Ω'
Proof 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)
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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]
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ Ω.theory *⊢[L]! p ⟷ q → (p ∈ Ω.theory ↔ q ∈ Ω.theory)
Tactic:
intro hpq
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ p ∈ Ω.theory ↔ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ p ∈ Ω.theory ↔ q ∈ Ω.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ p ∈ Ω.theory → q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ q ∈ Ω.theory → p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ p ∈ Ω.theory → q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ q ∈ Ω.theory → p ∈ Ω.theory
Tactic:
. intro hp; exact iff_mem_imp.mp (membership_iff.mpr $ conj₁'! hpq) hp;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ q ∈ Ω.theory → p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ q ∈ Ω.theory → p ∈ Ω.theory
Tactic:
. intro hq; exact iff_mem_imp.mp (membership_iff.mpr $ conj₂'! hpq) hq;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ p ∈ Ω.theory → q ∈ Ω.theory
Tactic:
intro hp
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
hp : p ∈ Ω.theory
⊢ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
hp : p ∈ Ω.theory
⊢ q ∈ Ω.theory
Tactic:
exact iff_mem_imp.mp (membership_iff.mpr $ conj₁'! hpq) hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
⊢ q ∈ Ω.theory → p ∈ Ω.theory
Tactic:
intro hq
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
hq : q ∈ Ω.theory
⊢ p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_congr
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : Ω.theory *⊢[L]! p ⟷ q
hq : q ∈ Ω.theory
⊢ p ∈ Ω.theory
Tactic:
exact iff_mem_imp.mp (membership_iff.mpr $ conj₂'! hpq) hq
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ ↔ Ω₁.theory = Ω₂.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ → Ω₁.theory = Ω₂.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ → Ω₁.theory = Ω₂.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂
Tactic:
. intro h; cases h; rfl;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂
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 α
⊢ Ω₁.theory = Ω₂.theory → Ω₁ = Ω₂
Tactic:
. intro h; cases Ω₁; cases Ω₂; simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω₁ = Ω₂ → Ω₁.theory = Ω₂.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 α
h : Ω₁ = Ω₂
⊢ Ω₁.theory = Ω₂.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω₁ = Ω₂
⊢ Ω₁.theory = Ω₂.theory
Tactic:
cases h
Proof state after:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₁.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.equality_def
Proof state before:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ : MCT L
p : Formula α
⊢ Ω₁.theory = Ω₁.theory
Tactic:
rfl
Proof state after:
no goals
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 α
⊢ Ω₁.theory = Ω₂.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 α
h : Ω₁.theory = Ω₂.theory
⊢ Ω₁ = Ω₂