Foundation.Modal.ConsistentTheory

source

@[reducible, inline]

abbrev LO.Modal.Theory.Consistent {α : Type u_1} (Λ : LO.Modal.Hilbert α) (T : LO.Modal.Theory α) :

Prop

Equations

LO.Modal.Theory.Consistent Λ T = T *⊬[Λ] ⊥

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Theory.Inconsistent {α : Type u_1} (Λ : LO.Modal.Hilbert α) (T : LO.Modal.Theory α) :

Prop

Equations

LO.Modal.Theory.Inconsistent Λ T = ¬LO.Modal.Theory.Consistent Λ T

Instances For

source

theorem LO.Modal.Theory.def_consistent {α : Type u_1} {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} :

LO.Modal.Theory.Consistent Λ T ↔ ∀ (Γ : List (LO.Modal.Formula α)), (∀ q ∈ Γ, q ∈ T) → Γ ⊬[Λ] ⊥

source

theorem LO.Modal.Theory.def_inconsistent {α : Type u_1} {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} :

¬LO.Modal.Theory.Consistent Λ T ↔ ∃ (Γ : List (LO.Modal.Formula α)), (∀ q ∈ Γ, q ∈ T) ∧ Γ ⊢[Λ]! ⊥

source

@[simp]

theorem LO.Modal.Theory.self_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Λ_consis : LO.System.Consistent Λ] :

LO.Modal.Theory.Consistent Λ Ax(Λ)

source

theorem LO.Modal.Theory.emptyset_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [Λ_consis : LO.System.Consistent Λ] :

LO.Modal.Theory.Consistent Λ ∅

source

theorem LO.Modal.Theory.union_consistent {α : Type u_1} {Λ : LO.Modal.Hilbert α} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} :

LO.Modal.Theory.Consistent Λ (T₁ ∪ T₂) → LO.Modal.Theory.Consistent Λ T₁ ∧ LO.Modal.Theory.Consistent Λ T₂

source

theorem LO.Modal.Theory.union_not_consistent {α : Type u_1} {Λ : LO.Modal.Hilbert α} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} :

¬LO.Modal.Theory.Consistent Λ T₁ ∨ ¬LO.Modal.Theory.Consistent Λ T₂ → ¬LO.Modal.Theory.Consistent Λ (T₁ ∪ T₂)

source

theorem LO.Modal.Theory.iff_insert_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} {p : LO.Modal.Formula α} :

LO.Modal.Theory.Consistent Λ (insert p T) ↔ ∀ {Γ : List (LO.Modal.Formula α)}, (∀ q ∈ Γ, q ∈ T) → Λ ⊬ p ⋏ ⋀Γ ➝ ⊥

source

theorem LO.Modal.Theory.iff_insert_inconsistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} {p : LO.Modal.Formula α} :

¬LO.Modal.Theory.Consistent Λ (insert p T) ↔ ∃ (Γ : List (LO.Modal.Formula α)), (∀ p ∈ Γ, p ∈ T) ∧ Λ ⊢! p ⋏ ⋀Γ ➝ ⊥

source

theorem LO.Modal.Theory.provable_iff_insert_neg_not_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} {p : LO.Modal.Formula α} :

T *⊢[Λ]! p ↔ ¬LO.Modal.Theory.Consistent Λ (insert (∼p) T)

source

theorem LO.Modal.Theory.unprovable_iff_insert_neg_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} {p : LO.Modal.Formula α} :

T *⊬[Λ] p ↔ LO.Modal.Theory.Consistent Λ (insert (∼p) T)

source

theorem LO.Modal.Theory.unprovable_iff_singleton_neg_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} :

Λ ⊬ p ↔ LO.Modal.Theory.Consistent Λ {∼p}

source

theorem LO.Modal.Theory.neg_provable_iff_insert_not_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} {p : LO.Modal.Formula α} :

T *⊢[Λ]! ∼p ↔ ¬LO.Modal.Theory.Consistent Λ (insert p T)

source

theorem LO.Modal.Theory.neg_unprovable_iff_insert_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} {p : LO.Modal.Formula α} :

T *⊬[Λ] ∼p ↔ LO.Modal.Theory.Consistent Λ (insert p T)

source

theorem LO.Modal.Theory.unprovable_iff_singleton_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} :

Λ ⊬ ∼p ↔ LO.Modal.Theory.Consistent Λ {p}

source

theorem LO.Modal.Theory.unprovable_falsum {α : Type u_1} {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) :

T *⊬[Λ] ⊥

source

theorem LO.Modal.Theory.unprovable_either {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) {p : LO.Modal.Formula α} :

¬(T *⊢[Λ]! p ∧ T *⊢[Λ]! ∼p)

source

theorem LO.Modal.Theory.not_mem_falsum_of_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) :

⊥ ∉ T

source

theorem LO.Modal.Theory.not_singleton_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) {p : LO.Modal.Formula α} [Λ.HasNecessitation] (h : ∼□p ∈ T) :

LO.Modal.Theory.Consistent Λ {∼p}

source

theorem LO.Modal.Theory.either_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) (p : LO.Modal.Formula α) :

LO.Modal.Theory.Consistent Λ (insert p T) ∨ LO.Modal.Theory.Consistent Λ (insert (∼p) T)

source

theorem LO.Modal.Theory.exists_maximal_consistent_theory {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) :

∃ (Z : LO.Modal.Theory α), LO.Modal.Theory.Consistent Λ Z ∧ T ⊆ Z ∧ ∀ (U : LO.Modal.Theory α), LO.Modal.Theory.Consistent Λ U → Z ⊆ U → U = Z

source

theorem LO.Modal.Theory.lindenbaum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) :

∃ (Z : LO.Modal.Theory α), LO.Modal.Theory.Consistent Λ Z ∧ T ⊆ Z ∧ ∀ (U : LO.Modal.Theory α), LO.Modal.Theory.Consistent Λ U → Z ⊆ U → U = Z

Alias of LO.Modal.Theory.exists_maximal_consistent_theory.

source

theorem LO.Modal.Theory.intro_union_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} (h : ∀ {Γ₁ Γ₂ : List (LO.Modal.Formula α)}, ((∀ p ∈ Γ₁, p ∈ T₁) ∧ ∀ p ∈ Γ₂, p ∈ T₂) → Λ ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ➝ ⊥) :

LO.Modal.Theory.Consistent Λ (T₁ ∪ T₂)

source

theorem LO.Modal.Theory.intro_triunion_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} {T₃ : LO.Modal.Theory α} (h : ∀ {Γ₁ Γ₂ Γ₃ : List (LO.Modal.Formula α)}, ((∀ p ∈ Γ₁, p ∈ T₁) ∧ (∀ p ∈ Γ₂, p ∈ T₂) ∧ ∀ p ∈ Γ₃, p ∈ T₃) → Λ ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ⋏ ⋀Γ₃ ➝ ⊥) :

LO.Modal.Theory.Consistent Λ (T₁ ∪ T₂ ∪ T₃)

source

theorem LO.Modal.Theory.not_mem_of_mem_neg {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) {p : LO.Modal.Formula α} (h : ∼p ∈ T) :

p ∉ T

source

theorem LO.Modal.Theory.not_mem_neg_of_mem {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (T_consis : LO.Modal.Theory.Consistent Λ T) {p : LO.Modal.Formula α} (h : p ∈ T) :

∼p ∉ T

source

structure LO.Modal.MaximalConsistentTheory {α : Type u_1} (Λ : LO.Modal.Hilbert α) :

Type u_1

theory : LO.Modal.Theory α
consistent : LO.Modal.Theory.Consistent Λ self.theory
maximal : ∀ {U : LO.Modal.Theory α}, self.theory ⊂ U → ¬LO.Modal.Theory.Consistent Λ U

Instances For

source

theorem LO.Modal.MaximalConsistentTheory.consistent {α : Type u_1} {Λ : LO.Modal.Hilbert α} (self : LO.Modal.MaximalConsistentTheory Λ) :

LO.Modal.Theory.Consistent Λ self.theory

source

theorem LO.Modal.MaximalConsistentTheory.maximal {α : Type u_1} {Λ : LO.Modal.Hilbert α} (self : LO.Modal.MaximalConsistentTheory Λ) {U : LO.Modal.Theory α} :

self.theory ⊂ U → ¬LO.Modal.Theory.Consistent Λ U

source

def LO.Modal.MCT {α : Type u_1} (Λ : LO.Modal.Hilbert α) :

Type u_1

Alias of LO.Modal.MaximalConsistentTheory.

Equations

@LO.Modal.MCT = @LO.Modal.MaximalConsistentTheory

Instances For

source

theorem LO.Modal.MaximalConsistentTheory.exists_maximal_Lconsistented_theory {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (consisT : LO.Modal.Theory.Consistent Λ T) :

∃ (Ω : LO.Modal.MCT Λ), T ⊆ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.lindenbaum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {T : LO.Modal.Theory α} (consisT : LO.Modal.Theory.Consistent Λ T) :

∃ (Ω : LO.Modal.MCT Λ), T ⊆ Ω.theory

Alias of LO.Modal.MaximalConsistentTheory.exists_maximal_Lconsistented_theory.

source

instance LO.Modal.MaximalConsistentTheory.instNonemptyMCTOfConsistentFormulaHilbert {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} [LO.System.Consistent Λ] :

Nonempty (LO.Modal.MCT Λ)

Equations

⋯ = ⋯

source

theorem LO.Modal.MaximalConsistentTheory.either_mem {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} (Ω : LO.Modal.MCT Λ) (p : LO.Modal.Formula α) :

p ∈ Ω.theory ∨ ∼p ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.maximal' {α : Type u_1} {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} (hp : p ∉ Ω.theory) :

¬LO.Modal.Theory.Consistent Λ (insert p Ω.theory)

source

theorem LO.Modal.MaximalConsistentTheory.membership_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} :

p ∈ Ω.theory ↔ Ω.theory *⊢[Λ]! p

source

theorem LO.Modal.MaximalConsistentTheory.subset_axiomset {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} :

Ax(Λ) ⊆ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.not_mem_falsum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} :

⊥ ∉ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.mem_verum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} :

⊤ ∈ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.unprovable_falsum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} :

Ω.theory *⊬[Λ] ⊥

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.iff_mem_neg {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} :

∼p ∈ Ω.theory ↔ p ∉ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_negneg {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} :

∼∼p ∈ Ω.theory ↔ p ∈ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.iff_mem_imp {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :

p ➝ q ∈ Ω.theory ↔ p ∈ Ω.theory → q ∈ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.iff_mem_and {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :

p ⋏ q ∈ Ω.theory ↔ p ∈ Ω.theory ∧ q ∈ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.iff_mem_or {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :

p ⋎ q ∈ Ω.theory ↔ p ∈ Ω.theory ∨ q ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_congr {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :

Ω.theory *⊢[Λ]! p ⭤ q → (p ∈ Ω.theory ↔ q ∈ Ω.theory)

source

theorem LO.Modal.MaximalConsistentTheory.mem_dn_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} :

p ∈ Ω.theory ↔ ∼∼p ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.equality_def {α : Type u_1} {Λ : LO.Modal.Hilbert α} {Ω₁ : LO.Modal.MCT Λ} {Ω₂ : LO.Modal.MCT Λ} :

Ω₁ = Ω₂ ↔ Ω₁.theory = Ω₂.theory

source

theorem LO.Modal.MaximalConsistentTheory.intro_equality {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω₁ : LO.Modal.MCT Λ} {Ω₂ : LO.Modal.MCT Λ} {h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory} :

Ω₁ = Ω₂

source

theorem LO.Modal.MaximalConsistentTheory.neg_imp {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω₁ : LO.Modal.MCT Λ} {Ω₂ : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (h : q ∈ Ω₂.theory → p ∈ Ω₁.theory) :

∼p ∈ Ω₁.theory → ∼q ∈ Ω₂.theory

source

theorem LO.Modal.MaximalConsistentTheory.neg_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω₁ : LO.Modal.MCT Λ} {Ω₂ : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (h : p ∈ Ω₁.theory ↔ q ∈ Ω₂.theory) :

∼p ∈ Ω₁.theory ↔ ∼q ∈ Ω₂.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_multibox {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] {n : ℕ} :

□^[n]p ∈ Ω.theory ↔ ∀ {Ω' : LO.Modal.MCT Λ}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_box {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] :

□p ∈ Ω.theory ↔ ∀ {Ω' : LO.Modal.MCT Λ}, □''⁻¹Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

source

theorem LO.Modal.MaximalConsistentTheory.multibox_dn_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] {n : ℕ} :

□^[n](∼∼p) ∈ Ω.theory ↔ □^[n]p ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.box_dn_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] :

□(∼∼p) ∈ Ω.theory ↔ □p ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.mem_multibox_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] {n : ℕ} :

□^[n]p ∈ Ω.theory ↔ ∼◇^[n](∼p) ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.mem_box_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] :

□p ∈ Ω.theory ↔ ∼◇(∼p) ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.mem_multidia_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] {n : ℕ} :

◇^[n]p ∈ Ω.theory ↔ ∼□^[n](∼p) ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.mem_dia_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] :

◇p ∈ Ω.theory ↔ ∼□(∼p) ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_multidia {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] {n : ℕ} :

◇^[n]p ∈ Ω.theory ↔ ∃ (Ω' : LO.Modal.MCT Λ), □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∈ Ω'.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_dia {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {p : LO.Modal.Formula α} [Λ.IsNormal] :

◇p ∈ Ω.theory ↔ ∃ (Ω' : LO.Modal.MCT Λ), □''⁻¹Ω.theory ⊆ Ω'.theory ∧ p ∈ Ω'.theory

source

theorem LO.Modal.MaximalConsistentTheory.multibox_multidia {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω₁ : LO.Modal.MCT Λ} {Ω₂ : LO.Modal.MCT Λ} [Λ.IsNormal] {n : ℕ} :

(∀ {p : LO.Modal.Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory) ↔ ∀ {p : LO.Modal.Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_conj {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} {Γ : List (LO.Modal.Formula α)} :

⋀Γ ∈ Ω.theory ↔ ∀ p ∈ Γ, p ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_multibox_conj {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} [Λ.IsNormal] {Γ : List (LO.Modal.Formula α)} {n : ℕ} :

□^[n]⋀Γ ∈ Ω.theory ↔ ∀ p ∈ Γ, □^[n]p ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_mem_box_conj {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {Ω : LO.Modal.MCT Λ} [Λ.IsNormal] {Γ : List (LO.Modal.Formula α)} :

□⋀Γ ∈ Ω.theory ↔ ∀ p ∈ Γ, □p ∈ Ω.theory