ComplementClosedConsistentFinset

@[reducible, inline]

abbrev LO.Modal.FormulaFinset.Consistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] (𝓢 : S) (Φ : FormulaFinset α) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.FormulaFinset.Consistent 𝓢 Φ = ↑Φ *⊬[𝓢] ⊥

@[reducible, inline]

abbrev LO.Modal.FormulaFinset.Inconsistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] (𝓢 : S) (Φ : FormulaFinset α) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.FormulaFinset.Inconsistent 𝓢 Φ = ¬LO.Modal.FormulaFinset.Consistent 𝓢 Φ

theorem LO.Modal.FormulaFinset.iff_theory_consistent_formulae_consistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} : FormulaSet.Consistent 𝓢 ↑Φ ↔ Consistent 𝓢 Φ

theorem LO.Modal.FormulaFinset.iff_inconsistent_inconsistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} : FormulaSet.Inconsistent 𝓢 ↑Φ ↔ Inconsistent 𝓢 Φ

theorem LO.Modal.FormulaFinset.empty_conisistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} [Entailment.Classical 𝓢] [Entailment.Consistent 𝓢] : Consistent 𝓢 ∅

theorem LO.Modal.FormulaFinset.provable_iff_insert_neg_not_consistent {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} {φ : Formula α} [Entailment.Classical 𝓢] : Inconsistent 𝓢 (insert (∼φ) Φ) ↔ ↑Φ *⊢[𝓢]! φ

theorem LO.Modal.FormulaFinset.neg_provable_iff_insert_not_consistent {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} {φ : Formula α} [Entailment.Classical 𝓢] : Inconsistent 𝓢 (insert φ Φ) ↔ ↑Φ *⊢[𝓢]! ∼φ

theorem LO.Modal.FormulaFinset.unprovable_iff_singleton_neg_consistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {φ : Formula α} [Entailment.Classical 𝓢] : Consistent 𝓢 {∼φ} ↔ 𝓢 ⊬ φ

theorem LO.Modal.FormulaFinset.unprovable_iff_singleton_compl_consistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {φ : Formula α} [Entailment.Classical 𝓢] : Consistent 𝓢 {-φ} ↔ 𝓢 ⊬ φ

theorem LO.Modal.FormulaFinset.provable_iff_singleton_compl_inconsistent {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {φ : Formula α} [Entailment.Classical 𝓢] : Inconsistent 𝓢 {-φ} ↔ 𝓢 ⊢! φ

theorem LO.Modal.FormulaFinset.intro_union_consistent {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} [Entailment.Classical 𝓢] {P₁ P₂ : FormulaFinset α} (h : ∀ {Γ₁ Γ₂ : List (Formula α)}, ((∀ φ ∈ Γ₁, φ ∈ P₁) ∧ ∀ φ ∈ Γ₂, φ ∈ P₂) → 𝓢 ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ==> ⊥) : Consistent 𝓢 (P₁ ∪ P₂)

theorem LO.Modal.FormulaFinset.intro_triunion_consistent {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} [Entailment.Classical 𝓢] {P₁ P₂ P₃ : FormulaFinset α} (h : ∀ {Γ₁ Γ₂ Γ₃ : List (Formula α)}, ((∀ φ ∈ Γ₁, φ ∈ P₁) ∧ (∀ φ ∈ Γ₂, φ ∈ P₂) ∧ ∀ φ ∈ Γ₃, φ ∈ P₃) → 𝓢 ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ⋏ ⋀Γ₃ ==> ⊥) : Consistent 𝓢 (P₁ ∪ P₂ ∪ P₃)

noncomputable def LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.next {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] (𝓢 : S) (φ : Formula α) (Φ : FormulaFinset α) : FormulaFinset α

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.next 𝓢 φ Φ = if LO.Modal.FormulaFinset.Consistent 𝓢 (insert φ Φ) then insert φ Φ else insert (-φ) Φ

noncomputable def LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.enum {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] (𝓢 : S) (Φ : FormulaFinset α) : List (Formula α) → FormulaFinset α

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.enum 𝓢 Φ [] = Φ

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.next_consistent {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} [Entailment.Classical 𝓢] (Φ_consis : Consistent 𝓢 Φ) (φ : Formula α) : Consistent 𝓢 (next 𝓢 φ Φ)

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.enum_consistent {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} [Entailment.Classical 𝓢] (Φ_consis : Consistent 𝓢 Φ) {l : List (Formula α)} : Consistent 𝓢 (enum 𝓢 Φ l)

@[simp]

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.enum_nil {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} : enum 𝓢 Φ [] = Φ

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.enum_subset_step {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} {ψ : Formula α} {l : List (Formula α)} : enum 𝓢 Φ l ⊆ enum 𝓢 Φ (ψ :: l)

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.enum_subset {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} {l : List (Formula α)} : Φ ⊆ enum 𝓢 Φ l

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.either {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} {φ : Formula α} {l : List (Formula α)} (hp : φ ∈ l) : φ ∈ enum 𝓢 Φ l ∨ -φ ∈ enum 𝓢 Φ l

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed.subset {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Φ : FormulaFinset α} {l : List (Formula α)} {φ : Formula α} (h : φ ∈ enum 𝓢 Φ l) : φ ∈ Φ ∨ φ ∈ l ∨ ∃ ψ ∈ l, -ψ = φ

theorem LO.Modal.FormulaFinset.existsConsistentComplementaryClosed {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {P : FormulaFinset α} [Entailment.Classical 𝓢] {S✝ : FormulaFinset α} (h_sub : P ⊆ S✝⁻) (P_consis : Consistent 𝓢 P) : ∃ (P' : FormulaFinset α), P ⊆ P' ∧ Consistent 𝓢 P' ∧ P'.ComplementaryClosed S✝

@[reducible, inline]

abbrev LO.Modal.ComplementClosedConsistentFinset {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] (𝓢 : S) (Ψ : FormulaFinset α) : Type u_1

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.ComplementClosedConsistentFinset 𝓢 Ψ = { T : LO.Modal.FormulaFinset α // LO.Modal.FormulaFinset.Consistent 𝓢 T ∧ T.ComplementaryClosed Ψ }

@[implicit_reducible]

instance LO.Modal.ComplementClosedConsistentFinset.instMembershipFormula {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} : Membership (Formula α) (ComplementClosedConsistentFinset 𝓢 Ψ)

Equations

• LO.Modal.ComplementClosedConsistentFinset.instMembershipFormula = { mem := fun (X : LO.Modal.ComplementClosedConsistentFinset 𝓢 Ψ) (φ : LO.Modal.Formula α) => φ ∈ ↑X }

theorem LO.Modal.ComplementClosedConsistentFinset.consistent {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} (X : ComplementClosedConsistentFinset 𝓢 Ψ) : FormulaFinset.Consistent 𝓢 ↑X

theorem LO.Modal.ComplementClosedConsistentFinset.closed {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} (X : ComplementClosedConsistentFinset 𝓢 Ψ) : (↑X).ComplementaryClosed Ψ

@[simp]

theorem LO.Modal.ComplementClosedConsistentFinset.unprovable_falsum {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} : ↑↑X *⊬[𝓢] ⊥

theorem LO.Modal.ComplementClosedConsistentFinset.mem_compl_of_not_mem {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} {ψ : Formula α} (hs : ψ ∈ Ψ) : ψ ∉ X → -ψ ∈ X

theorem LO.Modal.ComplementClosedConsistentFinset.mem_of_not_mem_compl {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} {ψ : Formula α} (hs : ψ ∈ Ψ) : -ψ ∉ X → ψ ∈ X

theorem LO.Modal.ComplementClosedConsistentFinset.equality_def {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X₁ X₂ : ComplementClosedConsistentFinset 𝓢 Ψ} : X₁ = X₂ ↔ ↑X₁ = ↑X₂

theorem LO.Modal.ComplementClosedConsistentFinset.lindenbaum {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} [Entailment.Classical 𝓢] {Φ Ψ : FormulaFinset α} (X_sub : Φ ⊆ Ψ⁻) (X_consis : FormulaFinset.Consistent 𝓢 Φ) : ∃ (X' : ComplementClosedConsistentFinset 𝓢 Ψ), Φ ⊆ ↑X'

@[implicit_reducible]

noncomputable instance LO.Modal.ComplementClosedConsistentFinset.instInhabitedOfConsistentFormula {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} [Entailment.Classical 𝓢] [Entailment.Consistent 𝓢] : Inhabited (ComplementClosedConsistentFinset 𝓢 Ψ)

Equations

• LO.Modal.ComplementClosedConsistentFinset.instInhabitedOfConsistentFormula = { default := ⋯.choose }

theorem LO.Modal.ComplementClosedConsistentFinset.membership_iff {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} [Entailment.Classical 𝓢] {ψ : Formula α} (hq_sub : ψ ∈ Ψ) : ψ ∈ X ↔ ↑↑X *⊢[𝓢]! ψ

theorem LO.Modal.ComplementClosedConsistentFinset.mem_verum {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} [Entailment.Classical 𝓢] (h : ⊤ ∈ Ψ) : ⊤ ∈ X

@[simp]

theorem LO.Modal.ComplementClosedConsistentFinset.mem_falsum {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} [Entailment.Classical 𝓢] : ⊥ ∉ X

theorem LO.Modal.ComplementClosedConsistentFinset.iff_mem_compl {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} [Entailment.Classical 𝓢] {ψ : Formula α} (hq_sub : ψ ∈ Ψ) : ψ ∈ X ↔ -ψ ∉ X

theorem LO.Modal.ComplementClosedConsistentFinset.iff_mem_imp {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} [Entailment.Classical 𝓢] {ψ χ : Formula α} (hsub_qr : ψ ==> χ ∈ Ψ) (hsub_q : ψ ∈ Ψ := by trivial) (hsub_r : χ ∈ Ψ := by trivial) : ψ ==> χ ∈ X ↔ ψ ∈ X → -χ ∉ X

theorem LO.Modal.ComplementClosedConsistentFinset.iff_not_mem_imp {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} {X : ComplementClosedConsistentFinset 𝓢 Ψ} [Entailment.Classical 𝓢] {ψ χ : Formula α} (hsub_qr : ψ ==> χ ∈ Ψ) (hsub_q : ψ ∈ Ψ := by trivial) (hsub_r : χ ∈ Ψ := by trivial) : ψ ==> χ ∉ X ↔ ψ ∈ X ∧ -χ ∈ X

instance LO.Modal.ComplementClosedConsistentFinset.instFinite {α : Type u_1} [DecidableEq α] {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} {Ψ : FormulaFinset α} : Finite (ComplementClosedConsistentFinset 𝓢 Ψ)