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

Equations

• -x = match x with | p.imp LO.Modal.Formula.falsum => p | p => ∼p

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} {p : LO.Modal.Formula α} : -(∼p) = p

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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 α} {p : LO.Modal.Formula α} (h : p ∈ P) : p ∈ P⁻

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

theorem LO.Modal.Formulae.complementary_mem_box {α : Type u_1} [DecidableEq α] {P : LO.Modal.Formulae α} {p : LO.Modal.Formula α} (hi : autoParam (∀ {q r : LO.Modal.Formula α}, q ➝ r ∈ P → q ∈ P) _auto✝) : □p ∈ P⁻ → □p ∈ P

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

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

theorem LO.Modal.Formulae.ComplementaryClosed.subset {α : Type u_1} [DecidableEq α] {P : LO.Modal.Formulae α} {S : LO.Modal.Formulae α} [self : P.ComplementaryClosed S] : P ⊆ S⁻

theorem LO.Modal.Formulae.ComplementaryClosed.either {α : Type u_1} [DecidableEq α] {P : LO.Modal.Formulae α} {S : LO.Modal.Formulae α} [self : P.ComplementaryClosed S] (p : LO.Modal.Formula α) : p ∈ S → p ∈ P ∨ -p ∈ P

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

Equations

• P.SubformulaeComplementaryClosed p = P.ComplementaryClosed (𝒮 p)

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

Equations

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

Equations

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

noncomputable def LO.Modal.Formulae.exists_consistent_complementary_closed.enum {α : Type u_1} [DecidableEq α] (Λ : LO.Modal.Hilbert α) (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 Λ P [] = P

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

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

@[simp]

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

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

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

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

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

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

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

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

theorem LO.Modal.ComplementaryClosedConsistentFormulae.consistent {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} (self : LO.Modal.ComplementaryClosedConsistentFormulae Λ S) : LO.Modal.Formulae.Consistent Λ self.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.closed {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} (self : LO.Modal.ComplementaryClosedConsistentFormulae Λ S) : self.formulae.ComplementaryClosed S

def LO.Modal.CCF {α : Type u_1} [DecidableEq α] (Λ : 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 α] {Λ : LO.Modal.Hilbert α} (S : LO.Modal.Formulae α) {X : LO.Modal.Formulae α} (X_sub : X ⊆ S⁻) (X_consis : LO.Modal.Formulae.Consistent Λ X) : ∃ (X' : LO.Modal.CCF Λ S), X ⊆ X'.formulae

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

Equations

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

@[simp]

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

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

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

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

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

@[simp]

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

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

theorem LO.Modal.ComplementaryClosedConsistentFormulae.iff_mem_imp {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF Λ S} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (hsub_qr : q ➝ r ∈ S) (hsub_q : autoParam (q ∈ S) _auto✝) (hsub_r : autoParam (r ∈ S) _auto✝) : q ➝ r ∈ X.formulae ↔ q ∈ X.formulae → -r ∉ X.formulae

theorem LO.Modal.ComplementaryClosedConsistentFormulae.iff_not_mem_imp {α : Type u_1} [DecidableEq α] {Λ : LO.Modal.Hilbert α} {S : LO.Modal.Formulae α} {X : LO.Modal.CCF Λ S} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (hsub_qr : q ➝ r ∈ S) (hsub_q : autoParam (q ∈ S) _auto✝) (hsub_r : autoParam (r ∈ S) _auto✝) : q ➝ r ∉ X.formulae ↔ q ∈ X.formulae ∧ -r ∈ X.formulae

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

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

Equations

• ⋯ = ⋯