Documentation

Mathlib.ModelTheory.Complexity

Quantifier Complexity #

This file defines quantifier complexity of first-order formulas, and constructs prenex normal forms.

Main Definitions #

Main Results #

inductive FirstOrder.Language.BoundedFormula.IsAtomic {L : FirstOrder.Language} {α : Type u'} {n : } :
L.BoundedFormula α nProp

An atomic formula is either equality or a relation symbol applied to terms. Note that and are not considered atomic in this convention.

Instances For
    theorem FirstOrder.Language.BoundedFormula.not_all_isAtomic {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α (n + 1)) :
    ¬φ.all.IsAtomic
    theorem FirstOrder.Language.BoundedFormula.not_ex_isAtomic {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α (n + 1)) :
    ¬φ.ex.IsAtomic
    theorem FirstOrder.Language.BoundedFormula.IsAtomic.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } {m : } {φ : L.BoundedFormula α m} (h : φ.IsAtomic) (f : αβ Fin n) :
    theorem FirstOrder.Language.BoundedFormula.IsAtomic.liftAt {L : FirstOrder.Language} {α : Type u'} {l : } {φ : L.BoundedFormula α l} {k : } {m : } (h : φ.IsAtomic) :
    theorem FirstOrder.Language.BoundedFormula.IsAtomic.castLE {L : FirstOrder.Language} {α : Type u'} {n : } {l : } {φ : L.BoundedFormula α l} {h : l n} (hφ : φ.IsAtomic) :
    inductive FirstOrder.Language.BoundedFormula.IsQF {L : FirstOrder.Language} {α : Type u'} {n : } :
    L.BoundedFormula α nProp

    A quantifier-free formula is a formula defined without quantifiers. These are all equivalent to boolean combinations of atomic formulas.

    Instances For
      theorem FirstOrder.Language.BoundedFormula.IsAtomic.isQF {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} :
      φ.IsAtomicφ.IsQF
      theorem FirstOrder.Language.BoundedFormula.IsQF.not {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} (h : φ.IsQF) :
      φ.not.IsQF
      theorem FirstOrder.Language.BoundedFormula.IsQF.sup {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsQF) :
      (φ ψ).IsQF
      theorem FirstOrder.Language.BoundedFormula.IsQF.inf {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsQF) :
      (φ ψ).IsQF
      theorem FirstOrder.Language.BoundedFormula.IsQF.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } {m : } {φ : L.BoundedFormula α m} (h : φ.IsQF) (f : αβ Fin n) :
      theorem FirstOrder.Language.BoundedFormula.IsQF.liftAt {L : FirstOrder.Language} {α : Type u'} {l : } {φ : L.BoundedFormula α l} {k : } {m : } (h : φ.IsQF) :
      theorem FirstOrder.Language.BoundedFormula.IsQF.castLE {L : FirstOrder.Language} {α : Type u'} {n : } {l : } {φ : L.BoundedFormula α l} {h : l n} (hφ : φ.IsQF) :
      theorem FirstOrder.Language.BoundedFormula.not_all_isQF {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α (n + 1)) :
      ¬φ.all.IsQF
      theorem FirstOrder.Language.BoundedFormula.not_ex_isQF {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α (n + 1)) :
      ¬φ.ex.IsQF
      inductive FirstOrder.Language.BoundedFormula.IsPrenex {L : FirstOrder.Language} {α : Type u'} {n : } :
      L.BoundedFormula α nProp

      Indicates that a bounded formula is in prenex normal form - that is, it consists of quantifiers applied to a quantifier-free formula.

      Instances For
        theorem FirstOrder.Language.BoundedFormula.IsQF.isPrenex {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} :
        φ.IsQFφ.IsPrenex
        theorem FirstOrder.Language.BoundedFormula.IsAtomic.isPrenex {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} (h : φ.IsAtomic) :
        φ.IsPrenex
        theorem FirstOrder.Language.BoundedFormula.IsPrenex.induction_on_all_not {L : FirstOrder.Language} {α : Type u'} {n : } {P : {n : } → L.BoundedFormula α nProp} {φ : L.BoundedFormula α n} (h : φ.IsPrenex) (hq : ∀ {m : } {ψ : L.BoundedFormula α m}, ψ.IsQFP ψ) (ha : ∀ {m : } {ψ : L.BoundedFormula α (m + 1)}, P ψP ψ.all) (hn : ∀ {m : } {ψ : L.BoundedFormula α m}, P ψP ψ.not) :
        P φ
        theorem FirstOrder.Language.BoundedFormula.IsPrenex.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } {m : } {φ : L.BoundedFormula α m} (h : φ.IsPrenex) (f : αβ Fin n) :
        theorem FirstOrder.Language.BoundedFormula.IsPrenex.castLE {L : FirstOrder.Language} {α : Type u'} {l : } {φ : L.BoundedFormula α l} (hφ : φ.IsPrenex) {n : } {h : l n} :
        theorem FirstOrder.Language.BoundedFormula.IsPrenex.liftAt {L : FirstOrder.Language} {α : Type u'} {l : } {φ : L.BoundedFormula α l} {k : } {m : } (h : φ.IsPrenex) :
        def FirstOrder.Language.BoundedFormula.toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : } :
        L.BoundedFormula α nL.BoundedFormula α nL.BoundedFormula α n

        An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex. If φ is quantifier-free and ψ is in prenex normal form, then φ.toPrenexImpRight ψ is a prenex normal form for φ.imp ψ.

        Equations
        Instances For
          theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} :
          ψ.IsQFφ.toPrenexImpRight ψ = φ.imp ψ
          theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsPrenex) :
          (φ.toPrenexImpRight ψ).IsPrenex
          def FirstOrder.Language.BoundedFormula.toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : } :
          L.BoundedFormula α nL.BoundedFormula α nL.BoundedFormula α n

          An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex. If φ and ψ are in prenex normal form, then φ.toPrenexImp ψ is a prenex normal form for φ.imp ψ.

          Equations
          Instances For
            theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} :
            φ.IsQFφ.toPrenexImp ψ = φ.toPrenexImpRight ψ
            theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImp {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsPrenex) (hψ : ψ.IsPrenex) :
            (φ.toPrenexImp ψ).IsPrenex
            def FirstOrder.Language.BoundedFormula.toPrenex {L : FirstOrder.Language} {α : Type u'} {n : } :
            L.BoundedFormula α nL.BoundedFormula α n

            For any bounded formula φ, φ.toPrenex is a semantically-equivalent formula in prenex normal form.

            Equations
            Instances For
              theorem FirstOrder.Language.BoundedFormula.toPrenex_isPrenex {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α n) :
              φ.toPrenex.IsPrenex
              theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } [Nonempty M] {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsPrenex) {v : αM} {xs : Fin nM} :
              (φ.toPrenexImpRight ψ).Realize v xs (φ.imp ψ).Realize v xs
              theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImp {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } [Nonempty M] {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (hφ : φ.IsPrenex) (hψ : ψ.IsPrenex) {v : αM} {xs : Fin nM} :
              (φ.toPrenexImp ψ).Realize v xs (φ.imp ψ).Realize v xs
              @[simp]
              theorem FirstOrder.Language.BoundedFormula.realize_toPrenex {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } [Nonempty M] (φ : L.BoundedFormula α n) {v : αM} {xs : Fin nM} :
              φ.toPrenex.Realize v xs φ.Realize v xs
              theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not {L : FirstOrder.Language} {α : Type u'} {n : } {P : L.BoundedFormula α nProp} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomicP ψ) (hsup : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁P φ₂P (φ₁ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φP φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, .Iff φ₁ φ₂(P φ₁ P φ₂)) :
              P φ
              theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_inf_not {L : FirstOrder.Language} {α : Type u'} {n : } {P : L.BoundedFormula α nProp} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomicP ψ) (hinf : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁P φ₂P (φ₁ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φP φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, .Iff φ₁ φ₂(P φ₁ P φ₂)) :
              P φ
              theorem FirstOrder.Language.BoundedFormula.iff_toPrenex {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α n) :
              .Iff φ φ.toPrenex
              theorem FirstOrder.Language.BoundedFormula.induction_on_all_ex {L : FirstOrder.Language} {α : Type u'} {n : } {P : {m : } → L.BoundedFormula α mProp} (φ : L.BoundedFormula α n) (hqf : ∀ {m : } {ψ : L.BoundedFormula α m}, ψ.IsQFP ψ) (hall : ∀ {m : } {ψ : L.BoundedFormula α (m + 1)}, P ψP ψ.all) (hex : ∀ {m : } {φ : L.BoundedFormula α (m + 1)}, P φP φ.ex) (hse : ∀ {m : } {φ₁ φ₂ : L.BoundedFormula α m}, .Iff φ₁ φ₂(P φ₁ P φ₂)) :
              P φ
              theorem FirstOrder.Language.BoundedFormula.induction_on_exists_not {L : FirstOrder.Language} {α : Type u'} {n : } {P : {m : } → L.BoundedFormula α mProp} (φ : L.BoundedFormula α n) (hqf : ∀ {m : } {ψ : L.BoundedFormula α m}, ψ.IsQFP ψ) (hnot : ∀ {m : } {φ : L.BoundedFormula α m}, P φP φ.not) (hex : ∀ {m : } {φ : L.BoundedFormula α (m + 1)}, P φP φ.ex) (hse : ∀ {m : } {φ₁ φ₂ : L.BoundedFormula α m}, .Iff φ₁ φ₂(P φ₁ P φ₂)) :
              P φ
              inductive FirstOrder.Language.BoundedFormula.IsUniversal {L : FirstOrder.Language} {α : Type u'} {n : } :
              L.BoundedFormula α nProp

              A universal formula is a formula defined by applying only universal quantifiers to a quantifier-free formula.

              Instances For
                theorem FirstOrder.Language.BoundedFormula.IsQF.isUniversal {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} :
                φ.IsQFφ.IsUniversal
                theorem FirstOrder.Language.BoundedFormula.IsAtomic.isUniversal {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} (h : φ.IsAtomic) :
                φ.IsUniversal
                inductive FirstOrder.Language.BoundedFormula.IsExistential {L : FirstOrder.Language} {α : Type u'} {n : } :
                L.BoundedFormula α nProp

                An existential formula is a formula defined by applying only existential quantifiers to a quantifier-free formula.

                Instances For
                  theorem FirstOrder.Language.BoundedFormula.IsQF.isExistential {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} :
                  φ.IsQFφ.IsExistential
                  theorem FirstOrder.Language.BoundedFormula.IsAtomic.isExistential {L : FirstOrder.Language} {α : Type u'} {n : } {φ : L.BoundedFormula α n} (h : φ.IsAtomic) :
                  φ.IsExistential
                  theorem FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective {L : FirstOrder.Language} {α : Type u'} {n : } {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [FunLike F M N] {φ : L.BoundedFormula α n} (hA : φ.IsAtomic) [L.HomClass F M N] {f : F} (hInj : Function.Injective f) {v : αM} {xs : Fin nM} :
                  φ.Realize v xsφ.Realize (f v) (f xs)
                  theorem FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp {L : FirstOrder.Language} {α : Type u'} {n : } {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [FunLike F M N] {φ : L.BoundedFormula α n} (hA : φ.IsAtomic) [EmbeddingLike F M N] [L.HomClass F M N] (f : F) {v : αM} {xs : Fin nM} :
                  φ.Realize v xsφ.Realize (f v) (f xs)
                  theorem FirstOrder.Language.BoundedFormula.IsQF.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : } {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] {φ : L.BoundedFormula α n} (hQF : φ.IsQF) (f : F) {v : αM} {xs : Fin nM} :
                  φ.Realize (f v) (f xs) φ.Realize v xs
                  theorem FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : } {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] {φ : L.BoundedFormula α n} (hU : φ.IsUniversal) (f : F) {v : αM} {xs : Fin nM} :
                  φ.Realize (f v) (f xs)φ.Realize v xs
                  theorem FirstOrder.Language.BoundedFormula.IsExistential.realize_embedding {L : FirstOrder.Language} {α : Type u'} {n : } {M : Type u_4} [L.Structure M] {N : Type u_5} [L.Structure N] {F : Type u_6} [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] {φ : L.BoundedFormula α n} (hE : φ.IsExistential) (f : F) {v : αM} {xs : Fin nM} :
                  φ.Realize v xsφ.Realize (f v) (f xs)

                  A theory is universal when it is comprised only of universal sentences - these theories apply also to substructures.

                  Instances
                    theorem FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem {L : FirstOrder.Language} {T : L.Theory} [self : T.IsUniversal] ⦃φ : L.Sentence :
                    theorem FirstOrder.Language.Theory.IsUniversal.models_of_embedding {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T : L.Theory} [hT : T.IsUniversal] {N : Type u_4} [L.Structure N] [N T] (f : L.Embedding M N) :
                    M T
                    instance FirstOrder.Language.Substructure.models_of_isUniversal {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) (T : L.Theory) [T.IsUniversal] [M T] :
                    S T
                    Equations
                    • =
                    theorem FirstOrder.Language.Theory.IsUniversal.insert {L : FirstOrder.Language} {T : L.Theory} [hT : T.IsUniversal] {φ : L.Sentence} (hφ : FirstOrder.Language.BoundedFormula.IsUniversal φ) :
                    (insert φ T).IsUniversal
                    theorem FirstOrder.Language.Relations.isAtomic {L : FirstOrder.Language} {α : Type u'} {n : } {l : } (r : L.Relations l) (ts : Fin lL.Term (α Fin n)) :
                    (r.boundedFormula ts).IsAtomic
                    theorem FirstOrder.Language.Relations.isQF {L : FirstOrder.Language} {α : Type u'} {n : } {l : } (r : L.Relations l) (ts : Fin lL.Term (α Fin n)) :
                    (r.boundedFormula ts).IsQF