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

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

Equations

• FirstOrder.Language.Term.listEncode (FirstOrder.Language.var i) = [Sum.inl i]
• FirstOrder.Language.Term.listEncode (FirstOrder.Language.func f ts) = Sum.inr { fst := l, snd := f } :: List.bind (List.finRange l) fun i => FirstOrder.Language.Term.listEncode (ts i)

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

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.
• FirstOrder.Language.Term.listDecode [] = []
• FirstOrder.Language.Term.listDecode (Sum.inl a :: l) = some (FirstOrder.Language.var a) :: FirstOrder.Language.Term.listDecode l

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Term.encoding_decode {L : FirstOrder.Language} {α : Type u'} (l : List (α ⊕ (i : ℕ) × FirstOrder.Language.Functions L i)) : Computability.Encoding.decode FirstOrder.Language.Term.encoding l = Option.join (List.head? (FirstOrder.Language.Term.listDecode l))

@[simp]

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

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

An encoding of terms as lists.

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 (FirstOrder.Language.Term L α) ≤ max Cardinal.aleph0 (Cardinal.mk (α ⊕ (i : ℕ) × FirstOrder.Language.Functions L i))

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

instance FirstOrder.Language.Term.instEncodableTerm {L : FirstOrder.Language} {α : Type u'} [Encodable α] [Encodable ((i : ℕ) × FirstOrder.Language.Functions L i)] : Encodable (FirstOrder.Language.Term L α)

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

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

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

Encodes a bounded formula as a list of symbols.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormula.listEncode FirstOrder.Language.BoundedFormula.falsum = [Sum.inr (Sum.inr (x + 2))]
• FirstOrder.Language.BoundedFormula.listEncode (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = [Sum.inl { fst := x, snd := t₁ }, Sum.inl { fst := x, snd := t₂ }]
• FirstOrder.Language.BoundedFormula.listEncode (FirstOrder.Language.BoundedFormula.all φ) = Sum.inr (Sum.inr 1) :: FirstOrder.Language.BoundedFormula.listEncode φ

def FirstOrder.Language.BoundedFormula.sigmaAll {L : FirstOrder.Language} {α : Type u'} : (n : ℕ) × FirstOrder.Language.BoundedFormula L α n → (n : ℕ) × FirstOrder.Language.BoundedFormula L α n

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

def FirstOrder.Language.BoundedFormula.sigmaImp {L : FirstOrder.Language} {α : Type u'} : (n : ℕ) × FirstOrder.Language.BoundedFormula L α n → (n : ℕ) × FirstOrder.Language.BoundedFormula L α n → (n : ℕ) × FirstOrder.Language.BoundedFormula L α n

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

def FirstOrder.Language.BoundedFormula.listDecode {L : FirstOrder.Language} {α : Type u'} (l : List ((k : ℕ) × FirstOrder.Language.Term L (α ⊕ Fin k) ⊕ (n : ℕ) × FirstOrder.Language.Relations L n ⊕ ℕ)) : ((n : ℕ) × FirstOrder.Language.BoundedFormula L α n) × { l' // sizeOf l' ≤ max 1 (sizeOf l) }

Decodes a list of symbols as a list of formulas.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.BoundedFormula.encoding_decode {L : FirstOrder.Language} {α : Type u'} (l : List ((k : ℕ) × FirstOrder.Language.Term L (α ⊕ Fin k) ⊕ (n : ℕ) × FirstOrder.Language.Relations L n ⊕ ℕ)) : Computability.Encoding.decode FirstOrder.Language.BoundedFormula.encoding l = some (FirstOrder.Language.BoundedFormula.listDecode l).fst

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

An encoding of bounded formulas as lists.

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

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