Arbitrary canonically ordered queries

An ordered query may depend on the fixed numbering of its input relations. Its source-only encoding serializes no numeric tables: the canonical numeric vocabulary is supplied by Ordered.Basic. Malformed relation tables and universes of size zero or one are rejected.

Main definitions

• Cslib.Logic.FO.Ordered.Structure: an input structure on Fin n, with n ≥ 2.
• Cslib.Logic.FO.Ordered.Query: arbitrary classes of these structures.
• Cslib.Logic.FO.Ordered.Query.encodedLanguage: their source-only encoded languages.
• Cslib.Logic.FO.Ordered.Definable: definability by one canonical ordered sentence.

Main results

• Cslib.Logic.FO.Ordered.Structure.ext: equality of ordered structures through a size cast.
• Cslib.Logic.FO.Ordered.mem_encodedLanguage_encode: exact canonical encoding membership.

References

• N. Immerman, Descriptive Complexity, Provisos 1.14–1.15

structure Cslib.Logic.FO.Ordered.Structure (L : FirstOrder.Language) : Type (max u v)

A finite structure on the canonical universe {0, …, n - 1}, with distinct 0 and 1.

• size : ℕ

  The size of the universe.

• size_ge_two : 2 ≤ self.size

  Immerman's Boolean-constant proviso.

• input : L.Structure (Fin self.size)

  The interpretation of the input symbols. Numeric symbols are supplied separately.

@[instance_reducible]

instance Cslib.Logic.FO.Ordered.structureCoeSort {L : FirstOrder.Language} : CoeSort (Structure L) Type

@[instance_reducible]

instance Cslib.Logic.FO.Ordered.structureInput {L : FirstOrder.Language} (M : Structure L) : L.Structure (Fin M.size)

instance Cslib.Logic.FO.Ordered.structureSize {L : FirstOrder.Language} (M : Structure L) : Fact (2 ≤ M.size)

theorem Cslib.Logic.FO.Ordered.Structure.ext {L : FirstOrder.Language} [L.IsRelational] {M N : Structure L} (h : M.size = N.size) (hrel : ∀ {r : ℕ} (R : L.Relations r) (x : Fin r → Fin M.size), FirstOrder.Language.Structure.RelMap R x ↔ FirstOrder.Language.Structure.RelMap R (Fin.cast h ∘ x)) : M = N

Ordered structures over a relational language are equal when their sizes are and the size cast preserves every relation.

@[reducible, inline]

abbrev Cslib.Logic.FO.Ordered.Query (L : FirstOrder.Language) : Type (max v u)

An ordered query is an arbitrary class of canonically ordered structures. Input relations need not be invariant under permutations that change the fixed order.

def Cslib.Logic.FO.Ordered.Definable {L : FirstOrder.Language} (K : Query L) : Prop

An ordered query is first-order definable if a sentence defines it on every canonical ordered structure.

def Cslib.Logic.FO.Ordered.decoded {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (a : EncodedStructure) (hn : 2 ≤ a.1) : Structure L

Decode a source-only input with a universe of size at least two.

def Cslib.Logic.FO.Ordered.Query.encodedLanguage {L : FirstOrder.Language} [L.IsRelational] (K : Query L) (v : Vocabulary L) : Set EncodedStructure

The language of an ordered query. Only original relation tables occur in the input; malformed shapes and universes of size zero or one are rejected.

theorem Cslib.Logic.FO.Ordered.Query.not_mem_encodedLanguage_of_not_wellFormed {L : FirstOrder.Language} [L.IsRelational] (K : Query L) (v : Vocabulary L) {a : EncodedStructure} (ha : ¬v.WellFormed a) : a ∉ K.encodedLanguage v

Malformed source tables are rejected independently of the query.

theorem Cslib.Logic.FO.Ordered.Query.not_mem_encodedLanguage_of_lt_two {L : FirstOrder.Language} [L.IsRelational] (K : Query L) (v : Vocabulary L) {a : EncodedStructure} (ha : a.1 < 2) : a ∉ K.encodedLanguage v

Universes of size zero or one are rejected independently of the query.

noncomputable def Cslib.Logic.FO.Ordered.encode {L : FirstOrder.Language} (v : Vocabulary L) (M : Structure L) : EncodedStructure

The canonical source-only encoding of an ordered structure.

@[simp]

theorem Cslib.Logic.FO.Ordered.decoded_encode {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (M : Structure L) : decoded v (encode v M) ⋯ = M

Decoding the canonical encoding returns the same ordered structure.

@[simp]

theorem Cslib.Logic.FO.Ordered.mem_encodedLanguage_encode {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (K : Query L) (M : Structure L) : encode v M ∈ K.encodedLanguage v ↔ M ∈ K

The canonical encoding of an ordered structure is in the encoded language of a query exactly when the structure is in the query.