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

• (FirstOrder.Language.var i).listEncode = [Sum.inl i]
• (FirstOrder.Language.func f ts).listEncode = Sum.inr ⟨l, f⟩ :: (List.finRange l).bind fun (i : Fin l) => (ts i).listEncode

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.
• 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 (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)) : FirstOrder.Language.Term.encoding.decode l = (FirstOrder.Language.Term.listDecode l).head?.join

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

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

An encoding of terms as lists.

Equations

• One or more equations did not get rendered due to their size.

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 α] [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 : Countable α] [h2 : Countable ((l : ℕ) × L.Functions l)] : Countable (L.Term α)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• FirstOrder.Language.BoundedFormula.falsum.listEncode = [Sum.inr (Sum.inr (x + 2))]
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).listEncode = [Sum.inl ⟨x, t₁⟩, Sum.inl ⟨x, t₂⟩]
• (FirstOrder.Language.BoundedFormula.rel R ts).listEncode = [Sum.inr (Sum.inl ⟨l, R⟩), Sum.inr (Sum.inr x)] ++ List.map (fun (i : Fin l) => Sum.inl ⟨x, ts i⟩) (List.finRange l)
• (φ₁.imp φ₂).listEncode = Sum.inr (Sum.inr 0) :: φ₁.listEncode ++ φ₂.listEncode
• φ.all.listEncode = Sum.inr (Sum.inr 1) :: φ.listEncode

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

• FirstOrder.Language.BoundedFormula.sigmaAll x = match x with | ⟨n.succ, φ⟩ => ⟨n, φ.all⟩ | x => default

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

• FirstOrder.Language.BoundedFormula.sigmaImp x✝ x = match x✝, x with | ⟨m, φ⟩, ⟨n, ψ⟩ => if h : m = n then ⟨m, φ.imp (⋯.mp ψ)⟩ else default

@[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 (sizeOf l) }

Decodes a list of symbols as a list of formulas.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.BoundedFormula.listDecode (Sum.inr (Sum.inr n.succ.succ) :: l) = (⟨n, FirstOrder.Language.BoundedFormula.falsum⟩, ⟨l, ⋯⟩)
• FirstOrder.Language.BoundedFormula.listDecode (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l) = (if h : n₁ = n₂ then ⟨n₁, FirstOrder.Language.BoundedFormula.equal t₁ (⋯.mp t₂)⟩ else default, ⟨l, ⋯⟩)
• FirstOrder.Language.BoundedFormula.listDecode x = (default, ⟨[], ⋯⟩)

@[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 = some (FirstOrder.Language.BoundedFormula.listDecode l).1

@[simp]

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

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

An encoding of bounded formulas as lists.

Equations

• One or more equations did not get rendered due to their size.

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

theorem FirstOrder.Language.BoundedFormula.card_le {L : FirstOrder.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)