Documentation

LeanPool.Incompleteness.Foundation.Modal.MaximalConsistentSet

MaximalConsistentSet #

source
@[reducible, inline]
abbrev LO.Modal.FormulaSet.Consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] (𝓒 : S) (T : FormulaSet Ξ±) :
Prop

Imported declaration from the Incompleteness formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.FormulaSet.Inconsistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] (𝓒 : S) (T : FormulaSet Ξ±) :
    Prop

    Imported declaration from the Incompleteness formalization.

    Equations
    Instances For
      source
      theorem LO.Modal.FormulaSet.def_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} :
      Consistent 𝓒 T ↔ βˆ€ (Ξ“ : List (Formula Ξ±)), (βˆ€ ψ ∈ Ξ“, ψ ∈ T) β†’ Ξ“ ⊬[𝓒] βŠ₯
      source
      theorem LO.Modal.FormulaSet.def_inconsistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} :
      Inconsistent 𝓒 T ↔ βˆƒ (Ξ“ : List (Formula Ξ±)), (βˆ€ ψ ∈ Ξ“, ψ ∈ T) ∧ Ξ“ ⊒[𝓒]! βŠ₯
      source
      theorem LO.Modal.FormulaSet.union_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T₁ Tβ‚‚ : FormulaSet Ξ±} :
      Consistent 𝓒 (T₁ βˆͺ Tβ‚‚) β†’ Consistent 𝓒 T₁ ∧ Consistent 𝓒 Tβ‚‚
      source
      theorem LO.Modal.FormulaSet.emptyset_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} [Entailment.Classical 𝓒] [H_consis : Entailment.Consistent 𝓒] :
      Consistent 𝓒 βˆ…
      source
      theorem LO.Modal.FormulaSet.not_mem_of_mem_neg {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} (T_consis : Consistent 𝓒 T) (h : βˆΌΟ† ∈ T) :
      Ο† βˆ‰ T
      source
      theorem LO.Modal.FormulaSet.not_mem_neg_of_mem {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} (T_consis : Consistent 𝓒 T) (h : Ο† ∈ T) :
      βˆΌΟ† βˆ‰ T
      source
      theorem LO.Modal.FormulaSet.iff_insert_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Consistent 𝓒 (insert Ο† T) ↔ βˆ€ {Ξ“ : List (Formula Ξ±)}, (βˆ€ ψ ∈ Ξ“, ψ ∈ T) β†’ 𝓒 ⊬ Ο† ⋏ β‹€Ξ“ ==> βŠ₯
      source
      theorem LO.Modal.FormulaSet.iff_insert_inconsistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Inconsistent 𝓒 (insert Ο† T) ↔ βˆƒ (Ξ“ : List (Formula Ξ±)), (βˆ€ Ο† ∈ Ξ“, Ο† ∈ T) ∧ 𝓒 ⊒! Ο† ⋏ β‹€Ξ“ ==> βŠ₯
      source
      theorem LO.Modal.FormulaSet.provable_iff_insert_neg_not_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Inconsistent 𝓒 (insert (βˆΌΟ†) T) ↔ T *⊒[𝓒]! Ο†
      source
      theorem LO.Modal.FormulaSet.unprovable_iff_insert_neg_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Consistent 𝓒 (insert (βˆΌΟ†) T) ↔ T *⊬[𝓒] Ο†
      source
      theorem LO.Modal.FormulaSet.unprovable_iff_singleton_neg_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Consistent 𝓒 {βˆΌΟ†} ↔ 𝓒 ⊬ Ο†
      source
      theorem LO.Modal.FormulaSet.neg_provable_iff_insert_not_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Inconsistent 𝓒 (insert Ο† T) ↔ T *⊒[𝓒]! βˆΌΟ†
      source
      theorem LO.Modal.FormulaSet.neg_unprovable_iff_insert_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Consistent 𝓒 (insert Ο† T) ↔ T *⊬[𝓒] βˆΌΟ†
      source
      theorem LO.Modal.FormulaSet.unprovable_iff_singleton_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} :
      Consistent 𝓒 {Ο†} ↔ 𝓒 ⊬ βˆΌΟ†
      source
      theorem LO.Modal.FormulaSet.unprovable_either {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} (T_consis : Consistent 𝓒 T) :
      Β¬(T *⊒[𝓒]! Ο† ∧ T *⊒[𝓒]! βˆΌΟ†)
      source
      theorem LO.Modal.FormulaSet.not_mem_falsum_of_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] (T_consis : Consistent 𝓒 T) :
      βŠ₯ βˆ‰ T
      source
      theorem LO.Modal.FormulaSet.not_singleton_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] {Ο† : Formula Ξ±} [Entailment.Necessitation 𝓒] (T_consis : Consistent 𝓒 T) (h : βˆΌβ–‘Ο† ∈ T) :
      Consistent 𝓒 {βˆΌΟ†}
      source
      theorem LO.Modal.FormulaSet.either_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} [Entailment.Classical 𝓒] (T_consis : Consistent 𝓒 T) (Ο† : Formula Ξ±) :
      Consistent 𝓒 (insert Ο† T) ∨ Consistent 𝓒 (insert (βˆΌΟ†) T)
      source
      theorem LO.Modal.FormulaSet.intro_union_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} [Entailment.Classical 𝓒] {T₁ Tβ‚‚ : FormulaSet Ξ±} (h : βˆ€ {Γ₁ Ξ“β‚‚ : List (Formula Ξ±)}, ((βˆ€ Ο† ∈ Γ₁, Ο† ∈ T₁) ∧ βˆ€ Ο† ∈ Ξ“β‚‚, Ο† ∈ Tβ‚‚) β†’ 𝓒 ⊬ ⋀Γ₁ ⋏ β‹€Ξ“β‚‚ ==> βŠ₯) :
      Consistent 𝓒 (T₁ βˆͺ Tβ‚‚)
      source
      theorem LO.Modal.FormulaSet.intro_triunion_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} [Entailment.Classical 𝓒] {T₁ Tβ‚‚ T₃ : FormulaSet Ξ±} (h : βˆ€ {Γ₁ Ξ“β‚‚ Γ₃ : List (Formula Ξ±)}, ((βˆ€ Ο† ∈ Γ₁, Ο† ∈ T₁) ∧ (βˆ€ Ο† ∈ Ξ“β‚‚, Ο† ∈ Tβ‚‚) ∧ βˆ€ Ο† ∈ Γ₃, Ο† ∈ T₃) β†’ 𝓒 ⊬ ⋀Γ₁ ⋏ β‹€Ξ“β‚‚ ⋏ ⋀Γ₃ ==> βŠ₯) :
      Consistent 𝓒 (T₁ βˆͺ Tβ‚‚ βˆͺ T₃)
      source
      theorem LO.Modal.FormulaSet.exists_consistent_maximal_of_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} (T_consis : Consistent 𝓒 T) :
      βˆƒ (Z : FormulaSet Ξ±), Consistent 𝓒 Z ∧ T βŠ† Z ∧ βˆ€ (U : Set (Formula Ξ±)), U *⊬[𝓒] βŠ₯ β†’ Z βŠ† U β†’ U = Z
      source
      theorem LO.Modal.FormulaSet.lindenbaum {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} (T_consis : Consistent 𝓒 T) :
      βˆƒ (Z : FormulaSet Ξ±), Consistent 𝓒 Z ∧ T βŠ† Z ∧ βˆ€ (U : Set (Formula Ξ±)), U *⊬[𝓒] βŠ₯ β†’ Z βŠ† U β†’ U = Z

      Alias of LO.Modal.FormulaSet.exists_consistent_maximal_of_consistent.

      source
      @[reducible, inline]
      abbrev LO.Modal.MaximalConsistentSet {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] (𝓒 : S) :
      Type u_1

      Imported declaration from the Incompleteness formalization.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance LO.Modal.MaximalConsistentSet.instMembershipFormula {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} :
        Membership (Formula Ξ±) (MaximalConsistentSet 𝓒)
        Equations
        source
        theorem LO.Modal.MaximalConsistentSet.consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} (Ξ© : MaximalConsistentSet 𝓒) :
        FormulaSet.Consistent 𝓒 ↑Ω
        source
        theorem LO.Modal.MaximalConsistentSet.maximal {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {U : FormulaSet Ξ±} (Ξ© : MaximalConsistentSet 𝓒) :
        ↑Ω βŠ‚ U β†’ FormulaSet.Inconsistent 𝓒 U
        source
        theorem LO.Modal.MaximalConsistentSet.maximal' {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} (Ξ© : MaximalConsistentSet 𝓒) {Ο† : Formula Ξ±} (hp : Ο† βˆ‰ Ξ©) :
        FormulaSet.Inconsistent 𝓒 (insert Ο† ↑Ω)
        source
        theorem LO.Modal.MaximalConsistentSet.equality_def {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ω₁ Ξ©β‚‚ : MaximalConsistentSet 𝓒} :
        Ω₁ = Ξ©β‚‚ ↔ ↑Ω₁ = ↑Ω₂
        source
        theorem LO.Modal.MaximalConsistentSet.exists_of_consistent {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} (consisT : FormulaSet.Consistent 𝓒 T) :
        βˆƒ (Ξ© : MaximalConsistentSet 𝓒), T βŠ† ↑Ω
        source
        theorem LO.Modal.MaximalConsistentSet.lindenbaum {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {T : FormulaSet Ξ±} (consisT : FormulaSet.Consistent 𝓒 T) :
        βˆƒ (Ξ© : MaximalConsistentSet 𝓒), T βŠ† ↑Ω

        Alias of LO.Modal.MaximalConsistentSet.exists_of_consistent.

        source
        instance LO.Modal.MaximalConsistentSet.instNonemptyOfConsistentFormula {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} [Entailment.Classical 𝓒] [Entailment.Consistent 𝓒] :
        Nonempty (MaximalConsistentSet 𝓒)
        source
        theorem LO.Modal.MaximalConsistentSet.either_mem {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} [Entailment.Classical 𝓒] (Ξ© : MaximalConsistentSet 𝓒) (Ο† : Formula Ξ±) :
        Ο† ∈ Ξ© ∨ βˆΌΟ† ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.membership_iff {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] :
        Ο† ∈ Ξ© ↔ ↑Ω *⊒[𝓒]! Ο†
        source
        @[simp]
        theorem LO.Modal.MaximalConsistentSet.not_mem_falsum {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} [Entailment.Classical 𝓒] :
        βŠ₯ βˆ‰ Ξ©
        source
        @[simp]
        theorem LO.Modal.MaximalConsistentSet.mem_verum {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} [Entailment.Classical 𝓒] :
        ⊀ ∈ Ω
        source
        @[simp]
        theorem LO.Modal.MaximalConsistentSet.iff_mem_neg {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] :
        βˆΌΟ† ∈ Ξ© ↔ Ο† βˆ‰ Ξ©
        source
        @[simp]
        theorem LO.Modal.MaximalConsistentSet.iff_mem_negneg {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] :
        βˆΌβˆΌΟ† ∈ Ξ© ↔ Ο† ∈ Ξ©
        source
        @[simp]
        theorem LO.Modal.MaximalConsistentSet.iff_mem_imp {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] {ψ : Formula Ξ±} :
        Ο† ==> ψ ∈ Ξ© ↔ Ο† ∈ Ξ© β†’ ψ ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.mdp {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] {ψ : Formula Ξ±} (hΟ†Οˆ : Ο† ==> ψ ∈ Ξ©) (hψ : Ο† ∈ Ξ©) :
        ψ ∈ Ω
        source
        @[simp]
        theorem LO.Modal.MaximalConsistentSet.iff_mem_and {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] {ψ : Formula Ξ±} :
        Ο† ⋏ ψ ∈ Ξ© ↔ Ο† ∈ Ξ© ∧ ψ ∈ Ξ©
        source
        @[simp]
        theorem LO.Modal.MaximalConsistentSet.iff_mem_or {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] {ψ : Formula Ξ±} :
        Ο† β‹Ž ψ ∈ Ξ© ↔ Ο† ∈ Ξ© ∨ ψ ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.iff_congr {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] {ψ : Formula Ξ±} :
        ↑Ω *⊒[𝓒]! Ο† <=> ψ β†’ (Ο† ∈ Ξ© ↔ ψ ∈ Ξ©)
        source
        theorem LO.Modal.MaximalConsistentSet.intro_equality {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ω₁ Ξ©β‚‚ : MaximalConsistentSet 𝓒} [Entailment.Classical 𝓒] {h : βˆ€ Ο† ∈ ↑Ω₁, Ο† ∈ ↑Ω₂} :
        Ω₁ = Ξ©β‚‚
        source
        theorem LO.Modal.MaximalConsistentSet.neg_imp {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ω₁ Ξ©β‚‚ : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] {ψ : Formula Ξ±} (h : ψ ∈ Ξ©β‚‚ β†’ Ο† ∈ Ω₁) :
        βˆΌΟ† ∈ Ω₁ β†’ ∼ψ ∈ Ξ©β‚‚
        source
        theorem LO.Modal.MaximalConsistentSet.neg_iff {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ω₁ Ξ©β‚‚ : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.Classical 𝓒] {ψ : Formula Ξ±} (h : Ο† ∈ Ω₁ ↔ ψ ∈ Ξ©β‚‚) :
        βˆΌΟ† ∈ Ω₁ ↔ ∼ψ ∈ Ξ©β‚‚
        source
        theorem LO.Modal.MaximalConsistentSet.iff_mem_conj {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} [Entailment.Classical 𝓒] {Ξ“ : List (Formula Ξ±)} :
        β‹€Ξ“ ∈ Ξ© ↔ βˆ€ Ο† ∈ Ξ“, Ο† ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.iff_mem_multibox {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] {n : β„•} :
        β–‘^[n]Ο† ∈ Ξ© ↔ βˆ€ {Ξ©' : MaximalConsistentSet 𝓒}, β–‘''⁻¹^[n]↑Ω βŠ† ↑Ω' β†’ Ο† ∈ Ξ©'
        source
        theorem LO.Modal.MaximalConsistentSet.iff_mem_box {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] :
        β–‘Ο† ∈ Ξ© ↔ βˆ€ {Ξ©' : MaximalConsistentSet 𝓒}, β–‘''⁻¹↑Ω βŠ† ↑Ω' β†’ Ο† ∈ Ξ©'
        source
        theorem LO.Modal.MaximalConsistentSet.multibox_dn_iff {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] {n : β„•} :
        β–‘^[n](βˆΌβˆΌΟ†) ∈ Ξ© ↔ β–‘^[n]Ο† ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.box_dn_iff {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] :
        β–‘(βˆΌβˆΌΟ†) ∈ Ξ© ↔ β–‘Ο† ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.mem_multibox_dual {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] {n : β„•} :
        β–‘^[n]Ο† ∈ Ξ© ↔ βˆΌβ—‡^[n](βˆΌΟ†) ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.mem_box_dual {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] :
        β–‘Ο† ∈ Ξ© ↔ βˆΌβ—‡(βˆΌΟ†) ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.mem_multidia_dual {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] {n : β„•} :
        β—‡^[n]Ο† ∈ Ξ© ↔ βˆΌβ–‘^[n](βˆΌΟ†) ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.mem_dia_dual {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] :
        β—‡Ο† ∈ Ξ© ↔ βˆΌβ–‘(βˆΌΟ†) ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.iff_mem_multidia {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] {n : β„•} :
        β—‡^[n]Ο† ∈ Ξ© ↔ βˆƒ (Ξ©' : MaximalConsistentSet 𝓒), β–‘''⁻¹^[n]↑Ω βŠ† ↑Ω' ∧ Ο† ∈ ↑Ω'
        source
        theorem LO.Modal.MaximalConsistentSet.iff_mem_dia {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} {Ο† : Formula Ξ±} [Entailment.K 𝓒] :
        β—‡Ο† ∈ Ξ© ↔ βˆƒ (Ξ©' : MaximalConsistentSet 𝓒), β–‘''⁻¹↑Ω βŠ† ↑Ω' ∧ Ο† ∈ ↑Ω'
        source
        theorem LO.Modal.MaximalConsistentSet.multibox_multidia {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ω₁ Ξ©β‚‚ : MaximalConsistentSet 𝓒} [Entailment.K 𝓒] {n : β„•} :
        (βˆ€ {Ο† : Formula Ξ±}, β–‘^[n]Ο† ∈ ↑Ω₁ β†’ Ο† ∈ ↑Ω₂) ↔ βˆ€ {Ο† : Formula Ξ±}, Ο† ∈ ↑Ω₂ β†’ β—‡^[n]Ο† ∈ ↑Ω₁
        source
        theorem LO.Modal.MaximalConsistentSet.iff_mem_multibox_conj {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} [Entailment.K 𝓒] {Ξ“ : List (Formula Ξ±)} {n : β„•} :
        β–‘^[n]β‹€Ξ“ ∈ Ξ© ↔ βˆ€ Ο† ∈ Ξ“, β–‘^[n]Ο† ∈ Ξ©
        source
        theorem LO.Modal.MaximalConsistentSet.iff_mem_box_conj {Ξ± : Type u_1} {S : Type u_2} [Entailment (Formula Ξ±) S] {𝓒 : S} {Ξ© : MaximalConsistentSet 𝓒} [Entailment.K 𝓒] {Ξ“ : List (Formula Ξ±)} :
        β–‘β‹€Ξ“ ∈ Ξ© ↔ βˆ€ Ο† ∈ Ξ“, β–‘Ο† ∈ Ξ©