Documentation

Mathlib.ModelTheory.Encoding

Encodings and Cardinality of First-Order Syntax #

Main Definitions #

Main Results #

TODO #

Decodes a list of variables and function symbols as a list of terms.

Equations
Instances For
    @[simp]
    theorem FirstOrder.Language.Term.encoding_Γ {L : FirstOrder.Language} {α : Type u'} :
    FirstOrder.Language.Term.encoding = (α (i : ) × FirstOrder.Language.Functions L i)

    An encoding of terms as lists.

    Instances For
      theorem FirstOrder.Language.Term.listEncode_injective {L : FirstOrder.Language} {α : Type u'} :
      Function.Injective FirstOrder.Language.Term.listEncode

      Encodes a bounded formula as a list of symbols.

      Equations
      Instances For

        Applies the forall quantifier to an element of (Σ n, L.BoundedFormula α n), or returns default if not possible.

        Instances For

          Applies imp to two elements of (Σ n, L.BoundedFormula α n), or returns default if not possible.

          Instances For

            Decodes a list of symbols as a list of formulas.

            Instances For
              @[simp]
              theorem FirstOrder.Language.BoundedFormula.encoding_Γ {L : FirstOrder.Language} {α : Type u'} :
              FirstOrder.Language.BoundedFormula.encoding = ((k : ) × FirstOrder.Language.Term L (α Fin k) (n : ) × FirstOrder.Language.Relations L n )

              An encoding of bounded formulas as lists.

              Instances For