internlm/Lean-Github huggingface dataset:
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 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
Proof state after:
case mpr
α : 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 mpr
α : 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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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 mpr.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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual
Proof state before:
case mpr.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_multidia_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_multidia_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_multidia_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₁'! multidiaDuality!);
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_multidia_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₂'! multidiaDuality!);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multidia_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_multidia_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_multidia_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_multidia_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_multidia_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_multidia_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_multidia_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₁'! multidiaDuality!);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multidia_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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multidia_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₁'! multidiaDuality!)
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multidia_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
Proof state after:
case mpr
α : 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_multidia_dual
Proof state before:
case mpr
α : 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 mpr.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_multidia_dual
Proof state before:
case mpr.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 mpr.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_multidia_dual
Proof state before:
case mpr.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 mpr.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_multidia_dual
Proof state before:
case mpr.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 mpr.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 mpr.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_multidia_dual
Proof state before:
case mpr.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 mpr.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 mpr.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_multidia_dual
Proof state before:
case mpr.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₂'! multidiaDuality!);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multidia_dual
Proof state before:
case mpr.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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multidia_dual
Proof state before:
case mpr.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₂'! multidiaDuality!)
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.multibox_multidia
Proof state before:
α : 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:
constructor
Proof state after:
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

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
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

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 H;
  apply mem_dn_iff.mpr;
  apply (neg_iff $ mem_multidia_dual).mp;
  exact iff_mem_neg.mpr h;
Proof state after:
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