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 : Language} {α : Type u'} : L.Term α → List (α ⊕ (i : ℕ) × L.Functions i)

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

def FirstOrder.Language.Term.listDecode {L : Language} {α : Type u'} : List (α ⊕ (i : ℕ) × L.Functions i) → List (L.Term α)

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

theorem FirstOrder.Language.Term.listDecode_encode_list {L : Language} {α : Type u'} (l : List (L.Term α)) : listDecode (List.flatMap listEncode l) = l

def FirstOrder.Language.Term.encoding {L : Language} {α : Type u'} : Computability.Encoding (L.Term α)

An encoding of terms as lists.

@[simp]

theorem FirstOrder.Language.Term.encoding_encode {L : Language} {α : Type u'} (a✝ : L.Term α) : Term.encoding.encode a✝ = a✝.listEncode

@[simp]

theorem FirstOrder.Language.Term.encoding_Γ {L : Language} {α : Type u'} : Term.encoding.Γ = (α ⊕ (i : ℕ) × L.Functions i)

@[simp]

theorem FirstOrder.Language.Term.encoding_decode {L : Language} {α : Type u'} (l : List (α ⊕ (i : ℕ) × L.Functions i)) : Term.encoding.decode l = (do let a ← (listDecode l).head? pure (some a)).join

theorem FirstOrder.Language.Term.listEncode_injective {L : Language} {α : Type u'} : Function.Injective listEncode

theorem FirstOrder.Language.Term.card_le {L : Language} {α : Type u'} : Cardinal.mk (L.Term α) ≤ max Cardinal.aleph0 (Cardinal.mk (α ⊕ (i : ℕ) × L.Functions i))

theorem FirstOrder.Language.Term.card_sigma {L : 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 : Language} {α : Type u'} [Encodable α] [Encodable ((i : ℕ) × L.Functions i)] : Encodable (L.Term α)

instance FirstOrder.Language.Term.instCountableOfSigmaNatFunctions {L : Language} {α : Type u'} [h1 : Countable α] [h2 : Countable ((l : ℕ) × L.Functions l)] : Countable (L.Term α)

instance FirstOrder.Language.Term.small {L : Language} {α : Type u'} [Small.{u, u'} α] : Small.{u, max u u'} (L.Term α)

def FirstOrder.Language.BoundedFormula.listEncode {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormula α n → List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)

Encodes a bounded formula as a list of symbols.

def FirstOrder.Language.BoundedFormula.sigmaAll {L : 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.

@[simp]

theorem FirstOrder.Language.BoundedFormula.sigmaAll_apply {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} : sigmaAll ⟨n + 1, φ⟩ = ⟨n, φ.all⟩

def FirstOrder.Language.BoundedFormula.sigmaImp {L : 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.

@[simp]

theorem FirstOrder.Language.BoundedFormula.sigmaImp_apply {L : Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormula α n} : sigmaImp ⟨n, φ⟩ ⟨n, ψ⟩ = ⟨n, φ.imp ψ⟩

Decodes a list of symbols as a list of formulas.

@[irreducible]

def FirstOrder.Language.BoundedFormula.listDecode {L : Language} {α : Type u'} : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → List ((n : ℕ) × L.BoundedFormula α n)

Decodes a list of symbols as a list of formulas.

@[simp]

theorem FirstOrder.Language.BoundedFormula.listDecode_encode_list {L : Language} {α : Type u'} (l : List ((n : ℕ) × L.BoundedFormula α n)) : listDecode (List.flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) => φ.snd.listEncode) l) = l

def FirstOrder.Language.BoundedFormula.encoding {L : Language} {α : Type u'} : Computability.Encoding ((n : ℕ) × L.BoundedFormula α n)

An encoding of bounded formulas as lists.

@[simp]

theorem FirstOrder.Language.BoundedFormula.encoding_decode {L : Language} {α : Type u'} (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) : BoundedFormula.encoding.decode l = (listDecode l)[0]?

@[simp]

theorem FirstOrder.Language.BoundedFormula.encoding_encode {L : Language} {α : Type u'} (φ : (n : ℕ) × L.BoundedFormula α n) : BoundedFormula.encoding.encode φ = φ.snd.listEncode

@[simp]

theorem FirstOrder.Language.BoundedFormula.encoding_Γ {L : Language} {α : Type u'} : BoundedFormula.encoding.Γ = ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)

theorem FirstOrder.Language.BoundedFormula.listEncode_sigma_injective {L : Language} {α : Type u'} : Function.Injective fun (φ : (n : ℕ) × L.BoundedFormula α n) => φ.snd.listEncode

theorem FirstOrder.Language.BoundedFormula.card_le {L : Language} {α : Type u'} : Cardinal.mk ((n : ℕ) × L.BoundedFormula α n) ≤ max Cardinal.aleph0 (Cardinal.lift.{max u v, u'} (Cardinal.mk α) + Cardinal.lift.{u', max u v} L.card)