Documentation

Mathlib.ModelTheory.Syntax

Basics on First-Order Syntax #

This file defines first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.

Main Definitions #

Implementation Notes #

References #

For the Flypitch project:

inductive FirstOrder.Language.Term (L : FirstOrder.Language) (α : Type u') :
Type (max u u')

A term on α is either a variable indexed by an element of α or a function symbol applied to simpler terms.

Instances For
    instance FirstOrder.Language.Term.instDecidableEq {L : FirstOrder.Language} {α : Type u'} [DecidableEq α] [(n : ) → DecidableEq (L.Functions n)] :
    DecidableEq (L.Term α)
    Equations

    The Finset of variables used in a given term.

    Equations
    Instances For
      def FirstOrder.Language.Term.varFinsetLeft {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [DecidableEq α] :
      L.Term (α β)Finset α

      The Finset of variables from the left side of a sum used in a given term.

      Equations
      Instances For
        @[simp]
        theorem FirstOrder.Language.Term.relabel_relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (f : αβ) (g : βγ) (t : L.Term α) :
        @[simp]
        theorem FirstOrder.Language.Term.relabelEquiv_symm_apply {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α β) :
        ∀ (a : L.Term β), (FirstOrder.Language.Term.relabelEquiv g).symm a = FirstOrder.Language.Term.relabel (⇑g.symm) a
        def FirstOrder.Language.Term.relabelEquiv {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α β) :
        L.Term α L.Term β

        Relabels a term's variables along a bijection.

        Equations
        Instances For
          def FirstOrder.Language.Term.restrictVar {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [DecidableEq α] (t : L.Term α) (_f : { x : α // x t.varFinset }β) :
          L.Term β

          Restricts a term to use only a set of the given variables.

          Equations
          Instances For
            def FirstOrder.Language.Term.restrictVarLeft {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [DecidableEq α] {γ : Type u_2} (t : L.Term (α γ)) (_f : { x : α // x t.varFinsetLeft }β) :
            L.Term (β γ)

            Restricts a term to use only a set of the given variables on the left side of a sum.

            Equations
            Instances For
              def FirstOrder.Language.Constants.term {L : FirstOrder.Language} {α : Type u'} (c : L.Constants) :
              L.Term α

              The representation of a constant symbol as a term.

              Equations
              Instances For
                def FirstOrder.Language.Functions.apply₁ {L : FirstOrder.Language} {α : Type u'} (f : L.Functions 1) (t : L.Term α) :
                L.Term α

                Applies a unary function to a term.

                Equations
                Instances For
                  def FirstOrder.Language.Functions.apply₂ {L : FirstOrder.Language} {α : Type u'} (f : L.Functions 2) (t₁ : L.Term α) (t₂ : L.Term α) :
                  L.Term α

                  Applies a binary function to two terms.

                  Equations
                  Instances For
                    def FirstOrder.Language.Term.constantsToVars {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} :
                    (L.withConstants γ).Term αL.Term (γ α)

                    Sends a term with constants to a term with extra variables.

                    Equations
                    Instances For
                      def FirstOrder.Language.Term.varsToConstants {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} :
                      L.Term (γ α)(L.withConstants γ).Term α

                      Sends a term with extra variables to a term with constants.

                      Equations
                      Instances For
                        @[simp]
                        theorem FirstOrder.Language.Term.constantsVarsEquiv_symm_apply {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} :
                        ∀ (a : L.Term (γ α)), FirstOrder.Language.Term.constantsVarsEquiv.symm a = a.varsToConstants
                        @[simp]
                        theorem FirstOrder.Language.Term.constantsVarsEquiv_apply {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} :
                        ∀ (a : (L.withConstants γ).Term α), FirstOrder.Language.Term.constantsVarsEquiv a = a.constantsToVars
                        def FirstOrder.Language.Term.constantsVarsEquiv {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} :
                        (L.withConstants γ).Term α L.Term (γ α)

                        A bijection between terms with constants and terms with extra variables.

                        Equations
                        • FirstOrder.Language.Term.constantsVarsEquiv = { toFun := FirstOrder.Language.Term.constantsToVars, invFun := FirstOrder.Language.Term.varsToConstants, left_inv := , right_inv := }
                        Instances For
                          def FirstOrder.Language.Term.constantsVarsEquivLeft {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} :
                          (L.withConstants γ).Term (α β) L.Term ((γ α) β)

                          A bijection between terms with constants and terms with extra variables.

                          Equations
                          Instances For
                            @[simp]
                            theorem FirstOrder.Language.Term.constantsVarsEquivLeft_apply {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (t : (L.withConstants γ).Term (α β)) :
                            FirstOrder.Language.Term.constantsVarsEquivLeft t = FirstOrder.Language.Term.relabel (⇑(Equiv.sumAssoc γ α β).symm) t.constantsToVars
                            @[simp]
                            theorem FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (t : L.Term ((γ α) β)) :
                            FirstOrder.Language.Term.constantsVarsEquivLeft.symm t = (FirstOrder.Language.Term.relabel (⇑(Equiv.sumAssoc γ α β)) t).varsToConstants
                            Equations
                            Equations
                            • FirstOrder.Language.Term.inhabitedOfConstant = { default := default.term }
                            def FirstOrder.Language.Term.liftAt {L : FirstOrder.Language} {α : Type u'} {n : } (n' : ) (m : ) :
                            L.Term (α Fin n)L.Term (α Fin (n + n'))

                            Raises all of the Fin-indexed variables of a term greater than or equal to m by n'.

                            Equations
                            Instances For
                              def FirstOrder.Language.Term.subst {L : FirstOrder.Language} {α : Type u'} {β : Type v'} :
                              L.Term α(αL.Term β)L.Term β

                              Substitutes the variables in a given term with terms.

                              Equations
                              Instances For
                                def FirstOrder.Language.LHom.onTerm {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L →ᴸ L') :
                                L.Term αL'.Term α

                                Maps a term's symbols along a language map.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem FirstOrder.Language.LHom.comp_onTerm {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {L'' : FirstOrder.Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
                                  (φ.comp ψ).onTerm = φ.onTerm ψ.onTerm
                                  @[simp]
                                  theorem FirstOrder.Language.Lequiv.onTerm_symm_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') :
                                  ∀ (a : L'.Term α), (FirstOrder.Language.Lequiv.onTerm φ).symm a = φ.invLHom.onTerm a
                                  @[simp]
                                  theorem FirstOrder.Language.Lequiv.onTerm_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') :
                                  ∀ (a : L.Term α), (FirstOrder.Language.Lequiv.onTerm φ) a = φ.toLHom.onTerm a
                                  def FirstOrder.Language.Lequiv.onTerm {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') :
                                  L.Term α L'.Term α

                                  Maps a term's symbols along a language equivalence.

                                  Equations
                                  Instances For
                                    inductive FirstOrder.Language.BoundedFormula (L : FirstOrder.Language) (α : Type u') :
                                    Type (max u v u')

                                    BoundedFormula α n is the type of formulas with free variables indexed by α and up to n additional free variables.

                                    Instances For
                                      @[reducible, inline]
                                      abbrev FirstOrder.Language.Formula (L : FirstOrder.Language) (α : Type u') :
                                      Type (max u v u')

                                      Formula α is the type of formulas with all free variables indexed by α.

                                      Equations
                                      • L.Formula α = L.BoundedFormula α 0
                                      Instances For
                                        @[reducible, inline]

                                        A sentence is a formula with no free variables.

                                        Equations
                                        Instances For
                                          @[reducible, inline]

                                          A theory is a set of sentences.

                                          Equations
                                          • L.Theory = Set L.Sentence
                                          Instances For
                                            def FirstOrder.Language.Relations.boundedFormula {L : FirstOrder.Language} {α : Type u'} {n : } {l : } (R : L.Relations n) (ts : Fin nL.Term (α Fin l)) :
                                            L.BoundedFormula α l

                                            Applies a relation to terms as a bounded formula.

                                            Equations
                                            Instances For
                                              def FirstOrder.Language.Relations.boundedFormula₁ {L : FirstOrder.Language} {α : Type u'} {n : } (r : L.Relations 1) (t : L.Term (α Fin n)) :
                                              L.BoundedFormula α n

                                              Applies a unary relation to a term as a bounded formula.

                                              Equations
                                              • r.boundedFormula₁ t = r.boundedFormula ![t]
                                              Instances For
                                                def FirstOrder.Language.Relations.boundedFormula₂ {L : FirstOrder.Language} {α : Type u'} {n : } (r : L.Relations 2) (t₁ : L.Term (α Fin n)) (t₂ : L.Term (α Fin n)) :
                                                L.BoundedFormula α n

                                                Applies a binary relation to two terms as a bounded formula.

                                                Equations
                                                • r.boundedFormula₂ t₁ t₂ = r.boundedFormula ![t₁, t₂]
                                                Instances For
                                                  def FirstOrder.Language.Term.bdEqual {L : FirstOrder.Language} {α : Type u'} {n : } (t₁ : L.Term (α Fin n)) (t₂ : L.Term (α Fin n)) :
                                                  L.BoundedFormula α n

                                                  The equality of two terms as a bounded formula.

                                                  Equations
                                                  Instances For
                                                    def FirstOrder.Language.Relations.formula {L : FirstOrder.Language} {α : Type u'} {n : } (R : L.Relations n) (ts : Fin nL.Term α) :
                                                    L.Formula α

                                                    Applies a relation to terms as a bounded formula.

                                                    Equations
                                                    Instances For
                                                      def FirstOrder.Language.Relations.formula₁ {L : FirstOrder.Language} {α : Type u'} (r : L.Relations 1) (t : L.Term α) :
                                                      L.Formula α

                                                      Applies a unary relation to a term as a formula.

                                                      Equations
                                                      • r.formula₁ t = r.formula ![t]
                                                      Instances For
                                                        def FirstOrder.Language.Relations.formula₂ {L : FirstOrder.Language} {α : Type u'} (r : L.Relations 2) (t₁ : L.Term α) (t₂ : L.Term α) :
                                                        L.Formula α

                                                        Applies a binary relation to two terms as a formula.

                                                        Equations
                                                        • r.formula₂ t₁ t₂ = r.formula ![t₁, t₂]
                                                        Instances For
                                                          def FirstOrder.Language.Term.equal {L : FirstOrder.Language} {α : Type u'} (t₁ : L.Term α) (t₂ : L.Term α) :
                                                          L.Formula α

                                                          The equality of two terms as a first-order formula.

                                                          Equations
                                                          Instances For
                                                            instance FirstOrder.Language.BoundedFormula.instInhabited {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                            Inhabited (L.BoundedFormula α n)
                                                            Equations
                                                            • FirstOrder.Language.BoundedFormula.instInhabited = { default := FirstOrder.Language.BoundedFormula.falsum }
                                                            instance FirstOrder.Language.BoundedFormula.instBot {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                            Bot (L.BoundedFormula α n)
                                                            Equations
                                                            • FirstOrder.Language.BoundedFormula.instBot = { bot := FirstOrder.Language.BoundedFormula.falsum }
                                                            @[match_pattern]
                                                            def FirstOrder.Language.BoundedFormula.not {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α n) :
                                                            L.BoundedFormula α n

                                                            The negation of a bounded formula is also a bounded formula.

                                                            Equations
                                                            Instances For
                                                              @[match_pattern]
                                                              def FirstOrder.Language.BoundedFormula.ex {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α (n + 1)) :
                                                              L.BoundedFormula α n

                                                              Puts an quantifier on a bounded formula.

                                                              Equations
                                                              • φ.ex = φ.not.all.not
                                                              Instances For
                                                                instance FirstOrder.Language.BoundedFormula.instTop {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                                Top (L.BoundedFormula α n)
                                                                Equations
                                                                • FirstOrder.Language.BoundedFormula.instTop = { top := .not }
                                                                instance FirstOrder.Language.BoundedFormula.instInf {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                                Inf (L.BoundedFormula α n)
                                                                Equations
                                                                • FirstOrder.Language.BoundedFormula.instInf = { inf := fun (f g : L.BoundedFormula α n) => (f.imp g.not).not }
                                                                instance FirstOrder.Language.BoundedFormula.instSup {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                                Sup (L.BoundedFormula α n)
                                                                Equations
                                                                • FirstOrder.Language.BoundedFormula.instSup = { sup := fun (f g : L.BoundedFormula α n) => f.not.imp g }
                                                                def FirstOrder.Language.BoundedFormula.iff {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) :
                                                                L.BoundedFormula α n

                                                                The biimplication between two bounded formulas.

                                                                Equations
                                                                • φ.iff ψ = φ.imp ψ ψ.imp φ
                                                                Instances For
                                                                  def FirstOrder.Language.BoundedFormula.freeVarFinset {L : FirstOrder.Language} {α : Type u'} [DecidableEq α] {n : } :
                                                                  L.BoundedFormula α nFinset α

                                                                  The Finset of variables used in a given formula.

                                                                  Equations
                                                                  Instances For
                                                                    def FirstOrder.Language.BoundedFormula.castLE {L : FirstOrder.Language} {α : Type u'} {m : } {n : } (_h : m n) :
                                                                    L.BoundedFormula α mL.BoundedFormula α n

                                                                    Casts L.BoundedFormula α m as L.BoundedFormula α n, where m ≤ n.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem FirstOrder.Language.BoundedFormula.castLE_rfl {L : FirstOrder.Language} {α : Type u'} {n : } (h : n n) (φ : L.BoundedFormula α n) :
                                                                      def FirstOrder.Language.BoundedFormula.restrictFreeVar {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [DecidableEq α] {n : } (φ : L.BoundedFormula α n) (_f : { x : α // x φ.freeVarFinset }β) :
                                                                      L.BoundedFormula β n

                                                                      Restricts a bounded formula to only use a particular set of free variables.

                                                                      Equations
                                                                      Instances For
                                                                        def FirstOrder.Language.BoundedFormula.alls {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                                        L.BoundedFormula α nL.Formula α

                                                                        Places universal quantifiers on all extra variables of a bounded formula.

                                                                        Equations
                                                                        • φ.alls = φ
                                                                        • φ.alls = φ.all.alls
                                                                        Instances For
                                                                          def FirstOrder.Language.BoundedFormula.exs {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                                          L.BoundedFormula α nL.Formula α

                                                                          Places existential quantifiers on all extra variables of a bounded formula.

                                                                          Equations
                                                                          • φ.exs = φ
                                                                          • φ.exs = φ.ex.exs
                                                                          Instances For
                                                                            def FirstOrder.Language.BoundedFormula.mapTermRel {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : } (ft : (n : ) → L.Term (α Fin n)L'.Term (β Fin (g n))) (fr : (n : ) → L.Relations nL'.Relations n) (h : (n : ) → L'.BoundedFormula β (g (n + 1))L'.BoundedFormula β (g n + 1)) {n : } :
                                                                            L.BoundedFormula α nL'.BoundedFormula β (g n)

                                                                            Maps bounded formulas along a map of terms and a map of relations.

                                                                            Equations
                                                                            Instances For
                                                                              def FirstOrder.Language.BoundedFormula.liftAt {L : FirstOrder.Language} {α : Type u'} {n : } (n' : ) (_m : ) :
                                                                              L.BoundedFormula α nL.BoundedFormula α (n + n')

                                                                              Raises all of the Fin-indexed variables of a formula greater than or equal to m by n'.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem FirstOrder.Language.BoundedFormula.mapTermRel_mapTermRel {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} {L'' : FirstOrder.Language} (ft : (n : ) → L.Term (α Fin n)L'.Term (β Fin n)) (fr : (n : ) → L.Relations nL'.Relations n) (ft' : (n : ) → L'.Term (β Fin n)L''.Term (γ Fin n)) (fr' : (n : ) → L'.Relations nL''.Relations n) {n : } (φ : L.BoundedFormula α n) :
                                                                                FirstOrder.Language.BoundedFormula.mapTermRel ft' fr' (fun (x : ) => id) (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun (x : ) => id) φ) = FirstOrder.Language.BoundedFormula.mapTermRel (fun (x : ) => ft' x ft x) (fun (x : ) => fr' x fr x) (fun (x : ) => id) φ
                                                                                @[simp]
                                                                                theorem FirstOrder.Language.BoundedFormula.mapTermRel_id_id_id {L : FirstOrder.Language} {α : Type u'} {n : } (φ : L.BoundedFormula α n) :
                                                                                FirstOrder.Language.BoundedFormula.mapTermRel (fun (x : ) => id) (fun (x : ) => id) (fun (x : ) => id) φ = φ
                                                                                @[simp]
                                                                                theorem FirstOrder.Language.BoundedFormula.mapTermRelEquiv_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} (ft : (n : ) → L.Term (α Fin n) L'.Term (β Fin n)) (fr : (n : ) → L.Relations n L'.Relations n) {n : } :
                                                                                ∀ (a : L.BoundedFormula α n), (FirstOrder.Language.BoundedFormula.mapTermRelEquiv ft fr) a = FirstOrder.Language.BoundedFormula.mapTermRel (fun (n : ) => (ft n)) (fun (n : ) => (fr n)) (fun (x : ) => id) a
                                                                                @[simp]
                                                                                theorem FirstOrder.Language.BoundedFormula.mapTermRelEquiv_symm_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} (ft : (n : ) → L.Term (α Fin n) L'.Term (β Fin n)) (fr : (n : ) → L.Relations n L'.Relations n) {n : } :
                                                                                ∀ (a : L'.BoundedFormula β n), (FirstOrder.Language.BoundedFormula.mapTermRelEquiv ft fr).symm a = FirstOrder.Language.BoundedFormula.mapTermRel (fun (n : ) => (ft n).symm) (fun (n : ) => (fr n).symm) (fun (x : ) => id) a
                                                                                def FirstOrder.Language.BoundedFormula.mapTermRelEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} (ft : (n : ) → L.Term (α Fin n) L'.Term (β Fin n)) (fr : (n : ) → L.Relations n L'.Relations n) {n : } :
                                                                                L.BoundedFormula α n L'.BoundedFormula β n

                                                                                An equivalence of bounded formulas given by an equivalence of terms and an equivalence of relations.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  def FirstOrder.Language.BoundedFormula.relabelAux {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) (k : ) :
                                                                                  α Fin kβ Fin (n + k)

                                                                                  A function to help relabel the variables in bounded formulas.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem FirstOrder.Language.BoundedFormula.sum_elim_comp_relabelAux {M : Type w} {α : Type u'} {β : Type v'} {n : } {m : } {g : αβ Fin n} {v : βM} {xs : Fin (n + m)M} :
                                                                                    def FirstOrder.Language.BoundedFormula.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α k) :
                                                                                    L.BoundedFormula β (n + k)

                                                                                    Relabels a bounded formula's variables along a particular function.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      def FirstOrder.Language.BoundedFormula.relabelEquiv {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α β) {k : } :
                                                                                      L.BoundedFormula α k L.BoundedFormula β k

                                                                                      Relabels a bounded formula's free variables along a bijection.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem FirstOrder.Language.BoundedFormula.relabel_falsum {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } :
                                                                                        FirstOrder.Language.BoundedFormula.relabel g FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
                                                                                        @[simp]
                                                                                        theorem FirstOrder.Language.BoundedFormula.relabel_imp {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α k) (ψ : L.BoundedFormula α k) :
                                                                                        @[simp]
                                                                                        theorem FirstOrder.Language.BoundedFormula.relabel_not {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α k) :
                                                                                        @[simp]
                                                                                        theorem FirstOrder.Language.BoundedFormula.relabel_all {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α (k + 1)) :
                                                                                        @[simp]
                                                                                        theorem FirstOrder.Language.BoundedFormula.relabel_ex {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α (k + 1)) :
                                                                                        def FirstOrder.Language.BoundedFormula.subst {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (φ : L.BoundedFormula α n) (f : αL.Term β) :
                                                                                        L.BoundedFormula β n

                                                                                        Substitutes the variables in a given formula with terms.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          def FirstOrder.Language.BoundedFormula.constantsVarsEquiv {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} {n : } :
                                                                                          (L.withConstants γ).BoundedFormula α n L.BoundedFormula (γ α) n

                                                                                          A bijection sending formulas with constants to formulas with extra variables.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            def FirstOrder.Language.BoundedFormula.toFormula {L : FirstOrder.Language} {α : Type u'} {n : } :
                                                                                            L.BoundedFormula α nL.Formula (α Fin n)

                                                                                            Turns the extra variables of a bounded formula into free variables.

                                                                                            Equations
                                                                                            Instances For
                                                                                              noncomputable def FirstOrder.Language.BoundedFormula.iSup {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (s : Finset β) (f : βL.BoundedFormula α n) :
                                                                                              L.BoundedFormula α n

                                                                                              take the disjunction of a finite set of formulas

                                                                                              Equations
                                                                                              Instances For
                                                                                                noncomputable def FirstOrder.Language.BoundedFormula.iInf {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : } (s : Finset β) (f : βL.BoundedFormula α n) :
                                                                                                L.BoundedFormula α n

                                                                                                take the conjunction of a finite set of formulas

                                                                                                Equations
                                                                                                Instances For
                                                                                                  def FirstOrder.Language.LHom.onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') {k : } :
                                                                                                  L.BoundedFormula α kL'.BoundedFormula α k

                                                                                                  Maps a bounded formula's symbols along a language map.

                                                                                                  Equations
                                                                                                  • g.onBoundedFormula FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
                                                                                                  • g.onBoundedFormula (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = (g.onTerm t₁).bdEqual (g.onTerm t₂)
                                                                                                  • g.onBoundedFormula (FirstOrder.Language.BoundedFormula.rel _R ts) = (g.onRelation _R).boundedFormula (g.onTerm ts)
                                                                                                  • g.onBoundedFormula (f₁.imp f₂) = (g.onBoundedFormula f₁).imp (g.onBoundedFormula f₂)
                                                                                                  • g.onBoundedFormula f.all = (g.onBoundedFormula f).all
                                                                                                  Instances For
                                                                                                    @[simp]
                                                                                                    theorem FirstOrder.Language.LHom.comp_onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : } {L'' : FirstOrder.Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
                                                                                                    (φ.comp ψ).onBoundedFormula = φ.onBoundedFormula ψ.onBoundedFormula
                                                                                                    def FirstOrder.Language.LHom.onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') :
                                                                                                    L.Formula αL'.Formula α

                                                                                                    Maps a formula's symbols along a language map.

                                                                                                    Equations
                                                                                                    • g.onFormula = g.onBoundedFormula
                                                                                                    Instances For
                                                                                                      def FirstOrder.Language.LHom.onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} (g : L →ᴸ L') :
                                                                                                      L.SentenceL'.Sentence

                                                                                                      Maps a sentence's symbols along a language map.

                                                                                                      Equations
                                                                                                      • g.onSentence = g.onFormula
                                                                                                      Instances For
                                                                                                        def FirstOrder.Language.LHom.onTheory {L : FirstOrder.Language} {L' : FirstOrder.Language} (g : L →ᴸ L') (T : L.Theory) :
                                                                                                        L'.Theory

                                                                                                        Maps a theory's symbols along a language map.

                                                                                                        Equations
                                                                                                        • g.onTheory T = g.onSentence '' T
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem FirstOrder.Language.LHom.mem_onTheory {L : FirstOrder.Language} {L' : FirstOrder.Language} {g : L →ᴸ L'} {T : L.Theory} {φ : L'.Sentence} :
                                                                                                          φ g.onTheory T φ₀T, g.onSentence φ₀ = φ
                                                                                                          @[simp]
                                                                                                          theorem FirstOrder.Language.LEquiv.onBoundedFormula_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : } (φ : L ≃ᴸ L') :
                                                                                                          ∀ (a : L.BoundedFormula α n), φ.onBoundedFormula a = φ.toLHom.onBoundedFormula a
                                                                                                          @[simp]
                                                                                                          theorem FirstOrder.Language.LEquiv.onBoundedFormula_symm_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : } (φ : L ≃ᴸ L') :
                                                                                                          ∀ (a : L'.BoundedFormula α n), φ.onBoundedFormula.symm a = φ.invLHom.onBoundedFormula a
                                                                                                          def FirstOrder.Language.LEquiv.onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : } (φ : L ≃ᴸ L') :
                                                                                                          L.BoundedFormula α n L'.BoundedFormula α n

                                                                                                          Maps a bounded formula's symbols along a language equivalence.

                                                                                                          Equations
                                                                                                          • φ.onBoundedFormula = { toFun := φ.toLHom.onBoundedFormula, invFun := φ.invLHom.onBoundedFormula, left_inv := , right_inv := }
                                                                                                          Instances For
                                                                                                            theorem FirstOrder.Language.LEquiv.onBoundedFormula_symm {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : } (φ : L ≃ᴸ L') :
                                                                                                            φ.onBoundedFormula.symm = φ.symm.onBoundedFormula
                                                                                                            def FirstOrder.Language.LEquiv.onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') :
                                                                                                            L.Formula α L'.Formula α

                                                                                                            Maps a formula's symbols along a language equivalence.

                                                                                                            Equations
                                                                                                            • φ.onFormula = φ.onBoundedFormula
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem FirstOrder.Language.LEquiv.onFormula_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') :
                                                                                                              φ.onFormula = φ.toLHom.onFormula
                                                                                                              @[simp]
                                                                                                              theorem FirstOrder.Language.LEquiv.onFormula_symm {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') :
                                                                                                              φ.onFormula.symm = φ.symm.onFormula
                                                                                                              @[simp]
                                                                                                              theorem FirstOrder.Language.LEquiv.onSentence_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} (φ : L ≃ᴸ L') :
                                                                                                              ∀ (a : L.BoundedFormula Empty 0), φ.onSentence a = φ.toLHom.onBoundedFormula a
                                                                                                              @[simp]
                                                                                                              theorem FirstOrder.Language.LEquiv.onSentence_symm_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} (φ : L ≃ᴸ L') :
                                                                                                              ∀ (a : L'.BoundedFormula Empty 0), φ.onSentence.symm a = φ.invLHom.onBoundedFormula a
                                                                                                              def FirstOrder.Language.LEquiv.onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} (φ : L ≃ᴸ L') :
                                                                                                              L.Sentence L'.Sentence

                                                                                                              Maps a sentence's symbols along a language equivalence.

                                                                                                              Equations
                                                                                                              • φ.onSentence = φ.onFormula
                                                                                                              Instances For
                                                                                                                def FirstOrder.Language.Formula.relabel {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : αβ) :
                                                                                                                L.Formula αL.Formula β

                                                                                                                Relabels a formula's variables along a particular function.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  def FirstOrder.Language.Formula.graph {L : FirstOrder.Language} {n : } (f : L.Functions n) :
                                                                                                                  L.Formula (Fin (n + 1))

                                                                                                                  The graph of a function as a first-order formula.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[reducible, inline]
                                                                                                                    abbrev FirstOrder.Language.Formula.not {L : FirstOrder.Language} {α : Type u'} (φ : L.Formula α) :
                                                                                                                    L.Formula α

                                                                                                                    The negation of a formula.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[reducible, inline]
                                                                                                                      abbrev FirstOrder.Language.Formula.imp {L : FirstOrder.Language} {α : Type u'} :
                                                                                                                      L.Formula αL.Formula αL.Formula α

                                                                                                                      The implication between formulas, as a formula.

                                                                                                                      Equations
                                                                                                                      • FirstOrder.Language.Formula.imp = FirstOrder.Language.BoundedFormula.imp
                                                                                                                      Instances For
                                                                                                                        noncomputable def FirstOrder.Language.Formula.iAlls {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} [Finite γ] (f : αβ γ) (φ : L.Formula α) :
                                                                                                                        L.Formula β

                                                                                                                        Given a map f : α → β ⊕ γ, iAlls f φ transforms a L.Formula α into a L.Formula β by renaming variables with the map f and then universally quantifying over all variables Sum.inr _.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          noncomputable def FirstOrder.Language.Formula.iExs {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} [Finite γ] (f : αβ γ) (φ : L.Formula α) :
                                                                                                                          L.Formula β

                                                                                                                          Given a map f : α → β ⊕ γ, iExs f φ transforms a L.Formula α into a L.Formula β by renaming variables with the map f and then universally quantifying over all variables Sum.inr _.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[reducible, inline]
                                                                                                                            abbrev FirstOrder.Language.Formula.iff {L : FirstOrder.Language} {α : Type u'} (φ : L.Formula α) (ψ : L.Formula α) :
                                                                                                                            L.Formula α

                                                                                                                            The biimplication between formulas, as a formula.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              def FirstOrder.Language.Formula.equivSentence {L : FirstOrder.Language} {α : Type u'} :
                                                                                                                              L.Formula α (L.withConstants α).Sentence

                                                                                                                              A bijection sending formulas to sentences with constants.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                theorem FirstOrder.Language.Formula.equivSentence_not {L : FirstOrder.Language} {α : Type u'} (φ : L.Formula α) :
                                                                                                                                FirstOrder.Language.Formula.equivSentence φ.not = FirstOrder.Language.Formula.not (FirstOrder.Language.Formula.equivSentence φ)
                                                                                                                                theorem FirstOrder.Language.Formula.equivSentence_inf {L : FirstOrder.Language} {α : Type u'} (φ : L.Formula α) (ψ : L.Formula α) :
                                                                                                                                FirstOrder.Language.Formula.equivSentence (φ ψ) = FirstOrder.Language.Formula.equivSentence φ FirstOrder.Language.Formula.equivSentence ψ
                                                                                                                                def FirstOrder.Language.Relations.reflexive {L : FirstOrder.Language} (r : L.Relations 2) :
                                                                                                                                L.Sentence

                                                                                                                                The sentence indicating that a basic relation symbol is reflexive.

                                                                                                                                Equations
                                                                                                                                • r.reflexive = (r.boundedFormula₂ ((FirstOrder.Language.var Sum.inr) 0) ((FirstOrder.Language.var Sum.inr) 0)).all
                                                                                                                                Instances For
                                                                                                                                  def FirstOrder.Language.Relations.irreflexive {L : FirstOrder.Language} (r : L.Relations 2) :
                                                                                                                                  L.Sentence

                                                                                                                                  The sentence indicating that a basic relation symbol is irreflexive.

                                                                                                                                  Equations
                                                                                                                                  • r.irreflexive = (r.boundedFormula₂ ((FirstOrder.Language.var Sum.inr) 0) ((FirstOrder.Language.var Sum.inr) 0)).not.all
                                                                                                                                  Instances For
                                                                                                                                    def FirstOrder.Language.Relations.symmetric {L : FirstOrder.Language} (r : L.Relations 2) :
                                                                                                                                    L.Sentence

                                                                                                                                    The sentence indicating that a basic relation symbol is symmetric.

                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      def FirstOrder.Language.Relations.antisymmetric {L : FirstOrder.Language} (r : L.Relations 2) :
                                                                                                                                      L.Sentence

                                                                                                                                      The sentence indicating that a basic relation symbol is antisymmetric.

                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        def FirstOrder.Language.Relations.transitive {L : FirstOrder.Language} (r : L.Relations 2) :
                                                                                                                                        L.Sentence

                                                                                                                                        The sentence indicating that a basic relation symbol is transitive.

                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For
                                                                                                                                          def FirstOrder.Language.Relations.total {L : FirstOrder.Language} (r : L.Relations 2) :
                                                                                                                                          L.Sentence

                                                                                                                                          The sentence indicating that a basic relation symbol is total.

                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For

                                                                                                                                            A sentence indicating that a structure has n distinct elements.

                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For

                                                                                                                                              A theory indicating that a structure is infinite.

                                                                                                                                              Equations
                                                                                                                                              Instances For

                                                                                                                                                A theory that indicates a structure is nonempty.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  def FirstOrder.Language.distinctConstantsTheory (L : FirstOrder.Language) {α : Type u'} (s : Set α) :
                                                                                                                                                  (L.withConstants α).Theory

                                                                                                                                                  A theory indicating that each of a set of constants is distinct.

                                                                                                                                                  Equations
                                                                                                                                                  • L.distinctConstantsTheory s = (fun (ab : α × α) => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s (Set.diagonal α))
                                                                                                                                                  Instances For
                                                                                                                                                    theorem FirstOrder.Language.distinctConstantsTheory_mono {L : FirstOrder.Language} {α : Type u'} {s : Set α} {t : Set α} (h : s t) :
                                                                                                                                                    L.distinctConstantsTheory s L.distinctConstantsTheory t
                                                                                                                                                    theorem FirstOrder.Language.directed_distinctConstantsTheory {L : FirstOrder.Language} {α : Type u'} :
                                                                                                                                                    Directed (fun (x1 x2 : (L.withConstants α).Theory) => x1 x2) L.distinctConstantsTheory
                                                                                                                                                    theorem FirstOrder.Language.distinctConstantsTheory_eq_iUnion {L : FirstOrder.Language} {α : Type u'} (s : Set α) :
                                                                                                                                                    L.distinctConstantsTheory s = ⋃ (t : Finset s), L.distinctConstantsTheory (Finset.map (Function.Embedding.subtype fun (x : α) => x s) t)