Documentation

Foundation.Modal.Complement

Equations
@[simp]
theorem LO.Modal.Formula.complement.neg_def {α : Type u_1} {φ : Formula α} :
-(φ) = φ
@[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.FormulaFinset.complementary_mem {α : Type u_1} [DecidableEq α] {P : FormulaFinset α} {φ : Formula α} (h : φ P) :
φ P
theorem LO.Modal.FormulaFinset.complementary_comp {α : Type u_1} [DecidableEq α] {P : FormulaFinset α} {φ : Formula α} (h : φ P) :
-φ P
theorem LO.Modal.FormulaFinset.mem_of {α : Type u_1} [DecidableEq α] {P : FormulaFinset α} {φ : Formula α} (h : φ P) :
φ P ψP, -ψ = φ
theorem LO.Modal.FormulaFinset.complementary_mem_box {α : Type u_1} [DecidableEq α] {P : FormulaFinset α} {φ : Formula α} (hi : ∀ {ψ χ : Formula α}, ψ χ Pψ P) :
φ Pφ P
Instances
    theorem LO.Modal.complement_derive_bot {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} [Entailment.Cl 𝓢] {φ : Formula α} [DecidableEq α] (hp : 𝓢 ⊢! φ) (hcp : 𝓢 ⊢! -φ) :
    𝓢 ⊢!
    theorem LO.Modal.neg_complement_derive_bot {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} [Entailment.Cl 𝓢] {φ : Formula α} [DecidableEq α] (hp : 𝓢 ⊢! φ) (hcp : 𝓢 ⊢! -φ) :
    𝓢 ⊢!
    theorem LO.Modal.of_imply_complement_bot {α : Type u_1} {S : Type u_2} [Entailment (Formula α) S] {𝓢 : S} [Entailment.Cl 𝓢] {φ : Formula α} [DecidableEq α] (h : 𝓢 ⊢! -φ ) :
    𝓢 ⊢! φ