Finite Structures

A finite structure over a vocabulary V interprets each relation symbol as a relation on a finite universe Fin card, and each constant symbol as an element of that universe.

Following Immerman's Proviso 1.15, all structures have at least 2 elements, ensuring that the built-in constants 0 and 1 are always distinct.

Built-in numeric predicates (min, max, ≤, succ) are not stored in the structure but computed from the Fin ordering (Proviso 1.14).

structure Complexity.DescriptiveComplexity.FinStruct (V : Vocabulary) : Type

A finite structure over vocabulary V. The universe is Fin card. Following Proviso 1.15, we require card ≥ 2.

• card : Nat

  Size of the universe

• hcard : 2 ≤ self.card

  The universe has at least 2 elements (Proviso 1.15)

• rel (i : Fin V.numRels) : (Fin (V.relArity i) → Fin self.card) → Prop

  Interpretation of each relation symbol

• const : Fin V.numConsts → Fin self.card

  Interpretation of each constant symbol

def Complexity.DescriptiveComplexity.termSTRUC : Lean.ParserDescr

STRUC V denotes finite structures over vocabulary V.

Equations

• Complexity.DescriptiveComplexity.termSTRUC = Lean.ParserDescr.node `Complexity.DescriptiveComplexity.termSTRUC 1024 (Lean.ParserDescr.symbol "STRUC")

def Complexity.DescriptiveComplexity.FinStruct.minElem {V : Vocabulary} (A : FinStruct V) : Fin A.card

The minimum element of the universe (built-in constant 0).

Equations

• A.minElem = ⟨0, ⋯⟩

def Complexity.DescriptiveComplexity.FinStruct.maxElem {V : Vocabulary} (A : FinStruct V) : Fin A.card

The maximum element of the universe (built-in constant card - 1).

Equations

• A.maxElem = ⟨A.card - 1, ⋯⟩

def Complexity.DescriptiveComplexity.FinStruct.oneElem {V : Vocabulary} (A : FinStruct V) : Fin A.card

The element 1 of the universe (built-in constant).

Equations

• A.oneElem = ⟨1, ⋯⟩

def Complexity.DescriptiveComplexity.FinStruct.leRel {V : Vocabulary} (A : FinStruct V) (a b : Fin A.card) : Prop

The built-in less-than-or-equal relation on the universe.

Equations

• A.leRel a b = (↑a ≤ ↑b)

def Complexity.DescriptiveComplexity.FinStruct.sucRel {V : Vocabulary} (A : FinStruct V) (a b : Fin A.card) : Prop

The built-in successor relation: sucRel a b iff b = a + 1.

Equations

• A.sucRel a b = (↑b = ↑a + 1)

@[implicit_reducible]

instance Complexity.DescriptiveComplexity.FinStruct.instDecidableRelFinCardLeRel {V : Vocabulary} (A : FinStruct V) : DecidableRel A.leRel

Equations

• A.instDecidableRelFinCardLeRel a b = (↑a).decLe ↑b

@[implicit_reducible]

instance Complexity.DescriptiveComplexity.FinStruct.instDecidableRelFinCardSucRel {V : Vocabulary} (A : FinStruct V) : DecidableRel A.sucRel

Equations

• A.instDecidableRelFinCardSucRel a b = (↑b).decEq (↑a + 1)

theorem Complexity.DescriptiveComplexity.FinStruct.minElem_ne_oneElem {V : Vocabulary} (A : FinStruct V) : A.minElem ≠ A.oneElem

The built-in constants 0 and 1 are distinct (follows from Proviso 1.15).

structure Complexity.DescriptiveComplexity.DecFinStruct (V : Vocabulary) : Type

A decidable finite structure: relations are Bool-valued.

• card : Nat

  Size of the universe

• hcard : 2 ≤ self.card

  The universe has at least 2 elements (Proviso 1.15)

• rel (i : Fin V.numRels) : (Fin (V.relArity i) → Fin self.card) → Bool

  Decidable interpretation of each relation symbol

• const : Fin V.numConsts → Fin self.card

  Interpretation of each constant symbol

def Complexity.DescriptiveComplexity.DecFinStruct.toFinStruct {V : Vocabulary} (A : DecFinStruct V) : FinStruct V

Convert a decidable structure to a propositional one.

Equations

• A.toFinStruct = { card := A.card, hcard := ⋯, rel := fun (i : Fin V.numRels) (args : Fin (V.relArity i) → Fin A.card) => A.rel i args = true, const := A.const }

@[implicit_reducible]

instance Complexity.DescriptiveComplexity.DecFinStruct.instCoeFinStruct {V : Vocabulary} : Coe (DecFinStruct V) (FinStruct V)

Equations

• Complexity.DescriptiveComplexity.DecFinStruct.instCoeFinStruct = { coe := Complexity.DescriptiveComplexity.DecFinStruct.toFinStruct }