internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋎ q ∈ Ω.theory ↔ 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 α
⊢ p ⋎ q ∈ Ω.theory → p ∈ Ω.theory ∨ q ∈ Ω.theory

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

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
Tactic:
. intro hpq;
  replace hpq := membership_iff.mp hpq;
  by_contra hC; simp [not_or] at hC;
  have ⟨hp, hq⟩ := hC;
  replace hp := membership_iff.mp $ iff_mem_neg.mpr hp;
  replace hq := membership_iff.mp $ iff_mem_neg.mpr hq;
  have : Ω.theory *⊢[L]! ⊥ := disj₃'! hp hq hpq;
  have : Ω.theory *⊬[L]! ⊥ := unprovable_falsum;
  contradiction;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
Tactic:
. rintro (hp | hq);
  . apply membership_iff.mpr;
    exact disj₁'! (membership_iff.mp hp);
  . apply membership_iff.mpr;
    exact disj₂'! (membership_iff.mp hq);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋎ q ∈ Ω.theory → p ∈ Ω.theory ∨ q ∈ Ω.theory
Tactic:
intro hpq
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⋎ q ∈ Ω.theory
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hpq : p ⋎ q ∈ Ω.theory
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory
Tactic:
replace hpq := membership_iff.mp hpq
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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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:
by_contra hC
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
hC : ¬(p ∈ Ω.theory ∨ q ∈ Ω.theory)
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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
hC : ¬(p ∈ Ω.theory ∨ q ∈ Ω.theory)
⊢ False
Tactic:
simp [not_or] at hC
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
⊢ False
Tactic:
have ⟨hp, hq⟩ := hC
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : p ∉ Ω.theory
hq : q ∉ Ω.theory
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : p ∉ Ω.theory
hq : q ∉ Ω.theory
⊢ False
Tactic:
replace hp := membership_iff.mp $ iff_mem_neg.mpr 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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hq : q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hq : q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
⊢ False
Tactic:
replace hq := membership_iff.mp $ iff_mem_neg.mpr hq
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
⊢ False
Tactic:
have : Ω.theory *⊢[L]! ⊥ := disj₃'! hp hq hpq
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
this : Ω.theory *⊢[L]! ⊥
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
this : Ω.theory *⊢[L]! ⊥
⊢ False
Tactic:
have : Ω.theory *⊬[L]! ⊥ := unprovable_falsum
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
this✝ : Ω.theory *⊢[L]! ⊥
this : Ω.theory *⊬[L]! ⊥
⊢ False
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
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
hC : p ∉ Ω.theory ∧ q ∉ Ω.theory
hp : Ω.theory *⊢[L]! ~p
hq : Ω.theory *⊢[L]! ~q
this✝ : Ω.theory *⊢[L]! ⊥
this : Ω.theory *⊬[L]! ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
Tactic:
rintro (hp | hq)
Proof state after:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory

case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory

case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
. apply membership_iff.mpr;
  exact disj₁'! (membership_iff.mp hp);
Proof state after:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
. apply membership_iff.mpr;
  exact disj₂'! (membership_iff.mp hq);
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hp : p ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q
Tactic:
exact disj₁'! (membership_iff.mp hp)
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ p ⋎ q ∈ Ω.theory
Tactic:
apply membership_iff.mpr
Proof state after:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_or
Proof state before:
case mpr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
hq : q ∈ Ω.theory
⊢ Ω.theory *⊢[L]! p ⋎ q
Tactic:
exact disj₂'! (membership_iff.mp hq)
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 : ℕ
⊢ □^[n]p ∈ Ω.theory ↔ ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) → □^[n]p ∈ Ω.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) → □^[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]
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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Ω'
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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Ω'
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) → □^[n]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 : ℕ
⊢ □^[n]p ∉ Ω.theory → ¬∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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;
)
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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 Ω'
Proof 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
Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_multibox
Proof 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
Proof 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
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

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Ω';
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 iff_mem_neg.mp;
  apply hΩ';
  simp only [Set.mem_insert_iff, true_or]
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
⊢ (L)-Consistent insert (~p) (□''⁻¹^[n]Ω.theory)
Tactic:
apply unprovable_iff_insert_neg_ParametricConsistent.mp
Proof 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
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
⊢ (□''⁻¹^[n]Ω.theory) *⊬[L]! p
Tactic:
by_contra hC
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
⊢ False
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
⊢ False
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp hC
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
⊢ False