mathlib documentation

model_theory.encoding

Encodings and Cardinality of First-Order Syntax #

Main Definitions #

Main Results #

TODO #

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

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]

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

Equations

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