# Encodings and Cardinality of First-Order Syntax #

## Main Definitions #

• FirstOrder.Language.Term.encoding encodes terms as lists.
• FirstOrder.Language.BoundedFormula.encoding encodes bounded formulas as lists.

## Main Results #

• FirstOrder.Language.Term.card_le shows that the number of terms in L.Term α is at most max ℵ₀ # (α ⊕ Σ i, L.Functions i).
• FirstOrder.Language.BoundedFormula.card_le shows that the number of bounded formulas in Σ n, L.BoundedFormula α 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
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
• .listEncode = []
• ().listEncode = Sum.inr l, f :: ().bind fun (i : Fin l) => (ts i).listEncode
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
• One or more equations did not get rendered due to their size.
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)) :
@[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 ((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 : ] [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
• = match x with | n.succ, φ => n, φ.all | x => default
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
• = match x✝, x with | m, φ, n, ψ => if h : m = n then m, φ.imp (.mp ψ) else default
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 () }

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 =
@[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