def LO.Modal.Formula.complement {α : Type u_1} : LO.Modal.Formula α → LO.Modal.Formula α

Equations

• -φ.imp LO.Modal.Formula.falsum = φ
• -x = ∼x

def LO.Modal.Formula.«term-_» : Lean.ParserDescr

Equations

• LO.Modal.Formula.«term-_» = Lean.ParserDescr.node `LO.Modal.Formula.«term-_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "-") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem LO.Modal.Formula.complement.neg_def {α : Type u_1} {φ : LO.Modal.Formula α} : -(∼φ) = φ

@[simp]

theorem LO.Modal.Formula.complement.bot_def {α : Type u_1} : -⊥ = ∼⊥

@[simp]

theorem LO.Modal.Formula.complement.box_def {α : Type u_1} {φ : LO.Modal.Formula α} : -(□φ) = ∼□φ

theorem LO.Modal.Formula.complement.imp_def₁ {α : Type u_1} {φ ψ : LO.Modal.Formula α} (hq : ψ ≠ ⊥) : -(φ ➝ ψ) = ∼(φ ➝ ψ)

theorem LO.Modal.Formula.complement.imp_def₂ {α : Type u_1} {φ ψ : LO.Modal.Formula α} (hq : ψ = ⊥) : -(φ ➝ ψ) = φ

theorem LO.Modal.Formula.complement.resort_box {α : Type u_1} {φ ψ : LO.Modal.Formula α} (h : -φ = □ψ) : φ = ∼□ψ

theorem LO.Modal.Formula.complement.or {α : Type u_1} [DecidableEq α] (φ : LO.Modal.Formula α) : -φ = ∼φ ∨ ∃ (ψ : LO.Modal.Formula α), ∼ψ = φ

theorem LO.Modal.complement_derive_bot {α : Type u_1} {S : Type u_2} [LO.System (LO.Modal.Formula α) S] {𝓢 : S} [LO.System.ModusPonens 𝓢] {φ : LO.Modal.Formula α} [DecidableEq α] (hp : 𝓢 ⊢! φ) (hcp : 𝓢 ⊢! -φ) : 𝓢 ⊢! ⊥

theorem LO.Modal.neg_complement_derive_bot {α : Type u_1} {S : Type u_2} [LO.System (LO.Modal.Formula α) S] {𝓢 : S} [LO.System.ModusPonens 𝓢] {φ : LO.Modal.Formula α} [DecidableEq α] (hp : 𝓢 ⊢! ∼φ) (hcp : 𝓢 ⊢! ∼-φ) : 𝓢 ⊢! ⊥

def LO.Modal.Formulae.complementary {α : Type u_1} [DecidableEq α] (P : LO.Modal.Formulae α) : LO.Modal.Formulae α

Equations

• P⁻ = P ∪ Finset.image LO.Modal.Formula.complement P

def LO.Modal.Formulae.«term_⁻» : Lean.TrailingParserDescr

Equations

• LO.Modal.Formulae.«term_⁻» = Lean.ParserDescr.trailingNode `LO.Modal.Formulae.«term_⁻» 80 80 (Lean.ParserDescr.symbol "⁻")

theorem LO.Modal.Formulae.complementary_mem {α : Type u_1} [DecidableEq α] {P : LO.Modal.Formulae α} {φ : LO.Modal.Formula α} (h : φ ∈ P) : φ ∈ P⁻

theorem LO.Modal.Formulae.complementary_comp {α : Type u_1} [DecidableEq α] {P : LO.Modal.Formulae α} {φ : LO.Modal.Formula α} (h : φ ∈ P) : -φ ∈ P⁻

theorem LO.Modal.Formulae.complementary_mem_box {α : Type u_1} [DecidableEq α] {P : LO.Modal.Formulae α} {φ : LO.Modal.Formula α} (hi : ∀ {ψ χ : LO.Modal.Formula α}, ψ ➝ χ ∈ P → ψ ∈ P := by trivial) : □φ ∈ P⁻ → □φ ∈ P

class LO.Modal.Formulae.ComplementaryClosed {α : Type u_1} [DecidableEq α] (P S : LO.Modal.Formulae α) : Prop

• subset : P ⊆ S⁻
• either : ∀ φ ∈ S, φ ∈ P ∨ -φ ∈ P

def LO.Modal.Formulae.SubformulaeComplementaryClosed {α : Type u_1} [DecidableEq α] (P : LO.Modal.Formulae α) (φ : LO.Modal.Formula α) : Prop

Equations

• P.SubformulaeComplementaryClosed φ = P.ComplementaryClosed φ.subformulae

def LO.Modal.Formulae.Consistent {α : Type u_1} (H : LO.Modal.Hilbert α) (P : LO.Modal.Formulae α) : Prop

Equations

• LO.Modal.Formulae.Consistent H P = ↑P *⊬[H] ⊥

@[simp]

theorem LO.Modal.Formulae.iff_theory_consistent_formulae_consistent {α : Type u_1} {H : LO.Modal.Hilbert α} {P : LO.Modal.Formulae α} : LO.Modal.Theory.Consistent H ↑P ↔ LO.Modal.Formulae.Consistent H P

@[simp]

theorem LO.Modal.Formulae.empty_conisistent {α : Type u_1} {H : LO.Modal.Hilbert α} [LO.System.Consistent H] : LO.Modal.Formulae.Consistent H ∅

theorem LO.Modal.Formulae.provable_iff_insert_neg_not_consistent {α : Type u_1} {H : LO.Modal.Hilbert α} [DecidableEq α] {P : LO.Modal.Formulae α} {φ : LO.Modal.Formula α} : ↑P *⊢[H]! φ ↔ ¬LO.Modal.Formulae.Consistent H (insert (∼φ) P)

theorem LO.Modal.Formulae.neg_provable_iff_insert_not_consistent {α : Type u_1} {H : LO.Modal.Hilbert α} [DecidableEq α] {P : LO.Modal.Formulae α} {φ : LO.Modal.Formula α} : ↑P *⊢[H]! ∼φ ↔ ¬LO.Modal.Formulae.Consistent H (insert φ P)

theorem LO.Modal.Formulae.unprovable_iff_singleton_neg_consistent {α : Type u_1} {H : LO.Modal.Hilbert α} [DecidableEq α] {φ : LO.Modal.Formula α} : H ⊬ φ ↔ LO.Modal.Formulae.Consistent H {∼φ}

theorem LO.Modal.Formulae.unprovable_iff_singleton_compl_consistent {α : Type u_1} {H : LO.Modal.Hilbert α} [DecidableEq α] {φ : LO.Modal.Formula α} : H ⊬ φ ↔ LO.Modal.Formulae.Consistent H {-φ}

theorem LO.Modal.Formulae.provable_iff_singleton_compl_inconsistent {α : Type u_1} {H : LO.Modal.Hilbert α} [DecidableEq α] {φ : LO.Modal.Formula α} : H ⊢! φ ↔ ¬LO.Modal.Formulae.Consistent H {-φ}

theorem LO.Modal.Formulae.intro_union_consistent {α : Type u_1} {H : LO.Modal.Hilbert α} [DecidableEq α] {P₁ P₂ : LO.Modal.Formulae α} (h : ∀ {Γ₁ Γ₂ : List (LO.Modal.Formula α)}, ((∀ φ ∈ Γ₁, φ ∈ P₁) ∧ ∀ φ ∈ Γ₂, φ ∈ P₂) → H ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ➝ ⊥) : LO.Modal.Formulae.Consistent H (P₁ ∪ P₂)

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

noncomputable def LO.Modal.Formulae.exists_consistent_complementary_closed.next {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] (φ : LO.Modal.Formula α) (P : LO.Modal.Formulae α) : LO.Modal.Formulae α

Equations

• LO.Modal.Formulae.exists_consistent_complementary_closed.next H φ P = if LO.Modal.Formulae.Consistent H (insert φ P) then insert φ P else insert (-φ) P

noncomputable def LO.Modal.Formulae.exists_consistent_complementary_closed.enum {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] (P : LO.Modal.Formulae α) : List (LO.Modal.Formula α) → LO.Modal.Formulae α

Equations

• One or more equations did not get rendered due to their size.
• LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P [] = P

theorem LO.Modal.Formulae.exists_consistent_complementary_closed.next_consistent {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] {P : LO.Modal.Formulae α} (P_consis : LO.Modal.Formulae.Consistent H P) (φ : LO.Modal.Formula α) : LO.Modal.Formulae.Consistent H (LO.Modal.Formulae.exists_consistent_complementary_closed.next H φ P)

theorem LO.Modal.Formulae.exists_consistent_complementary_closed.enum_consistent {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] {P : LO.Modal.Formulae α} (P_consis : LO.Modal.Formulae.Consistent H P) {l : List (LO.Modal.Formula α)} : LO.Modal.Formulae.Consistent H (LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P l)

@[simp]

theorem LO.Modal.Formulae.exists_consistent_complementary_closed.enum_nil {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] {P : LO.Modal.Formulae α} : LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P [] = P

theorem LO.Modal.Formulae.exists_consistent_complementary_closed.enum_subset_step {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] {P : LO.Modal.Formulae α} {ψ : LO.Modal.Formula α} {l : List (LO.Modal.Formula α)} : LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P l ⊆ LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P (ψ :: l)

theorem LO.Modal.Formulae.exists_consistent_complementary_closed.enum_subset {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] {P : LO.Modal.Formulae α} {l : List (LO.Modal.Formula α)} : P ⊆ LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P l

theorem LO.Modal.Formulae.exists_consistent_complementary_closed.either {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] {P : LO.Modal.Formulae α} {φ : LO.Modal.Formula α} {l : List (LO.Modal.Formula α)} (hp : φ ∈ l) : φ ∈ LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P l ∨ -φ ∈ LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P l

theorem LO.Modal.Formulae.exists_consistent_complementary_closed.subset {α : Type u_1} (H : LO.Modal.Hilbert α) [DecidableEq α] {P : LO.Modal.Formulae α} {l : List (LO.Modal.Formula α)} {φ : LO.Modal.Formula α} (h : φ ∈ LO.Modal.Formulae.exists_consistent_complementary_closed.enum H P l) : φ ∈ P ∨ φ ∈ l ∨ ∃ ψ ∈ l, -ψ = φ

theorem LO.Modal.Formulae.exists_consistent_complementary_closed {α : Type u_1} {H : LO.Modal.Hilbert α} [DecidableEq α] {P : LO.Modal.Formulae α} (S : LO.Modal.Formulae α) (h_sub : P ⊆ S⁻) (P_consis : LO.Modal.Formulae.Consistent H P) : ∃ (P' : LO.Modal.Formulae α), P ⊆ P' ∧ LO.Modal.Formulae.Consistent H P' ∧ P'.ComplementaryClosed S

structure LO.Modal.ComplementaryClosedConsistentFormulae {α : Type u_1} [DecidableEq α] (H : LO.Modal.Hilbert α) (S : LO.Modal.Formulae α) : Type u_1

• formulae : LO.Modal.Formulae α
• consistent : LO.Modal.Formulae.Consistent H self.formulae
• closed : self.formulae.ComplementaryClosed S

def LO.Modal.CCF {α : Type u_1} [DecidableEq α] (H : LO.Modal.Hilbert α) (S : LO.Modal.Formulae α) : Type u_1

Alias of LO.Modal.ComplementaryClosedConsistentFormulae.

Equations

• @LO.Modal.CCF = @LO.Modal.ComplementaryClosedConsistentFormulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.lindenbaum {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} (S : LO.Modal.Formulae α) {X : LO.Modal.Formulae α} (X_sub : X ⊆ S⁻) (X_consis : LO.Modal.Formulae.Consistent H X) : ∃ (X' : LO.Modal.CCF H S), X ⊆ X'.formulae

noncomputable instance LO.Modal.ComplementaryClosedConsistentFormulae.instInhabitedCCFOfConsistentFormulaHilbert {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} [LO.System.Consistent H] : Inhabited (LO.Modal.CCF H S)

Equations

• LO.Modal.ComplementaryClosedConsistentFormulae.instInhabitedCCFOfConsistentFormulaHilbert = { default := ⋯.choose }

@[simp]

theorem LO.Modal.ComplementaryClosedConsistentFormulae.unprovable_falsum {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} : ↑X.formulae *⊬[H] ⊥

theorem LO.Modal.ComplementaryClosedConsistentFormulae.mem_compl_of_not_mem {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} {ψ : LO.Modal.Formula α} (hs : ψ ∈ S) : ψ ∉ X.formulae → -ψ ∈ X.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.mem_of_not_mem_compl {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} {ψ : LO.Modal.Formula α} (hs : ψ ∈ S) : -ψ ∉ X.formulae → ψ ∈ X.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.membership_iff {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} {ψ : LO.Modal.Formula α} (hq_sub : ψ ∈ S) : ψ ∈ X.formulae ↔ ↑X.formulae *⊢[H]! ψ

theorem LO.Modal.ComplementaryClosedConsistentFormulae.mem_verum {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} (h : ⊤ ∈ S) : ⊤ ∈ X.formulae

@[simp]

theorem LO.Modal.ComplementaryClosedConsistentFormulae.mem_falsum {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} : ⊥ ∉ X.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.iff_mem_compl {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} {ψ : LO.Modal.Formula α} (hq_sub : ψ ∈ S) : ψ ∈ X.formulae ↔ -ψ ∉ X.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.iff_mem_imp {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} {ψ χ : LO.Modal.Formula α} (hsub_qr : ψ ➝ χ ∈ S) (hsub_q : ψ ∈ S := by trivial) (hsub_r : χ ∈ S := by trivial) : ψ ➝ χ ∈ X.formulae ↔ ψ ∈ X.formulae → -χ ∉ X.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.iff_not_mem_imp {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF H S} {ψ χ : LO.Modal.Formula α} (hsub_qr : ψ ➝ χ ∈ S) (hsub_q : ψ ∈ S := by trivial) (hsub_r : χ ∈ S := by trivial) : ψ ➝ χ ∉ X.formulae ↔ ψ ∈ X.formulae ∧ -χ ∈ X.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.equality_def {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X₁ X₂ : LO.Modal.CCF H S} : X₁ = X₂ ↔ X₁.formulae = X₂.formulae

instance LO.Modal.ComplementaryClosedConsistentFormulae.instFiniteCCF {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} : Finite (LO.Modal.CCF H S)

Equations

• ⋯ = ⋯