Foundation.Modal.Hilbert.ConsistentTheory

source

@[reducible, inline]

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

Prop

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

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

Consistent H T ↔ ∀ (Γ : List (Formula α)), (∀ ψ ∈ Γ, ψ ∈ T) → Γ ⊬[H] ⊥

source

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

¬Consistent H T ↔ ∃ (Γ : List (Formula α)), (∀ ψ ∈ Γ, ψ ∈ T) ∧ Γ ⊢[H]! ⊥

source

@[simp]

theorem LO.Modal.Theory.self_consistent {α : Type u_1} {H : Hilbert α} [H_consis : System.Consistent H] :

Consistent H H.axioms

source

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

Consistent H (T₁ ∪ T₂) → Consistent H T₁ ∧ Consistent H T₂

source

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

¬Consistent H T₁ ∨ ¬Consistent H T₂ → ¬Consistent H (T₁ ∪ T₂)

source

theorem LO.Modal.Theory.emptyset_consistent {α : Type u_1} {H : Hilbert α} [H_consis : System.Consistent H] :

Consistent H ∅

source

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

Consistent H (insert φ T) ↔ ∀ {Γ : List (Formula α)}, (∀ ψ ∈ Γ, ψ ∈ T) → H ⊬ φ ⋏ ⋀Γ ➝ ⊥

source

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

¬Consistent H (insert φ T) ↔ ∃ (Γ : List (Formula α)), (∀ φ ∈ Γ, φ ∈ T) ∧ H ⊢! φ ⋏ ⋀Γ ➝ ⊥

source

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

T *⊢[H]! φ ↔ ¬Consistent H (insert (∼φ) T)

source

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

T *⊬[H] φ ↔ Consistent H (insert (∼φ) T)

source

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

H ⊬ φ ↔ Consistent H {∼φ}

source

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

T *⊢[H]! ∼φ ↔ ¬Consistent H (insert φ T)

source

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

T *⊬[H] ∼φ ↔ Consistent H (insert φ T)

source

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

H ⊬ ∼φ ↔ Consistent H {φ}

source

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

T *⊬[H] ⊥

source

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

¬(T *⊢[H]! φ ∧ T *⊢[H]! ∼φ)

source

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

⊥ ∉ T

source

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

Consistent H {∼φ}

source

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

Consistent H (insert φ T) ∨ Consistent H (insert (∼φ) T)

source

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

∃ (Z : Theory α), Consistent H Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent H U → Z ⊆ U → U = Z

source

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

∃ (Z : Theory α), Consistent H Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent H 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} {H : Hilbert α} {T₁ T₂ : Theory α} (h : ∀ {Γ₁ Γ₂ : List (Formula α)}, ((∀ φ ∈ Γ₁, φ ∈ T₁) ∧ ∀ φ ∈ Γ₂, φ ∈ T₂) → H ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ➝ ⊥) :

Consistent H (T₁ ∪ T₂)

source

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

Consistent H (T₁ ∪ T₂ ∪ T₃)

source

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

φ ∉ T

source

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

∼φ ∉ T

source

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

Type u_1

theory : Theory α
consistent : Theory.Consistent H self.theory
maximal {U : Theory α} : self.theory ⊂ U → ¬Theory.Consistent H U

source

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

Type u_1

Alias of LO.Modal.MaximalConsistentTheory.

Equations

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

Instances For

LO.Modal.MaximalConsistentTheory.instNonemptyMCTOfConsistentFormulaHilbert

source

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

∃ (Ω : MCT H), T ⊆ Ω.theory

source

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

∃ (Ω : MCT H), T ⊆ Ω.theory

Alias of LO.Modal.MaximalConsistentTheory.exists_maximal_Lconsistented_theory.

source

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

Nonempty (MCT H)

source

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

φ ∈ Ω.theory ∨ ∼φ ∈ Ω.theory

source

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

¬Theory.Consistent H (insert φ Ω.theory)

source

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

φ ∈ Ω.theory ↔ Ω.theory *⊢[H]! φ

source

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

H.axioms ⊆ Ω.theory

source

@[simp]

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

⊥ ∉ Ω.theory

source

@[simp]

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

⊤ ∈ Ω.theory

source

@[simp]

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

Ω.theory *⊬[H] ⊥

source

@[simp]

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

∼φ ∈ Ω.theory ↔ φ ∉ Ω.theory

source

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

∼∼φ ∈ Ω.theory ↔ φ ∈ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.iff_mem_imp {α : Type u_1} [DecidableEq α] {H : Hilbert α} {Ω : MCT H} {φ ψ : Formula α} :

φ ➝ ψ ∈ Ω.theory ↔ φ ∈ Ω.theory → ψ ∈ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.iff_mem_and {α : Type u_1} [DecidableEq α] {H : Hilbert α} {Ω : MCT H} {φ ψ : Formula α} :

φ ⋏ ψ ∈ Ω.theory ↔ φ ∈ Ω.theory ∧ ψ ∈ Ω.theory

source

@[simp]

theorem LO.Modal.MaximalConsistentTheory.iff_mem_or {α : Type u_1} [DecidableEq α] {H : Hilbert α} {Ω : MCT H} {φ ψ : Formula α} :

φ ⋎ ψ ∈ Ω.theory ↔ φ ∈ Ω.theory ∨ ψ ∈ Ω.theory

source

theorem LO.Modal.MaximalConsistentTheory.iff_congr {α : Type u_1} [DecidableEq α] {H : Hilbert α} {Ω : MCT H} {φ ψ : Formula α} :

Ω.theory *⊢[H]! φ ⭤ ψ → (φ ∈ Ω.theory ↔ ψ ∈ Ω.theory)

source

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

φ ∈ Ω.theory ↔ ∼∼φ ∈ Ω.theory

source

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

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

source

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

Ω₁ = Ω₂

source

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

∼φ ∈ Ω₁.theory → ∼ψ ∈ Ω₂.theory

source

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

∼φ ∈ Ω₁.theory ↔ ∼ψ ∈ Ω₂.theory

source

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

□^[n]φ ∈ Ω.theory ↔ ∀ {Ω' : MCT H}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → φ ∈ Ω'.theory

source

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

□φ ∈ Ω.theory ↔ ∀ {Ω' : MCT H}, □''⁻¹Ω.theory ⊆ Ω'.theory → φ ∈ Ω'.theory

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

◇^[n]φ ∈ Ω.theory ↔ ∃ (Ω' : MCT H), □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ φ ∈ Ω'.theory

source

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

◇φ ∈ Ω.theory ↔ ∃ (Ω' : MCT H), □''⁻¹Ω.theory ⊆ Ω'.theory ∧ φ ∈ Ω'.theory

source

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

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

source

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

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

source

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

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

source

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

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