Subformulas

def LO.Modal.Formula.subformulas {α : Type u_1} [DecidableEq α] : Formula α → FormulaFinset α

Imported declaration from the Incompleteness formalization.

Equations

• (LO.Modal.Formula.atom a).subformulas = {LO.Modal.Formula.atom a}
• LO.Modal.Formula.falsum.subformulas = {⊥}
• (φ.imp ψ).subformulas = insert (φ ==> ψ) (φ.subformulas ∪ ψ.subformulas)
• φ.box.subformulas = insert (□φ) φ.subformulas

@[simp]

theorem LO.Modal.Formula.subformulas.mem_self {α : Type u_1} [DecidableEq α] {φ : Formula α} : φ ∈ φ.subformulas

theorem LO.Modal.Formula.subformulas.mem_imp {α : Type u_1} [DecidableEq α] {φ ψ χ : Formula α} (h : ψ ==> χ ∈ φ.subformulas) : ψ ∈ φ.subformulas ∧ χ ∈ φ.subformulas

theorem LO.Modal.Formula.subformulas.mem_imp₁ {α : Type u_1} [DecidableEq α] {φ ψ χ : Formula α} (h : ψ ==> χ ∈ φ.subformulas) : ψ ∈ φ.subformulas

theorem LO.Modal.Formula.subformulas.mem_imp₂ {α : Type u_1} [DecidableEq α] {φ ψ χ : Formula α} (h : ψ ==> χ ∈ φ.subformulas) : χ ∈ φ.subformulas

theorem LO.Modal.Formula.subformulas.mem_box {α : Type u_1} [DecidableEq α] {φ ψ : Formula α} (h : □ψ ∈ φ.subformulas) : ψ ∈ φ.subformulas

@[simp]

theorem LO.Modal.Formula.subformulas.complexity_lower {α : Type u_1} [DecidableEq α] {φ ψ : Formula α} (h : ψ ∈ φ.subformulas) : ψ.complexity ≤ φ.complexity

class LO.Modal.FormulaSet.SubformulaClosed {α : Type u_1} (P : FormulaSet α) : Prop

Imported declaration from the Incompleteness formalization.

• imp_closed {φ ψ : Formula α} : φ ==> ψ ∈ P → φ ∈ P ∧ ψ ∈ P
• box_closed {φ : Formula α} : □φ ∈ P → φ ∈ P

theorem LO.Modal.FormulaSet.SubformulaClosed.mem_imp₁ {α : Type u_1} {φ : Formula α} {P : FormulaSet α} [hP : P.SubformulaClosed] {ψ : Formula α} (h : φ ==> ψ ∈ P) : φ ∈ P

theorem LO.Modal.FormulaSet.SubformulaClosed.mem_imp₂ {α : Type u_1} {φ : Formula α} {P : FormulaSet α} [hP : P.SubformulaClosed] {ψ : Formula α} (h : φ ==> ψ ∈ P) : ψ ∈ P

theorem LO.Modal.FormulaSet.SubformulaClosed.mem_box {α : Type u_1} {φ : Formula α} {P : FormulaSet α} [hP : P.SubformulaClosed] (h : □φ ∈ P) : φ ∈ P

instance LO.Modal.FormulaSet.SubformulaClosed.instCoeFormulaFinsetFormulaSubformulas {α : Type u_1} {φ : Formula α} [DecidableEq α] : SubformulaClosed ↑φ.subformulas