Encodings and Cardinality of First-Order Syntax #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main Definitions #

first_order.language.term.encoding encodes terms as lists.
first_order.language.bounded_formula.encoding encodes bounded formulas as lists.

Main Results #

first_order.language.term.card_le shows that the number of terms in L.term α is at most max ℵ₀ # (α ⊕ Σ i, L.functions i).
first_order.language.bounded_formula.card_le shows that the number of bounded formulas in Σ n, L.bounded_formula α 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

source

def first_order.language.term.list_encode {L : first_order.language} {α : Type u'} :

L.term α → list (α ⊕ Σ (i : ℕ), L.functions i)

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

Equations

(first_order.language.term.func f ts).list_encode = sum.inr ⟨a_2, f⟩ :: (list.fin_range a_2).bind (λ (i : fin a_2), (ts i).list_encode)
(first_order.language.term.var i).list_encode = [sum.inl i]

source

def first_order.language.term.list_decode {L : first_order.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

first_order.language.term.list_decode (sum.inr ⟨n, f⟩ :: l) = dite (∀ (i : fin n), ↥(((first_order.language.term.list_decode l).nth ↑i).join.is_some)) (λ (h : ∀ (i : fin n), ↥(((first_order.language.term.list_decode l).nth ↑i).join.is_some)), ↑(first_order.language.term.func f (λ (i : fin n), option.get _)) :: list.drop n (first_order.language.term.list_decode l)) (λ (h : ¬∀ (i : fin n), ↥(((first_order.language.term.list_decode l).nth ↑i).join.is_some)), [option.none])
first_order.language.term.list_decode (sum.inl a :: l) = option.some (first_order.language.term.var a) :: first_order.language.term.list_decode l
first_order.language.term.list_decode list.nil = list.nil

source

theorem first_order.language.term.list_decode_encode_list {L : first_order.language} {α : Type u'} (l : list (L.term α)) :

first_order.language.term.list_decode (l.bind first_order.language.term.list_encode) = list.map option.some l

source

@[simp]

theorem first_order.language.term.encoding_Γ {L : first_order.language} {α : Type u'} :

first_order.language.term.encoding.Γ = (α ⊕ Σ (i : ℕ), L.functions i)

source

@[simp]

theorem first_order.language.term.encoding_decode {L : first_order.language} {α : Type u'} (l : list (α ⊕ Σ (i : ℕ), L.functions i)) :

first_order.language.term.encoding.decode l = (first_order.language.term.list_decode l).head'.join

source

@[simp]

theorem first_order.language.term.encoding_encode {L : first_order.language} {α : Type u'} (ᾰ : L.term α) :

first_order.language.term.encoding.encode ᾰ = ᾰ.list_encode

source

@[protected]

def first_order.language.term.encoding {L : first_order.language} {α : Type u'} :

computability.encoding (L.term α)

An encoding of terms as lists.

Equations

first_order.language.term.encoding = {Γ := α ⊕ Σ (i : ℕ), L.functions i, encode := first_order.language.term.list_encode α, decode := λ (l : list (α ⊕ Σ (i : ℕ), L.functions i)), (first_order.language.term.list_decode l).head'.join, decode_encode := _}

source

theorem first_order.language.term.list_encode_injective {L : first_order.language} {α : Type u'} :

function.injective first_order.language.term.list_encode

source

theorem first_order.language.term.card_le {L : first_order.language} {α : Type u'} :

cardinal.mk (L.term α) ≤ linear_order.max cardinal.aleph_0 (cardinal.mk (α ⊕ Σ (i : ℕ), L.functions i))

source

theorem first_order.language.term.card_sigma {L : first_order.language} {α : Type u'} :

cardinal.mk (Σ (n : ℕ), L.term (α ⊕ fin n)) = linear_order.max cardinal.aleph_0 (cardinal.mk (α ⊕ Σ (i : ℕ), L.functions i))

source

@[protected, instance]

def first_order.language.term.encodable {L : first_order.language} {α : Type u'} [encodable α] [encodable (Σ (i : ℕ), L.functions i)] :

encodable (L.term α)

Equations

first_order.language.term.encodable = encodable.of_left_injection first_order.language.term.list_encode (λ (l : list (α ⊕ Σ (i : ℕ), L.functions i)), (first_order.language.term.list_decode l).head'.join) first_order.language.term.encodable._proof_1

source

@[protected, instance]

def first_order.language.term.countable {L : first_order.language} {α : Type u'} [h1 : countable α] [h2 : countable (Σ (l : ℕ), L.functions l)] :

countable (L.term α)

source

@[protected, instance]

def first_order.language.term.small {L : first_order.language} {α : Type u'} [small α] :

small (L.term α)

source

def first_order.language.bounded_formula.list_encode {L : first_order.language} {α : Type u'} {n : ℕ} :

L.bounded_formula α n → list ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ)

Encodes a bounded formula as a list of symbols.

Equations

φ.all.list_encode = sum.inr (sum.inr 1) :: φ.list_encode
(φ₁.imp φ₂).list_encode = sum.inr (sum.inr 0) :: φ₁.list_encode ++ φ₂.list_encode
(first_order.language.bounded_formula.rel R ts).list_encode = [sum.inr (sum.inl ⟨a_5, R⟩), sum.inr (sum.inr n)] ++ list.map (λ (i : fin a_5), sum.inl ⟨n, ts i⟩) (list.fin_range a_5)
(first_order.language.bounded_formula.equal t₁ t₂).list_encode = [sum.inl ⟨n, t₁⟩, sum.inl ⟨n, t₂⟩]
first_order.language.bounded_formula.falsum.list_encode = [sum.inr (sum.inr (n + 2))]

source

def first_order.language.bounded_formula.sigma_all {L : first_order.language} {α : Type u'} :

(Σ (n : ℕ), L.bounded_formula α n) → (Σ (n : ℕ), L.bounded_formula α n)

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

Equations

first_order.language.bounded_formula.sigma_all ⟨n + 1, φ⟩ = ⟨n, φ.all⟩
first_order.language.bounded_formula.sigma_all ⟨0, snd⟩ = inhabited.default

source

def first_order.language.bounded_formula.sigma_imp {L : first_order.language} {α : Type u'} :

(Σ (n : ℕ), L.bounded_formula α n) → (Σ (n : ℕ), L.bounded_formula α n) → (Σ (n : ℕ), L.bounded_formula α n)

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

Equations

first_order.language.bounded_formula.sigma_imp ⟨m, φ⟩ ⟨n, ψ⟩ = dite (m = n) (λ (h : m = n), ⟨m, φ.imp (_.mp ψ)⟩) (λ (h : ¬m = n), inhabited.default)

source

@[simp]

def first_order.language.bounded_formula.list_decode {L : first_order.language} {α : Type u'} (l : list ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ)) :

(Σ (n : ℕ), L.bounded_formula α n) × {l' // l'.sizeof ≤ linear_order.max 1 l.sizeof}

Decodes a list of symbols as a list of formulas.

Equations

first_order.language.bounded_formula.list_decode (sum.inr (sum.inr (n + 2)) :: l) = (⟨n, first_order.language.bounded_formula.falsum n⟩, ⟨l, _⟩)
first_order.language.bounded_formula.list_decode (sum.inr (sum.inr 1) :: l) = (first_order.language.bounded_formula.sigma_all (first_order.language.bounded_formula.list_decode l).fst, ⟨↑((first_order.language.bounded_formula.list_decode l).snd), _⟩)
first_order.language.bounded_formula.list_decode (sum.inr (sum.inr 0) :: l) = (first_order.language.bounded_formula.sigma_imp (first_order.language.bounded_formula.list_decode l).fst (first_order.language.bounded_formula.list_decode ↑((first_order.language.bounded_formula.list_decode l).snd)).fst, ⟨↑((first_order.language.bounded_formula.list_decode ↑((first_order.language.bounded_formula.list_decode l).snd)).snd), _⟩)
first_order.language.bounded_formula.list_decode (sum.inr (sum.inl ⟨n, R⟩) :: sum.inr (sum.inr k) :: l) = (dite (∀ (i : fin n), ↥(((list.map sum.get_left l).nth ↑i).join.is_some)) (λ (h : ∀ (i : fin n), ↥(((list.map sum.get_left l).nth ↑i).join.is_some)), dite (∀ (i : fin n), (option.get _).fst = k) (λ (h' : ∀ (i : fin n), (option.get _).fst = k), ⟨k, first_order.language.bounded_formula.rel R (λ (i : fin n), _.mp (option.get _).snd)⟩) (λ (h' : ¬∀ (i : fin n), (option.get _).fst = k), inhabited.default)) (λ (h : ¬∀ (i : fin n), ↥(((list.map sum.get_left l).nth ↑i).join.is_some)), inhabited.default), ⟨list.drop n l, _⟩)
first_order.language.bounded_formula.list_decode (sum.inr (sum.inl ⟨fst, snd⟩) :: sum.inr (sum.inl val) :: tl) = (inhabited.default sigma.inhabited, ⟨list.nil ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ), _⟩)
first_order.language.bounded_formula.list_decode (sum.inr (sum.inl ⟨fst, snd⟩) :: sum.inl val :: tl) = (inhabited.default sigma.inhabited, ⟨list.nil ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ), _⟩)
first_order.language.bounded_formula.list_decode [sum.inr (sum.inl ⟨fst, snd⟩)] = (inhabited.default sigma.inhabited, ⟨list.nil ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ), _⟩)
first_order.language.bounded_formula.list_decode (sum.inl ⟨fst, snd⟩ :: sum.inr val :: tl) = (inhabited.default sigma.inhabited, ⟨list.nil ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ), _⟩)
first_order.language.bounded_formula.list_decode (sum.inl ⟨n₁, t₁⟩ :: sum.inl ⟨n₂, t₂⟩ :: l) = (dite (n₁ = n₂) (λ (h : n₁ = n₂), ⟨n₁, first_order.language.bounded_formula.equal t₁ (_.mp t₂)⟩) (λ (h : ¬n₁ = n₂), inhabited.default), ⟨l, _⟩)
first_order.language.bounded_formula.list_decode [sum.inl ⟨fst, snd⟩] = (inhabited.default sigma.inhabited, ⟨list.nil ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ), _⟩)
first_order.language.bounded_formula.list_decode list.nil = (inhabited.default sigma.inhabited, ⟨list.nil ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ), _⟩)

source

@[simp]

theorem first_order.language.bounded_formula.list_decode_encode_list {L : first_order.language} {α : Type u'} (l : list (Σ (n : ℕ), L.bounded_formula α n)) :

(first_order.language.bounded_formula.list_decode (l.bind (λ (φ : Σ (n : ℕ), L.bounded_formula α n), first_order.language.bounded_formula.list_encode φ.snd))).fst = l.head

source

@[simp]

theorem first_order.language.bounded_formula.encoding_encode {L : first_order.language} {α : Type u'} (φ : Σ (n : ℕ), L.bounded_formula α n) :

first_order.language.bounded_formula.encoding.encode φ = first_order.language.bounded_formula.list_encode φ.snd

source

@[protected]

def first_order.language.bounded_formula.encoding {L : first_order.language} {α : Type u'} :

computability.encoding (Σ (n : ℕ), L.bounded_formula α n)

An encoding of bounded formulas as lists.

Equations

first_order.language.bounded_formula.encoding = {Γ := (Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ, encode := λ (φ : Σ (n : ℕ), L.bounded_formula α n), first_order.language.bounded_formula.list_encode φ.snd, decode := λ (l : list ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ)), ↑((first_order.language.bounded_formula.list_decode l).fst), decode_encode := _}

source

@[simp]

theorem first_order.language.bounded_formula.encoding_Γ {L : first_order.language} {α : Type u'} :

first_order.language.bounded_formula.encoding.Γ = ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ)

source

@[simp]

theorem first_order.language.bounded_formula.encoding_decode {L : first_order.language} {α : Type u'} (l : list ((Σ (k : ℕ), L.term (α ⊕ fin k)) ⊕ (Σ (n : ℕ), L.relations n) ⊕ ℕ)) :

first_order.language.bounded_formula.encoding.decode l = ↑((first_order.language.bounded_formula.list_decode l).fst)

source

theorem first_order.language.bounded_formula.list_encode_sigma_injective {L : first_order.language} {α : Type u'} :

function.injective (λ (φ : Σ (n : ℕ), L.bounded_formula α n), first_order.language.bounded_formula.list_encode φ.snd)

source

theorem first_order.language.bounded_formula.card_le {L : first_order.language} {α : Type u'} :

cardinal.mk (Σ (n : ℕ), L.bounded_formula α n) ≤ linear_order.max cardinal.aleph_0 ((cardinal.mk α).lift + L.card.lift)