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).flatMap fun (i : Fin l) => (ts i).listEncode

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

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.

@[simp]

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

@[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_decode {L : FirstOrder.Language} {α : Type u'} (l : List (α ⊕ (i : ℕ) × L.Functions i)) : FirstOrder.Language.Term.encoding.decode l = (do let a ← (FirstOrder.Language.Term.listDecode l).head? pure (some a)).join

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 ⟨n.succ, φ⟩ = ⟨n, φ.all⟩
• FirstOrder.Language.BoundedFormula.sigmaAll x = default

@[simp]

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

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 ⟨m, φ⟩ ⟨n, ψ⟩ = if h : m = n then ⟨m, φ.imp (⋯.mp ψ)⟩ else default

@[simp]

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

Decodes a list of symbols as a list of formulas.

@[irreducible]

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

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⟩ :: FirstOrder.Language.BoundedFormula.listDecode l
• FirstOrder.Language.BoundedFormula.listDecode x = []

@[simp]

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

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.

@[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 = (FirstOrder.Language.BoundedFormula.listDecode l)[0]?

@[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_Γ {L : FirstOrder.Language} {α : Type u'} : FirstOrder.Language.BoundedFormula.encoding.Γ = ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)

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)