Documentation

Complexity.Logics.FirstOrder.Subformula

Subformulas #

The subformulas of a bounded formula of Mathlib's first-order logic, each with its number of bound variables (Cslib.Logic.FO.subformulas). They form a finite set, closed under taking subformulas: the operands of an implication and the body of a universal quantification of a subformula are subformulas.

Main definitions #

Main results #

References #

source
def Cslib.Logic.FO.subformulas {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} :
L.BoundedFormula α n → Set ((k : ℕ) × L.BoundedFormula α k)

The subformulas of a bounded formula, each with its number of bound variables.

Instances For
    source
    theorem Cslib.Logic.FO.self_mem_subformulas {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α n) :
    ⟨n, φ⟩ ∈ subformulas φ

    A formula is one of its own subformulas.

    source
    theorem Cslib.Logic.FO.finite_subformulas {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α n) :
    (subformulas φ).Finite

    A formula has finitely many subformulas.

    source
    theorem Cslib.Logic.FO.subformulas_subset {L : FirstOrder.Language} {α : Type u_1} {n k : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α k} (h : ⟨k, ψ⟩ ∈ subformulas φ) :
    subformulas ψ ⊆ subformulas φ

    The subformulas of a subformula are subformulas.

    source
    theorem Cslib.Logic.FO.mem_subformulas_of_imp_left {L : FirstOrder.Language} {α : Type u_1} {n k : ℕ} {φ : L.BoundedFormula α n} {ψ χ : L.BoundedFormula α k} (h : ⟨k, ψ.imp χ⟩ ∈ subformulas φ) :
    ⟨k, ψ⟩ ∈ subformulas φ

    The antecedent of an implication among the subformulas is a subformula.

    source
    theorem Cslib.Logic.FO.mem_subformulas_of_imp_right {L : FirstOrder.Language} {α : Type u_1} {n k : ℕ} {φ : L.BoundedFormula α n} {ψ χ : L.BoundedFormula α k} (h : ⟨k, ψ.imp χ⟩ ∈ subformulas φ) :
    ⟨k, χ⟩ ∈ subformulas φ

    The consequent of an implication among the subformulas is a subformula.

    source
    theorem Cslib.Logic.FO.mem_subformulas_of_all {L : FirstOrder.Language} {α : Type u_1} {n k : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α (k + 1)} (h : ⟨k, ψ.all⟩ ∈ subformulas φ) :
    ⟨k + 1, ψ⟩ ∈ subformulas φ

    The body of a universal quantification among the subformulas is a subformula.