mathlib documentation

model_theory.encoding

Encodings and Cardinality of First-Order Syntax #

Main Definitions #

Main Results #

TODO #

def first_order.language.term.list_encode {L : first_order.language} {α : Type u'} :
L.term αlist Σ (i : ), L.functions i)

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

Equations
@[protected]

An encoding of terms as lists.

Equations
@[protected, instance]
def first_order.language.term.encodable {L : first_order.language} {α : Type u'} [encodable α] [encodable (Σ (i : ), L.functions i)] :
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]
def first_order.language.term.small {L : first_order.language} {α : Type u'} [small α] :
small (L.term α)
def first_order.language.bounded_formula.list_encode {L : first_order.language} {α : Type u'} {n : } :
L.bounded_formula α nlist ((Σ (k : ), L.term fin k)) (Σ (n : ), L.relations n) )

Encodes a bounded formula as a list of symbols.

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

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 : ), L.bounded_formula α n)(Σ (n : ), L.bounded_formula α n)(Σ (n : ), L.bounded_formula α 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 : ), L.bounded_formula α n) × {l' // l'.sizeof linear_order.max 1 l.sizeof}

Decodes a list of symbols as a list of formulas.

Equations
@[protected]

An encoding of bounded formulas as lists.

Equations