@[reducible, inline]
abbrev
LO.Modal.Standard.Theory.Consistent
{α : Type u_1}
(Λ : LO.Modal.Standard.DeductionParameter α)
(T : LO.Modal.Standard.Theory α)
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
LO.Modal.Standard.Theory.Inconsistent
{α : Type u_1}
(Λ : LO.Modal.Standard.DeductionParameter α)
(T : LO.Modal.Standard.Theory α)
:
Equations
Instances For
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 α}
:
@[simp]
theorem
LO.Modal.Standard.Theory.self_consistent
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ_consis : LO.System.Consistent Λ]
:
theorem
LO.Modal.Standard.Theory.emptyset_consistent
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[Λ_consis : LO.System.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 α}
:
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 α}
:
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 α}
:
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 α}
:
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 α}
:
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 α}
:
theorem
LO.Modal.Standard.Theory.unprovable_iff_singleton_consistent
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{p : LO.Modal.Standard.Formula α}
:
Λ ⊬! ~p ↔ (Λ)-Consistent {p}
theorem
LO.Modal.Standard.Theory.unprovable_falsum
{α : Type u_1}
{Λ : LO.Modal.Standard.DeductionParameter α}
{T : LO.Modal.Standard.Theory α}
(T_consis : (Λ)-Consistent 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 α}
:
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₂)
theorem
LO.Modal.Standard.Theory.intro_triunion_consistent
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{T₁ : LO.Modal.Standard.Theory α}
{T₂ : LO.Modal.Standard.Theory α}
{T₃ : LO.Modal.Standard.Theory α}
(h : ∀ {Γ₁ Γ₂ Γ₃ : List (LO.Modal.Standard.Formula α)},
((∀ p ∈ Γ₁, p ∈ T₁) ∧ (∀ p ∈ Γ₂, p ∈ T₂) ∧ ∀ p ∈ Γ₃, p ∈ T₃) → Λ ⊬! ⋀Γ₁ ⋏ ⋀Γ₂ ⋏ ⋀Γ₃ ⟶ ⊥)
:
(Λ)-Consistent (T₁ ∪ T₂ ∪ T₃)
theorem
LO.Modal.Standard.Theory.not_mem_of_mem_neg
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{T : LO.Modal.Standard.Theory α}
(T_consis : (Λ)-Consistent T)
{p : LO.Modal.Standard.Formula α}
(h : ~p ∈ T)
:
p ∉ T
theorem
LO.Modal.Standard.Theory.not_mem_neg_of_mem
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{T : LO.Modal.Standard.Theory α}
(T_consis : (Λ)-Consistent T)
{p : LO.Modal.Standard.Formula α}
(h : p ∈ T)
:
~p ∉ 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
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.lindenbaum
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{T : LO.Modal.Standard.Theory α}
(consisT : (Λ)-Consistent T)
:
Alias of LO.Modal.Standard.MaximalConsistentTheory.exists_maximal_Lconsistented_theory
.
instance
LO.Modal.Standard.MaximalConsistentTheory.instNonemptyOfConsistentFormulaDeductionParameter
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
[LO.System.Consistent Λ]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.MaximalConsistentTheory.either_mem
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
(Ω : (Λ)-MCT)
(p : LO.Modal.Standard.Formula α)
:
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 α}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.subset_axiomset
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
:
@[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}
:
@[simp]
theorem
LO.Modal.Standard.MaximalConsistentTheory.unprovable_falsum
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
:
@[simp]
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_neg
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_negneg
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
:
@[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 α}
:
@[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 α}
:
@[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 α}
:
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 α}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.mem_dn_iff
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
:
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)
:
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)
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_multibox
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
{n : ℕ}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_box
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.multibox_dn_iff
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
{n : ℕ}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.box_dn_iff
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.mem_multibox_dual
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
{n : ℕ}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.mem_box_dual
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.mem_multidia_dual
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
{n : ℕ}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.mem_dia_dual
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_multidia
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
{n : ℕ}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_dia
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{p : LO.Modal.Standard.Formula α}
[Λ.IsNormal]
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.multibox_multidia
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω₁ : (Λ)-MCT}
{Ω₂ : (Λ)-MCT}
[Λ.IsNormal]
{n : ℕ}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_conj
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
{Γ : List (LO.Modal.Standard.Formula α)}
:
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 : ℕ}
:
theorem
LO.Modal.Standard.MaximalConsistentTheory.iff_mem_box_conj
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Standard.DeductionParameter α}
{Ω : (Λ)-MCT}
[Λ.IsNormal]
{Γ : List (LO.Modal.Standard.Formula α)}
: