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 inL.Term α
is at mostmax ℵ₀ # (α ⊕ Σ i, L.Functions i)
.FirstOrder.Language.BoundedFormula.card_le
shows that the number of bounded formulas inΣ n, L.BoundedFormula α n
is at mostmax ℵ₀ (Cardinal.lift.{max u v} #α + Cardinal.lift.{u'} L.card)
.
TODO #
Primcodable
instances for terms and formulas, based on theencoding
s- 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)
Instances For
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
Instances For
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
An encoding of terms as lists.
Instances For
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)]
:
instance
FirstOrder.Language.Term.instCountableTerm
{L : FirstOrder.Language}
{α : Type u'}
[h1 : Countable α]
[h2 : Countable ((l : ℕ) × FirstOrder.Language.Functions L 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 φ
Instances For
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.
Instances For
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.
Instances For
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 ⊕ ℕ))
:
Decodes a list of symbols as a list of formulas.
Instances For
@[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.
Instances For
theorem
FirstOrder.Language.BoundedFormula.listEncode_sigma_injective
{L : FirstOrder.Language}
{α : Type u'}
:
Function.Injective fun φ => FirstOrder.Language.BoundedFormula.listEncode φ.snd