Documentation

Foundation.Modal.Complemental

Equations
  • -x = match x with | p.imp LO.Modal.Formula.falsum => p | p => p
Instances For
    @[simp]
    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.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
    Instances For
      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 Pq P) _auto✝) :
      p Pp P
      Instances
        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 Sp P -p P
        Equations
        • P.SubformulaeComplementaryClosed p = P.ComplementaryClosed (𝒮 p)
        Instances For
          Equations
          Instances For
            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₂)Λ Γ₁ Γ₂ ) :
            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₃)Λ Γ₁ Γ₂ Γ₃ ) :
            Equations
            Instances For
              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
              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
                Equations
                • LO.Modal.ComplementaryClosedConsistentFormulae.instInhabitedCCFOfConsistentFormulaHilbert = { default := .choose }
                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) :
                qX.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) :
                -qX.formulaeq 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
                @[simp]
                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 -qX.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-rX.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 rX.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