mathlib3documentation

model_theory.encoding

Encodings and Cardinality of First-Order Syntax #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main Definitions #

• first_order.language.term.encoding encodes terms as lists.
• first_order.language.bounded_formula.encoding encodes bounded formulas as lists.

Main Results #

• first_order.language.term.card_le shows that the number of terms in L.term α is at most max ℵ₀ # (α ⊕ Σ i, L.functions i).
• first_order.language.bounded_formula.card_le shows that the number of bounded formulas in Σ n, L.bounded_formula α n is at most max ℵ₀ (cardinal.lift.{max u v} (#α) + cardinal.lift.{u'} L.card).

TODO #

• primcodable instances for terms and formulas, based on the encodings
• Computability facts about term and formula operations, to set up a computability approach to incompleteness

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

Equations

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

Equations
@[simp]
@[simp]
@[protected]

An encoding of terms as lists.

Equations
@[protected, instance]
Equations
@[protected, instance]
def first_order.language.term.countable {L : first_order.language} {α : Type u'} [h1 : countable α] [h2 : countable (Σ (l : ), L.functions l)] :
@[protected, instance]

Encodes a bounded formula as a list of symbols.

Equations

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

Equations
def first_order.language.bounded_formula.sigma_imp {L : first_order.language} {α : Type u'} :
(Σ (n : ), n) (Σ (n : ), n) (Σ (n : ), n)

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

Equations
@[simp]
def first_order.language.bounded_formula.list_decode {L : first_order.language} {α : Type u'} (l : list ((Σ (k : ), L.term fin k)) (Σ (n : ), L.relations n) )) :
(Σ (n : ), n) × {l' // l'.sizeof l.sizeof}

Decodes a list of symbols as a list of formulas.

Equations
@[protected]

An encoding of bounded formulas as lists.

Equations
@[simp]
theorem first_order.language.bounded_formula.encoding_decode {L : first_order.language} {α : Type u'} (l : list ((Σ (k : ), L.term fin k)) (Σ (n : ), L.relations n) )) :