Documentation

Foundation.FirstOrder.Basic.Syntax.Formula

Formulas of first-order logic #

This file defines the formulas of first-order logic.

φ : Semiformula L ξ n is a (semi-)formula of language L with bounded variables of Fin n and free variables of ξ. The quantification is represented by de Bruijn index.

inductive LO.FirstOrder.Semiformula (L : LO.FirstOrder.Language) (ξ : Type u_1) :
Type (max u_1 u_2)
Instances For
    @[reducible, inline]
    abbrev LO.FirstOrder.Formula (L : LO.FirstOrder.Language) (ξ : Type u_1) :
    Type (max u_1 u_2)
    Equations
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          Equations
          Instances For
            theorem LO.FirstOrder.Semiformula.neg_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ n) :
            φ.neg.neg = φ
            Equations
            • LO.FirstOrder.Semiformula.instLogicalConnective = LO.LogicalConnective.mk
            Equations
            • LO.FirstOrder.Semiformula.instQuantifier = LO.Quantifier.mk
            def LO.FirstOrder.Semiformula.toStr {L : LO.FirstOrder.Language} {ξ : Type u_1} [(k : ) → ToString (L.Func k)] [(k : ) → ToString (L.Rel k)] [ToString ξ] {n : } :
            Equations
            Instances For
              instance LO.FirstOrder.Semiformula.instRepr {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [(k : ) → ToString (L.Func k)] [(k : ) → ToString (L.Rel k)] [ToString ξ] :
              Equations
              instance LO.FirstOrder.Semiformula.instToString {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [(k : ) → ToString (L.Func k)] [(k : ) → ToString (L.Rel k)] [ToString ξ] :
              Equations
              • LO.FirstOrder.Semiformula.instToString = { toString := LO.FirstOrder.Semiformula.toStr }
              @[simp]
              theorem LO.FirstOrder.Semiformula.neg_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
              (φ ψ) = φ ψ
              @[simp]
              theorem LO.FirstOrder.Semiformula.neg_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
              (φ ψ) = φ ψ
              @[simp]
              @[simp]
              @[simp]
              theorem LO.FirstOrder.Semiformula.neg_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
              φ = ψ φ = ψ
              theorem LO.FirstOrder.Semiformula.imp_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
              φ ψ = φ ψ
              theorem LO.FirstOrder.Semiformula.iff_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
              φ ψ = (φ ψ) (ψ φ)
              theorem LO.FirstOrder.Semiformula.ball_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
              (∀[φ] ψ) = ∀' (φ ψ)
              theorem LO.FirstOrder.Semiformula.bex_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
              (∃[φ] ψ) = ∃' φ ψ
              @[simp]
              theorem LO.FirstOrder.Semiformula.neg_ball {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
              (∀[φ] ψ) = ∃[φ] ψ
              @[simp]
              theorem LO.FirstOrder.Semiformula.neg_bex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
              (∃[φ] ψ) = ∀[φ] ψ
              @[simp]
              theorem LO.FirstOrder.Semiformula.and_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ₁ ψ₁ φ₂ ψ₂ : LO.FirstOrder.Semiformula L ξ n) :
              φ₁ φ₂ = ψ₁ ψ₂ φ₁ = ψ₁ φ₂ = ψ₂
              @[simp]
              theorem LO.FirstOrder.Semiformula.or_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ₁ ψ₁ φ₂ ψ₂ : LO.FirstOrder.Semiformula L ξ n) :
              φ₁ φ₂ = ψ₁ ψ₂ φ₁ = ψ₁ φ₂ = ψ₂
              @[simp]
              theorem LO.FirstOrder.Semiformula.all_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
              ∀' φ = ∀' ψ φ = ψ
              @[simp]
              theorem LO.FirstOrder.Semiformula.ex_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
              ∃' φ = ∃' ψ φ = ψ
              @[simp]
              @[simp]
              @[simp]
              theorem LO.FirstOrder.Semiformula.univItr_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + k)) :
              ∀^[k] φ = ∀^[k] ψ φ = ψ
              @[simp]
              theorem LO.FirstOrder.Semiformula.exItr_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (φ ψ : LO.FirstOrder.Semiformula L ξ (n + k)) :
              ∃^[k] φ = ∃^[k] ψ φ = ψ
              @[simp]
              theorem LO.FirstOrder.Semiformula.imp_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ₁ φ₂ ψ₁ ψ₂ : LO.FirstOrder.Semiformula L ξ n} :
              φ₁ φ₂ = ψ₁ ψ₂ φ₁ = ψ₁ φ₂ = ψ₂
              @[reducible, inline]
              abbrev LO.FirstOrder.Semiformula.rel! {ξ : Type u_1} {n : } (L : LO.FirstOrder.Language) (k : ) (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
              Equations
              Instances For
                @[reducible, inline]
                abbrev LO.FirstOrder.Semiformula.nrel! {ξ : Type u_1} {n : } (L : LO.FirstOrder.Language) (k : ) (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                Equations
                Instances For
                  Equations
                  • LO.FirstOrder.Semiformula.verum.complexity = 0
                  • LO.FirstOrder.Semiformula.falsum.complexity = 0
                  • (LO.FirstOrder.Semiformula.rel r v).complexity = 0
                  • (LO.FirstOrder.Semiformula.nrel r v).complexity = 0
                  • (φ.and ψ).complexity = φ.complexity ψ.complexity + 1
                  • (φ.or ψ).complexity = φ.complexity ψ.complexity + 1
                  • φ.all.complexity = φ.complexity + 1
                  • φ.ex.complexity = φ.complexity + 1
                  Instances For
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } :
                    .complexity = 0
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_bot {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } :
                    .complexity = 0
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                    (LO.FirstOrder.Semiformula.rel r v).complexity = 0
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                    (φ ψ).complexity = φ.complexity ψ.complexity + 1
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_and' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                    (φ.and ψ).complexity = φ.complexity ψ.complexity + 1
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                    (φ ψ).complexity = φ.complexity ψ.complexity + 1
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_or' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                    (φ.or ψ).complexity = φ.complexity ψ.complexity + 1
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                    (∀' φ).complexity = φ.complexity + 1
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_all' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                    φ.all.complexity = φ.complexity + 1
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                    (∃' φ).complexity = φ.complexity + 1
                    @[simp]
                    theorem LO.FirstOrder.Semiformula.complexity_ex' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                    φ.ex.complexity = φ.complexity + 1
                    def LO.FirstOrder.Semiformula.cases' {L : LO.FirstOrder.Language} {ξ : Type u_1} {C : (n : ) → LO.FirstOrder.Semiformula L ξ nSort w} (hverum : {n : } → C n ) (hfalsum : {n : } → C n ) (hrel : {n k : } → (r : L.Rel k) → (v : Fin kLO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.rel r v)) (hnrel : {n k : } → (r : L.Rel k) → (v : Fin kLO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.nrel r v)) (hand : {n : } → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n (φ ψ)) (hor : {n : } → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n (φ ψ)) (hall : {n : } → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C n (∀' φ)) (hex : {n : } → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C n (∃' φ)) {n : } (φ : LO.FirstOrder.Semiformula L ξ n) :
                    C n φ
                    Equations
                    Instances For
                      def LO.FirstOrder.Semiformula.rec' {L : LO.FirstOrder.Language} {ξ : Type u_1} {C : (n : ) → LO.FirstOrder.Semiformula L ξ nSort w} (hverum : {n : } → C n ) (hfalsum : {n : } → C n ) (hrel : {n k : } → (r : L.Rel k) → (v : Fin kLO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.rel r v)) (hnrel : {n k : } → (r : L.Rel k) → (v : Fin kLO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.nrel r v)) (hand : {n : } → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n φC n ψC n (φ ψ)) (hor : {n : } → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n φC n ψC n (φ ψ)) (hall : {n : } → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C (n + 1) φC n (∀' φ)) (hex : {n : } → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C (n + 1) φC n (∃' φ)) {n : } (φ : LO.FirstOrder.Semiformula L ξ n) :
                      C n φ
                      Equations
                      Instances For
                        @[simp]
                        theorem LO.FirstOrder.Semiformula.complexity_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ n) :
                        (φ).complexity = φ.complexity
                        def LO.FirstOrder.Semiformula.hasDecEq {L : LO.FirstOrder.Language} {ξ : Type u_1} [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] [DecidableEq ξ] {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                        Decidable (φ = ψ)
                        Instances For
                          instance LO.FirstOrder.Semiformula.instDecidableEq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] [DecidableEq ξ] :
                          Equations
                          • LO.FirstOrder.Semiformula.instDecidableEq = LO.FirstOrder.Semiformula.hasDecEq

                          Quantifier Rank

                          Equations
                          Instances For
                            @[simp]
                            @[simp]
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                            (φ ψ).qr = φ.qr ψ.qr
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                            (φ ψ).qr = φ.qr ψ.qr
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                            (∀' φ).qr = φ.qr + 1
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                            (∃' φ).qr = φ.qr + 1
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ : LO.FirstOrder.Semiformula L ξ n) :
                            (φ).qr = φ.qr
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_imply {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                            (φ ψ).qr = φ.qr ψ.qr
                            @[simp]
                            theorem LO.FirstOrder.Semiformula.qr_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                            (φ ψ).qr = φ.qr ψ.qr

                            Open (Semi-)Formula

                            Equations
                            • φ.Open = (φ.qr = 0)
                            Instances For
                              @[simp]
                              @[simp]
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.open_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.open_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.open_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ ψ : LO.FirstOrder.Semiformula L ξ n} :
                              (φ ψ).Open φ.Open ψ.Open
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.open_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ ψ : LO.FirstOrder.Semiformula L ξ n} :
                              (φ ψ).Open φ.Open ψ.Open
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.not_open_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} :
                              ¬(∀' φ).Open
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.not_open_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} :
                              ¬(∃' φ).Open
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.open_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ : LO.FirstOrder.Semiformula L ξ n} :
                              (φ).Open φ.Open
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.open_imply {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ ψ : LO.FirstOrder.Semiformula L ξ n} :
                              (φ ψ).Open φ.Open ψ.Open
                              @[simp]
                              theorem LO.FirstOrder.Semiformula.open_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ ψ : LO.FirstOrder.Semiformula L ξ n} :
                              (φ ψ).Open φ.Open ψ.Open

                              Free Variables

                              Equations
                              • (LO.FirstOrder.Semiformula.rel a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables
                              • (LO.FirstOrder.Semiformula.nrel a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables
                              • LO.FirstOrder.Semiformula.verum.freeVariables =
                              • LO.FirstOrder.Semiformula.falsum.freeVariables =
                              • (φ.and ψ).freeVariables = φ.freeVariables ψ.freeVariables
                              • (φ.or ψ).freeVariables = φ.freeVariables ψ.freeVariables
                              • φ.all.freeVariables = φ.freeVariables
                              • φ.ex.freeVariables = φ.freeVariables
                              Instances For
                                theorem LO.FirstOrder.Semiformula.freeVariables_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] {k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                                (LO.FirstOrder.Semiformula.rel r v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables
                                theorem LO.FirstOrder.Semiformula.freeVariables_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] {k : } (r : L.Rel k) (v : Fin kLO.FirstOrder.Semiterm L ξ n) :
                                (LO.FirstOrder.Semiformula.nrel r v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables
                                @[simp]
                                @[simp]
                                @[simp]
                                theorem LO.FirstOrder.Semiformula.freeVariables_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                                (φ ψ).freeVariables = φ.freeVariables ψ.freeVariables
                                @[simp]
                                theorem LO.FirstOrder.Semiformula.freeVariables_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                                (φ ψ).freeVariables = φ.freeVariables ψ.freeVariables
                                @[simp]
                                theorem LO.FirstOrder.Semiformula.freeVariables_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                                (∀' φ).freeVariables = φ.freeVariables
                                @[simp]
                                theorem LO.FirstOrder.Semiformula.freeVariables_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                                (∃' φ).freeVariables = φ.freeVariables
                                @[simp]
                                theorem LO.FirstOrder.Semiformula.freeVariables_not {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (φ : LO.FirstOrder.Semiformula L ξ n) :
                                (φ).freeVariables = φ.freeVariables
                                @[simp]
                                theorem LO.FirstOrder.Semiformula.freeVariables_imp {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                                (φ ψ).freeVariables = φ.freeVariables ψ.freeVariables
                                @[simp]
                                theorem LO.FirstOrder.Semiformula.freeVariables_univClosure {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (φ : LO.FirstOrder.Semiformula L ξ n) :
                                (∀* φ).freeVariables = φ.freeVariables
                                @[simp]
                                @[reducible, inline]
                                Equations
                                • φ.FVar? x = (x φ.freeVariables)
                                Instances For
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] {x : ξ} {k : } {R : L.Rel k} {v : Fin kLO.FirstOrder.Semiterm L ξ n} :
                                  (LO.FirstOrder.Semiformula.rel R v).FVar? x ∃ (i : Fin k), (v i).FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] {x : ξ} {k : } {R : L.Rel k} {v : Fin kLO.FirstOrder.Semiterm L ξ n} :
                                  (LO.FirstOrder.Semiformula.nrel R v).FVar? x ∃ (i : Fin k), (v i).FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (x : ξ) :
                                  ¬.FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_falsum {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (x : ξ) :
                                  ¬.FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (x : ξ) (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                                  (φ ψ).FVar? x φ.FVar? x ψ.FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (x : ξ) (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                                  (φ ψ).FVar? x φ.FVar? x ψ.FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (x : ξ) (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                                  (∀' φ).FVar? x φ.FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (x : ξ) (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) :
                                  (∃' φ).FVar? x φ.FVar? x
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.fvar?_univClosure {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] (x : ξ) (φ : LO.FirstOrder.Semiformula L ξ n) :
                                  (∀* φ).FVar? x φ.FVar? x
                                  theorem LO.FirstOrder.Semiformula.List.maximam?_some_of_not_nil {α : Type u_5} [LinearOrder α] {l : List α} (h : l []) :
                                  l.max?.isSome = true
                                  theorem LO.FirstOrder.Semiformula.List.maximam?_eq_some {α : Type u_5} [LinearOrder α] {l : List α} {a : α} (h : l.max? = some a) (x : α) :
                                  x lx a
                                  theorem LO.FirstOrder.Semiformula.ne_of_ne_complexity {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {φ ψ : LO.FirstOrder.Semiformula L ξ n} (h : φ.complexity ψ.complexity) :
                                  φ ψ
                                  @[simp]
                                  theorem LO.FirstOrder.Semiformula.ne_or_left {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (φ ψ : LO.FirstOrder.Semiformula L ξ n) :
                                  φ φ ψ
                                  @[simp]
                                  Equations
                                  Instances For
                                    theorem LO.FirstOrder.Semiformula.lMap_rel {n : } {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {k : } (r : L₁.Rel k) (v : Fin kLO.FirstOrder.Semiterm L₁ ξ n) :
                                    @[simp]
                                    theorem LO.FirstOrder.Semiformula.lMap_rel₀ {n : } {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (r : L₁.Rel 0) (v : Fin 0LO.FirstOrder.Semiterm L₁ ξ n) :
                                    @[simp]
                                    theorem LO.FirstOrder.Semiformula.lMap_rel₂ {n : } {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (r : L₁.Rel 2) (t₁ t₂ : LO.FirstOrder.Semiterm L₁ ξ n) :
                                    theorem LO.FirstOrder.Semiformula.lMap_nrel {n : } {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {k : } (r : L₁.Rel k) (v : Fin kLO.FirstOrder.Semiterm L₁ ξ n) :
                                    @[simp]
                                    theorem LO.FirstOrder.Semiformula.lMap_nrel₀ {n : } {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (r : L₁.Rel 0) (v : Fin 0LO.FirstOrder.Semiterm L₁ ξ n) :
                                    @[simp]
                                    theorem LO.FirstOrder.Semiformula.lMap_nrel₂ {n : } {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (r : L₁.Rel 2) (t₁ t₂ : LO.FirstOrder.Semiterm L₁ ξ n) :
                                    @[simp]
                                    @[simp]
                                    @[simp]
                                    theorem LO.FirstOrder.Semiformula.freeVariables_lMap {n : } {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_5} [DecidableEq ξ] (Φ : L₁.Hom L₂) (φ : LO.FirstOrder.Semiformula L₁ ξ n) :
                                    ((LO.FirstOrder.Semiformula.lMap Φ) φ).freeVariables = φ.freeVariables
                                    @[reducible, inline]
                                    Equations
                                    Instances For
                                      Equations
                                      • LO.FirstOrder.instCollectionSyntacticFormulaTheory = inferInstance
                                      Equations
                                      • LO.FirstOrder.instCollectionSentenceClosedTheory = inferInstance
                                      Equations