@[reducible, inline]

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

Equations

• (Λ)-Consistent T = T *⊬[Λ]! ⊥

def LO.Modal.Standard.«term(_)-Consistent_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Equations

• LO.Modal.Standard.Theory.Inconsistent Λ T = ¬(Λ)-Consistent T

theorem LO.Modal.Standard.Theory.def_consistent {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} : (Λ)-Consistent T ↔ ∀ (Γ : List (LO.Modal.Standard.Formula α)), (∀ q ∈ Γ, q ∈ T) → Γ ⊬[Λ]! ⊥

theorem LO.Modal.Standard.Theory.def_inconsistent {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} : ¬(Λ)-Consistent T ↔ ∃ (Γ : List (LO.Modal.Standard.Formula α)), (∀ q ∈ Γ, q ∈ T) ∧ Γ ⊢[Λ]! ⊥

@[simp]

theorem LO.Modal.Standard.Theory.self_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ_consis : LO.System.Consistent Λ] : (Λ)-Consistent Ax(Λ)

theorem LO.Modal.Standard.Theory.emptyset_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [Λ_consis : LO.System.Consistent Λ] : (Λ)-Consistent ∅

theorem LO.Modal.Standard.Theory.union_consistent {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {T₁ : LO.Modal.Standard.Theory α} {T₂ : LO.Modal.Standard.Theory α} : (Λ)-Consistent (T₁ ∪ T₂) → (Λ)-Consistent T₁ ∧ (Λ)-Consistent T₂

theorem LO.Modal.Standard.Theory.union_not_consistent {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {T₁ : LO.Modal.Standard.Theory α} {T₂ : LO.Modal.Standard.Theory α} : ¬(Λ)-Consistent T₁ ∨ ¬(Λ)-Consistent T₂ → ¬(Λ)-Consistent (T₁ ∪ T₂)

theorem LO.Modal.Standard.Theory.iff_insert_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} {p : LO.Modal.Standard.Formula α} : (Λ)-Consistent insert p T ↔ ∀ {Γ : List (LO.Modal.Standard.Formula α)}, (∀ q ∈ Γ, q ∈ T) → Λ ⊬! p ⋏ ⋀Γ ⟶ ⊥

theorem LO.Modal.Standard.Theory.iff_insert_inconsistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} {p : LO.Modal.Standard.Formula α} : ¬(Λ)-Consistent insert p T ↔ ∃ (Γ : List (LO.Modal.Standard.Formula α)), (∀ p ∈ Γ, p ∈ T) ∧ Λ ⊢! p ⋏ ⋀Γ ⟶ ⊥

theorem LO.Modal.Standard.Theory.provable_iff_insert_neg_not_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} {p : LO.Modal.Standard.Formula α} : T *⊢[Λ]! p ↔ ¬(Λ)-Consistent insert (~p) T

theorem LO.Modal.Standard.Theory.unprovable_iff_insert_neg_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} {p : LO.Modal.Standard.Formula α} : T *⊬[Λ]! p ↔ (Λ)-Consistent insert (~p) T

theorem LO.Modal.Standard.Theory.unprovable_iff_singleton_neg_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {p : LO.Modal.Standard.Formula α} : Λ ⊬! p ↔ (Λ)-Consistent {~p}

theorem LO.Modal.Standard.Theory.neg_provable_iff_insert_not_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} {p : LO.Modal.Standard.Formula α} : T *⊢[Λ]! ~p ↔ ¬(Λ)-Consistent insert p T

theorem LO.Modal.Standard.Theory.neg_unprovable_iff_insert_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} {p : LO.Modal.Standard.Formula α} : T *⊬[Λ]! ~p ↔ (Λ)-Consistent insert p T

theorem LO.Modal.Standard.Theory.unprovable_falsum {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (T_consis : (Λ)-Consistent T) : T *⊬[Λ]! ⊥

theorem LO.Modal.Standard.Theory.unprovable_either {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (T_consis : (Λ)-Consistent T) {p : LO.Modal.Standard.Formula α} : ¬(T *⊢[Λ]! p ∧ T *⊢[Λ]! ~p)

theorem LO.Modal.Standard.Theory.not_mem_falsum_of_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (T_consis : (Λ)-Consistent T) : ⊥ ∉ T

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

theorem LO.Modal.Standard.Theory.either_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (T_consis : (Λ)-Consistent T) (p : LO.Modal.Standard.Formula α) : (Λ)-Consistent insert p T ∨ (Λ)-Consistent insert (~p) T

theorem LO.Modal.Standard.Theory.exists_maximal_consistent_theory {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (T_consis : (Λ)-Consistent T) : ∃ (Z : LO.Modal.Standard.Theory α), (Λ)-Consistent Z ∧ T ⊆ Z ∧ ∀ (U : LO.Modal.Standard.Theory α), (Λ)-Consistent U → Z ⊆ U → U = Z

theorem LO.Modal.Standard.Theory.lindenbaum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (T_consis : (Λ)-Consistent T) : ∃ (Z : LO.Modal.Standard.Theory α), (Λ)-Consistent Z ∧ T ⊆ Z ∧ ∀ (U : LO.Modal.Standard.Theory α), (Λ)-Consistent U → Z ⊆ U → U = Z

Alias of LO.Modal.Standard.Theory.exists_maximal_consistent_theory.

theorem LO.Modal.Standard.Theory.intro_union_consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T₁ : LO.Modal.Standard.Theory α} {T₂ : LO.Modal.Standard.Theory α} (h : ∀ {Γ₁ Γ₂ : List (LO.Modal.Standard.Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → Λ ⊬! ⋀Γ₁ ⋏ ⋀Γ₂ ⟶ ⊥) : (Λ)-Consistent (T₁ ∪ T₂)

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

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

theorem LO.Modal.Standard.MaximalConsistentTheory.consistent {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} (self : (Λ)-MCT) : (Λ)-Consistent self.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.maximal {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} (self : (Λ)-MCT) {U : LO.Modal.Standard.Theory α} : self.theory ⊂ U → ¬(Λ)-Consistent U

def LO.Modal.Standard.«term(_)-MCT» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Standard.MaximalConsistentTheory.exists_maximal_Lconsistented_theory {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (consisT : (Λ)-Consistent T) : ∃ (Ω : (Λ)-MCT), T ⊆ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.lindenbaum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {T : LO.Modal.Standard.Theory α} (consisT : (Λ)-Consistent T) : ∃ (Ω : (Λ)-MCT), T ⊆ Ω.theory

Alias of LO.Modal.Standard.MaximalConsistentTheory.exists_maximal_Lconsistented_theory.

noncomputable instance LO.Modal.Standard.MaximalConsistentTheory.instInhabitedOfConsistentFormulaDeductionParameter {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [LO.System.Consistent Λ] : Inhabited (Λ)-MCT

Equations

• LO.Modal.Standard.MaximalConsistentTheory.instInhabitedOfConsistentFormulaDeductionParameter = { default := ⋯.choose }

theorem LO.Modal.Standard.MaximalConsistentTheory.either_mem {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} (Ω : (Λ)-MCT) (p : LO.Modal.Standard.Formula α) : p ∈ Ω.theory ∨ ~p ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.maximal' {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} (hp : p ∉ Ω.theory) : ¬(Λ)-Consistent insert p Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.membership_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} : p ∈ Ω.theory ↔ Ω.theory *⊢[Λ]! p

theorem LO.Modal.Standard.MaximalConsistentTheory.subset_axiomset {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} : Ax(Λ) ⊆ Ω.theory

@[simp]

theorem LO.Modal.Standard.MaximalConsistentTheory.not_mem_falsum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} : ⊥ ∉ Ω.theory

@[simp]

theorem LO.Modal.Standard.MaximalConsistentTheory.mem_verum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} : ⊤ ∈ Ω.theory

@[simp]

theorem LO.Modal.Standard.MaximalConsistentTheory.unprovable_falsum {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} : Ω.theory *⊬[Λ]! ⊥

@[simp]

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_neg {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} : ~p ∈ Ω.theory ↔ p ∉ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_negneg {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} : ~~p ∈ Ω.theory ↔ p ∈ Ω.theory

@[simp]

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_imp {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : p ⟶ q ∈ Ω.theory ↔ p ∈ Ω.theory → q ∈ Ω.theory

@[simp]

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_and {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : p ⋏ q ∈ Ω.theory ↔ p ∈ Ω.theory ∧ q ∈ Ω.theory

@[simp]

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_or {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : p ⋎ q ∈ Ω.theory ↔ p ∈ Ω.theory ∨ q ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_congr {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : Ω.theory *⊢[Λ]! p ⟷ q → (p ∈ Ω.theory ↔ q ∈ Ω.theory)

theorem LO.Modal.Standard.MaximalConsistentTheory.mem_dn_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} : p ∈ Ω.theory ↔ ~~p ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.equality_def {α : Type u_1} {Λ : LO.Modal.Standard.DeductionParameter α} {Ω₁ : (Λ)-MCT} {Ω₂ : (Λ)-MCT} : Ω₁ = Ω₂ ↔ Ω₁.theory = Ω₂.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.intro_equality {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω₁ : (Λ)-MCT} {Ω₂ : (Λ)-MCT} {h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory} : Ω₁ = Ω₂

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

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

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_multibox {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] {n : ℕ} : □^[n]p ∈ Ω.theory ↔ ∀ {Ω' : (Λ)-MCT}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_box {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] : □p ∈ Ω.theory ↔ ∀ {Ω' : (Λ)-MCT}, □''⁻¹Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.multibox_dn_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] {n : ℕ} : □^[n](~~p) ∈ Ω.theory ↔ □^[n]p ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.box_dn_iff {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] : □(~~p) ∈ Ω.theory ↔ □p ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.mem_multibox_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] {n : ℕ} : □^[n]p ∈ Ω.theory ↔ ~◇^[n](~p) ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.mem_box_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] : □p ∈ Ω.theory ↔ ~◇(~p) ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.mem_multidia_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] {n : ℕ} : ◇^[n]p ∈ Ω.theory ↔ ~□^[n](~p) ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.mem_dia_dual {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] : ◇p ∈ Ω.theory ↔ ~□(~p) ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_multidia {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] {n : ℕ} : ◇^[n]p ∈ Ω.theory ↔ ∃ (Ω' : (Λ)-MCT), □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∈ Ω'.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_dia {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {p : LO.Modal.Standard.Formula α} [Λ.IsNormal] : ◇p ∈ Ω.theory ↔ ∃ (Ω' : (Λ)-MCT), □''⁻¹Ω.theory ⊆ Ω'.theory ∧ p ∈ Ω'.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.multibox_multidia {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω₁ : (Λ)-MCT} {Ω₂ : (Λ)-MCT} [Λ.IsNormal] {n : ℕ} : (∀ {p : LO.Modal.Standard.Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory) ↔ ∀ {p : LO.Modal.Standard.Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω₁.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_conj {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} {Γ : List (LO.Modal.Standard.Formula α)} : ⋀Γ ∈ Ω.theory ↔ ∀ p ∈ Γ, p ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_multibox_conj {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} [Λ.IsNormal] {Γ : List (LO.Modal.Standard.Formula α)} {n : ℕ} : □^[n]⋀Γ ∈ Ω.theory ↔ ∀ p ∈ Γ, □^[n]p ∈ Ω.theory

theorem LO.Modal.Standard.MaximalConsistentTheory.iff_mem_box_conj {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} {Ω : (Λ)-MCT} [Λ.IsNormal] {Γ : List (LO.Modal.Standard.Formula α)} : □⋀Γ ∈ Ω.theory ↔ ∀ p ∈ Γ, □p ∈ Ω.theory