Documentation

Mathlib.ModelTheory.Encoding

Encodings and Cardinality of First-Order Syntax #

Main Definitions #

Main Results #

TODO #

def FirstOrder.Language.Term.listEncode {L : FirstOrder.Language} {α : Type u'} :
L.Term αList (α (i : ) × L.Functions i)

Encodes a term as a list of variables and function symbols.

Equations
Instances For
    def FirstOrder.Language.Term.listDecode {L : FirstOrder.Language} {α : Type u'} :
    List (α (i : ) × L.Functions i)List (Option (L.Term α))

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

    Equations
    Instances For
      theorem FirstOrder.Language.Term.listDecode_encode_list {L : FirstOrder.Language} {α : Type u'} (l : List (L.Term α)) :
      FirstOrder.Language.Term.listDecode (l.bind FirstOrder.Language.Term.listEncode) = List.map some l
      @[simp]
      theorem FirstOrder.Language.Term.encoding_decode {L : FirstOrder.Language} {α : Type u'} (l : List (α (i : ) × L.Functions i)) :
      FirstOrder.Language.Term.encoding.decode l = (FirstOrder.Language.Term.listDecode l).head?.join
      @[simp]
      theorem FirstOrder.Language.Term.encoding_Γ {L : FirstOrder.Language} {α : Type u'} :
      FirstOrder.Language.Term.encoding = (α (i : ) × L.Functions i)
      @[simp]
      theorem FirstOrder.Language.Term.encoding_encode {L : FirstOrder.Language} {α : Type u'} :
      ∀ (a : L.Term α), FirstOrder.Language.Term.encoding.encode a = a.listEncode

      An encoding of terms as lists.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem FirstOrder.Language.Term.listEncode_injective {L : FirstOrder.Language} {α : Type u'} :
        Function.Injective FirstOrder.Language.Term.listEncode
        theorem FirstOrder.Language.Term.card_le {L : FirstOrder.Language} {α : Type u'} :
        Cardinal.mk (L.Term α) max Cardinal.aleph0 (Cardinal.mk (α (i : ) × L.Functions i))
        theorem FirstOrder.Language.Term.card_sigma {L : FirstOrder.Language} {α : Type u'} :
        Cardinal.mk ((n : ) × L.Term (α Fin n)) = max Cardinal.aleph0 (Cardinal.mk (α (i : ) × L.Functions i))
        instance FirstOrder.Language.Term.instEncodableOfSigmaNatFunctions {L : FirstOrder.Language} {α : Type u'} [Encodable α] [Encodable ((i : ) × L.Functions i)] :
        Encodable (L.Term α)
        Equations
        • One or more equations did not get rendered due to their size.
        instance FirstOrder.Language.Term.instCountableOfSigmaNatFunctions {L : FirstOrder.Language} {α : Type u'} [h1 : Countable α] [h2 : Countable ((l : ) × L.Functions l)] :
        Countable (L.Term α)
        Equations
        • =
        Equations
        • =
        def FirstOrder.Language.BoundedFormula.listEncode {L : FirstOrder.Language} {α : Type u'} {n : } :
        L.BoundedFormula α nList ((k : ) × L.Term (α Fin k) (n : ) × L.Relations n )

        Encodes a bounded formula as a list of symbols.

        Equations
        Instances For
          def FirstOrder.Language.BoundedFormula.sigmaAll {L : FirstOrder.Language} {α : Type u'} :
          (n : ) × L.BoundedFormula α n(n : ) × L.BoundedFormula α n

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

          Equations
          Instances For
            def FirstOrder.Language.BoundedFormula.sigmaImp {L : FirstOrder.Language} {α : Type u'} :
            (n : ) × L.BoundedFormula α n(n : ) × L.BoundedFormula α n(n : ) × L.BoundedFormula α n

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

            Equations
            Instances For
              @[irreducible]
              def FirstOrder.Language.BoundedFormula.listDecode {L : FirstOrder.Language} {α : Type u'} (l : List ((k : ) × L.Term (α Fin k) (n : ) × L.Relations n )) :
              ((n : ) × L.BoundedFormula α n) × { l' : List ((k : ) × L.Term (α Fin k) (n : ) × L.Relations n ) // sizeOf l' max 1 (sizeOf l) }

              Decodes a list of symbols as a list of formulas.

              Equations
              Instances For
                @[simp]
                theorem FirstOrder.Language.BoundedFormula.listDecode_encode_list {L : FirstOrder.Language} {α : Type u'} (l : List ((n : ) × L.BoundedFormula α n)) :
                (FirstOrder.Language.BoundedFormula.listDecode (l.bind fun (φ : (n : ) × L.BoundedFormula α n) => φ.snd.listEncode)).1 = l.headI
                @[simp]
                theorem FirstOrder.Language.BoundedFormula.encoding_encode {L : FirstOrder.Language} {α : Type u'} (φ : (n : ) × L.BoundedFormula α n) :
                FirstOrder.Language.BoundedFormula.encoding.encode φ = φ.snd.listEncode
                @[simp]
                theorem FirstOrder.Language.BoundedFormula.encoding_decode {L : FirstOrder.Language} {α : Type u'} (l : List ((k : ) × L.Term (α Fin k) (n : ) × L.Relations n )) :
                FirstOrder.Language.BoundedFormula.encoding.decode l = some (FirstOrder.Language.BoundedFormula.listDecode l).1
                @[simp]
                theorem FirstOrder.Language.BoundedFormula.encoding_Γ {L : FirstOrder.Language} {α : Type u'} :
                FirstOrder.Language.BoundedFormula.encoding = ((k : ) × L.Term (α Fin k) (n : ) × L.Relations n )

                An encoding of bounded formulas as lists.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem FirstOrder.Language.BoundedFormula.listEncode_sigma_injective {L : FirstOrder.Language} {α : Type u'} :
                  Function.Injective fun (φ : (n : ) × L.BoundedFormula α n) => φ.snd.listEncode