Coding Space for Countable Structures

This file defines the space of countable relational L-structures coded as functions from relation queries to Bool. The carrier-parametric versions RelQueryOn L α and StructureSpaceOn L α generalize over the carrier type, while RelQuery L and StructureSpace L specialize to carrier ℕ.

Main Definitions

• RelQueryOn L α: Carrier-parametric relation query index type.
• StructureSpaceOn L α: Carrier-parametric coding space RelQueryOn L α → Bool.
• RelQuery L: Relation queries for carrier ℕ (= RelQueryOn L ℕ).
• StructureSpace L: The coding space for ℕ-structures (= StructureSpaceOn L ℕ).
• StructureSpaceOn.toStructure: Decode a code into an L-structure on carrier α.
• StructureSpaceOn.ofStructure: Encode a structure into a code.

Main Results

• StructureSpaceOn.relMap_toStructure: Relation holding in the decoded structure corresponds to the code returning true.
• StructureSpaceOn.toStructure_ofStructure: Round-trip from structure to code to structure preserves relation satisfaction.

def FirstOrder.Language.RelQueryOn (L : Language) (α : Type u_1) : Type (max v u_1)

A carrier-parametric relation query: a choice of relation symbol and a tuple of elements from the carrier type α.

Equations

• L.RelQueryOn α = ((R : (l : ℕ) × L.Relations l) × (Fin R.fst → α))

def FirstOrder.Language.RelQuery (L : Language) : Type v

A relation query for carrier ℕ.

Equations

• L.RelQuery = L.RelQueryOn ℕ

instance FirstOrder.Language.instCountableRelQueryOnOfSigmaNatRelations {L : Language} {α : Type u_1} [Countable ((l : ℕ) × L.Relations l)] [Countable α] : Countable (L.RelQueryOn α)

instance FirstOrder.Language.instCountableRelQueryOfSigmaNatRelations {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Countable L.RelQuery

@[reducible, inline]

abbrev FirstOrder.Language.StructureSpaceOn (L : Language) (α : Type u_1) : Type (max u_1 v)

The carrier-parametric coding space for L-structures on α: for each relation query, does the relation hold on that tuple? This is an abbrev so type class resolution can see through it.

Equations

• L.StructureSpaceOn α = (L.RelQueryOn α → Bool)

def FirstOrder.Language.StructureSpace (L : Language) : Type v

The coding space for countable L-structures on ℕ: for each relation query, does the relation hold on that tuple?

Equations

• L.StructureSpace = L.StructureSpaceOn ℕ

@[reducible, inline]

abbrev FirstOrder.Language.StructurePairSpaceOn (L : Language) (α : Type u_1) : Type (max u_1 v)

The pair space for carrier α.

Equations

• L.StructurePairSpaceOn α = (L.StructureSpaceOn α × L.StructureSpaceOn α)

noncomputable def FirstOrder.Language.StructureSpaceOn.toStructure {L : Language} {α : Type u_1} [L.IsRelational] (c : L.StructureSpaceOn α) : L.Structure α

Decode a code into an L-structure on carrier α. Relations are determined by the code; functions are eliminated by IsRelational.

Equations

• c.toStructure = { funMap := fun {n : ℕ} (f : L.Functions n) => isEmptyElim f, RelMap := fun {x : ℕ} (R : L.Relations x) (v : Fin x → α) => c ⟨⟨x, R⟩, v⟩ = true }

@[simp]

theorem FirstOrder.Language.StructureSpaceOn.relMap_toStructure {L : Language} {α : Type u_1} [L.IsRelational] (c : L.StructureSpaceOn α) {l : ℕ} (R : L.Relations l) (v : Fin l → α) : Structure.RelMap R v ↔ c ⟨⟨l, R⟩, v⟩ = true

The relation holding in the decoded structure corresponds to the code value.

noncomputable def FirstOrder.Language.StructureSpaceOn.ofStructure {L : Language} {α : Type u_1} [L.IsRelational] (inst : L.Structure α) : L.StructureSpaceOn α

Encode an L-structure on carrier α into a code. Takes an explicit structure instance rather than using the typeclass.

Equations

• FirstOrder.Language.StructureSpaceOn.ofStructure inst ⟨⟨fst, R⟩, v⟩ = decide (FirstOrder.Language.Structure.RelMap R v)

theorem FirstOrder.Language.StructureSpaceOn.toStructure_ofStructure {L : Language} {α : Type u_1} [L.IsRelational] (inst : L.Structure α) {l : ℕ} (R : L.Relations l) (v : Fin l → α) : Structure.RelMap R v ↔ Structure.RelMap R v

Round-trip: decoding the code of a structure preserves relation satisfaction.

theorem FirstOrder.Language.StructureSpaceOn.ofStructure_toStructure {L : Language} {α : Type u_1} [L.IsRelational] (c : L.StructureSpaceOn α) : ofStructure c.toStructure = c

Round-trip: encoding a decoded structure recovers the original code.

noncomputable def FirstOrder.Language.StructureSpace.toStructure {L : Language} [L.IsRelational] (c : L.StructureSpace) : L.Structure ℕ

Decode a code into an L-structure on ℕ.

Equations

• c.toStructure = FirstOrder.Language.StructureSpaceOn.toStructure c

@[simp]

theorem FirstOrder.Language.StructureSpace.relMap_toStructure {L : Language} [L.IsRelational] (c : L.StructureSpace) {l : ℕ} (R : L.Relations l) (v : Fin l → ℕ) : Structure.RelMap R v ↔ c ⟨⟨l, R⟩, v⟩ = true

The relation holding in the decoded structure corresponds to the code value.

noncomputable def FirstOrder.Language.StructureSpace.ofStructure {L : Language} [L.IsRelational] (inst : L.Structure ℕ) : L.StructureSpace

Encode an L-structure on ℕ into a code.

Equations

• FirstOrder.Language.StructureSpace.ofStructure inst = FirstOrder.Language.StructureSpaceOn.ofStructure inst

theorem FirstOrder.Language.StructureSpace.toStructure_ofStructure {L : Language} [L.IsRelational] (inst : L.Structure ℕ) {l : ℕ} (R : L.Relations l) (v : Fin l → ℕ) : Structure.RelMap R v ↔ Structure.RelMap R v

Round-trip: decoding the code of a structure preserves relation satisfaction.

theorem FirstOrder.Language.StructureSpace.ofStructure_toStructure {L : Language} [L.IsRelational] (c : L.StructureSpace) : ofStructure c.toStructure = c

Round-trip: encoding a decoded structure recovers the original code.