Complement

def LO.Modal.Formula.complement {α : Type u_1} : Formula α → Formula α

Imported declaration from the Incompleteness formalization.

Equations

• -φ.imp LO.Modal.Formula.falsum = φ
• -x✝ = ∼x✝

def LO.Modal.Formula.«term-_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

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} (φ : Formula α) : -φ = ∼φ ∨ ∃ (ψ : Formula α), ∼ψ = φ

def LO.Modal.FormulaFinset.complementary {α : Type u_1} [DecidableEq α] (P : FormulaFinset α) : FormulaFinset α

Imported declaration from the Incompleteness formalization.

Equations

• P⁻ = P ∪ Finset.image LO.Modal.Formula.complement P

def LO.Modal.FormulaFinset.«term_⁻» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.FormulaFinset.«term_⁻» = Lean.ParserDescr.trailingNode `LO.Modal.FormulaFinset.«term_⁻» 80 80 (Lean.ParserDescr.symbol "⁻")

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 := by trivial) : □φ ∈ P⁻ → □φ ∈ P

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

Equations

• P.SubformulaeComplementaryClosed φ = P.ComplementaryClosed φ.subformulas

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

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