Examples of Finite Structures

Concrete examples from Immerman Chapter 1:

• A small directed graph (3-cycle)
• A binary string (with built-in ordering)
• An isomorphism between two concrete graphs

def Complexity.DescriptiveComplexity.cycle3 : FinStruct Vocabulary.graph

A directed graph on 3 vertices {0, 1, 2} with edges 0→1, 1→2, 2→0 (a directed 3-cycle).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.cycle3' : FinStruct Vocabulary.graph

Another directed 3-cycle: edges 0→2, 2→1, 1→0. This is isomorphic to cycle3 via the permutation 0↦0, 1↦2, 2↦1.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.perm3 : Fin 3 → Fin 3

The permutation 0↦0, 1↦2, 2↦1 on Fin 3 (an involution).

Equations

• Complexity.DescriptiveComplexity.perm3 ⟨0, isLt⟩ = ⟨0, isLt⟩
• Complexity.DescriptiveComplexity.perm3 ⟨1, isLt⟩ = ⟨2, Complexity.DescriptiveComplexity.cycle3._proof_5⟩
• Complexity.DescriptiveComplexity.perm3 ⟨2, isLt⟩ = ⟨1, Complexity.DescriptiveComplexity.cycle3._proof_4⟩

def Complexity.DescriptiveComplexity.cycle3Iso : Iso cycle3 cycle3'

An isomorphism between the two 3-cycles, via the permutation 0↦0, 1↦2, 2↦1.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.string101 : FinStruct Vocabulary.stringBuiltinOrder

The binary string "101" of length 3: positions 0 and 2 are 1-bits. The linear ordering is built-in via Fin 3.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DescriptiveComplexity.cycle3_fo_indistinguishable (φ : Sentence Vocabulary.graph) : Sentence.Models cycle3 φ ↔ Sentence.Models cycle3' φ

The two example 3-cycles satisfy exactly the same first-order sentences: they are isomorphic (cycle3Iso), and first-order logic cannot distinguish isomorphic structures. An end-to-end check of the isomorphism-invariance chain.