Instances For
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))
Instances For
@[simp]
@[simp]
theorem
LO.Modal.Formula.complement.imp_def₁
{α : Type u_1}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(hq : q ≠ ⊥)
:
theorem
LO.Modal.Formula.complement.imp_def₂
{α : Type u_1}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(hq : q = ⊥)
:
theorem
LO.Modal.Formula.complement.resort_box
{α : Type u_1}
{p : LO.Modal.Formula α}
{q : LO.Modal.Formula α}
(h : -p = □q)
:
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)
:
Equations
- P⁻ = P ∪ Finset.image LO.Modal.Formula.complement P
Instances For
Equations
- LO.Modal.Formulae.«term_⁻» = Lean.ParserDescr.trailingNode `LO.Modal.Formulae.term_⁻ 80 80 (Lean.ParserDescr.symbol "⁻")
Instances For
theorem
LO.Modal.Formulae.complementary_mem
{α : Type u_1}
[DecidableEq α]
{P : LO.Modal.Formulae α}
{p : LO.Modal.Formula α}
(h : p ∈ P)
:
theorem
LO.Modal.Formulae.complementary_comp
{α : Type u_1}
[DecidableEq α]
{P : LO.Modal.Formulae α}
{p : LO.Modal.Formula α}
(h : 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✝)
:
class
LO.Modal.Formulae.ComplementaryClosed
{α : Type u_1}
[DecidableEq α]
(P : LO.Modal.Formulae α)
(S : LO.Modal.Formulae α)
:
Instances
theorem
LO.Modal.Formulae.ComplementaryClosed.subset
{α : Type u_1}
[DecidableEq α]
{P : LO.Modal.Formulae α}
{S : LO.Modal.Formulae α}
[self : P.ComplementaryClosed 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 α)
:
def
LO.Modal.Formulae.SubformulaeComplementaryClosed
{α : Type u_1}
[DecidableEq α]
(P : LO.Modal.Formulae α)
(p : LO.Modal.Formula α)
:
Instances For
def
LO.Modal.Formulae.Consistent
{α : Type u_1}
(Λ : LO.Modal.Hilbert α)
(P : LO.Modal.Formulae α)
:
Equations
- LO.Modal.Formulae.Consistent Λ P = ↑P *⊬[Λ] ⊥
Instances For
@[simp]
theorem
LO.Modal.Formulae.iff_theory_consistent_formulae_consistent
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
{P : LO.Modal.Formulae α}
:
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 α}
:
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 α}
:
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 Λ]
:
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 α)
:
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
Instances For
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
Instances For
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 α)
:
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 α)}
:
@[simp]
theorem
LO.Modal.Formulae.exists_consistent_complementary_closed.enum_nil
{α : Type u_1}
[DecidableEq α]
(Λ : LO.Modal.Hilbert α)
{P : LO.Modal.Formulae α}
:
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 α)}
:
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 α)}
:
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)
:
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)
:
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
Instances For
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
.
Instances For
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}
:
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)
:
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)
:
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)
:
theorem
LO.Modal.ComplementaryClosedConsistentFormulae.mem_verum
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Hilbert α}
{S : LO.Modal.Formulae α}
{X : LO.Modal.CCF Λ S}
(h : ⊤ ∈ S)
:
@[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)
:
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✝)
:
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✝)
:
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}
:
instance
LO.Modal.ComplementaryClosedConsistentFormulae.instFiniteCCF
{α : Type u_1}
[DecidableEq α]
{Λ : LO.Modal.Hilbert α}
{S : LO.Modal.Formulae α}
:
Finite (LO.Modal.CCF Λ S)
Equations
- ⋯ = ⋯