def LO.Modal.Formula.complement {α : Type u_1} : Formula α → 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} {φ : Formula α} : -(∼φ) = φ

@[simp]

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

@[simp]

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

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

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

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

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

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

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

def LO.Modal.Formulae.complementary {α : Type u_1} [DecidableEq α] (P : Formulae α) : 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 : Formulae α} {φ : Formula α} (h : φ ∈ P) : φ ∈ P⁻

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

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

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

• subset : P ⊆ S⁻
• either (φ : Formula α) : φ ∈ S → φ ∈ P ∨ -φ ∈ P

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

Equations

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

def LO.Modal.Formulae.Consistent {α : Type u_1} (H : Hilbert α) (P : 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 : Hilbert α} {P : Formulae α} : Theory.Consistent H ↑P ↔ Consistent H P

@[simp]

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

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

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

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

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

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

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

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

noncomputable def LO.Modal.Formulae.exists_consistent_complementary_closed.next {α : Type u_1} (H : Hilbert α) [DecidableEq α] (φ : Formula α) (P : Formulae α) : 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 : Hilbert α) [DecidableEq α] (P : Formulae α) : List (Formula α) → 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 : Hilbert α) [DecidableEq α] {P : Formulae α} (P_consis : Consistent H P) (φ : Formula α) : Consistent H (next H φ P)

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

@[simp]

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

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

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

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

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

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

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

@[simp]

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

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

theorem LO.Modal.ComplementaryClosedConsistentFormulae.iff_mem_imp {α : Type u_1} [DecidableEq α] {H : Hilbert α} {S : Formulae α} {X : CCF H S} {ψ χ : 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 : Hilbert α} {S : Formulae α} {X : CCF H S} {ψ χ : 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 : Hilbert α} {S : Formulae α} {X₁ X₂ : CCF H S} : X₁ = X₂ ↔ X₁.formulae = X₂.formulae

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