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
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
Instances For
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
Instances For
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) = l
@[simp]
theorem
FirstOrder.Language.Term.encoding_encode
{L : FirstOrder.Language}
{α : Type u'}
:
∀ (a : L.Term α), FirstOrder.Language.Term.encoding.encode a = a.listEncode
@[simp]
@[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
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.
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 (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
- ⋯ = ⋯
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
Instances For
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
Instances For
@[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⟩
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
Instances For
@[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]
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 = []
Instances For
@[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) = l
@[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
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.
Instances For
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)