First-order definability and first-order reductions

Descriptive complexity studies classes of finite structures. As in Mathlib's model theory, a class of L-structures is a set of bundled structures, Set (Bundled L.Structure); the notions below only look at its finite members. In particular, a class is closed under isomorphism (Cslib.Logic.IsoClosed) when it contains, with a finite structure, every structure isomorphic to it.

A class K is first-order definable (FO.Definable K) when some first-order sentence holds in exactly the finite structures of K. Such a class is closed under isomorphism, and the definable classes are closed under complement, intersection and union.

A class K of L-structures is first-order reducible to a class K' of L'-structures (FO.Reduces K K') when some first-order interpretation I of L' in L satisfies M ∈ K ↔ I.Model M ∈ K' for every finite M Immerman, Definition 2.11. Reducibility is reflexive and transitive on classes closed under isomorphism Immerman, Exercise 2.15, and first-order definability is closed under it: if K' is defined by φ, then K is defined by the pullback of φ Immerman, Definition 3.9 and Framework 3.12.

Senellart and Gnatenko formalize first-order reductions over Mathlib's model theory too, as the backbone of a library of completeness results Senellart and Gnatenko. Their decision problems are predicates on structures bundled with a proof of invariance under isomorphism, and their reductions are data, required to be correct on the finite nonempty structures. Here a class is a set of bundled structures, as in Mathlib, invariance under isomorphism is the separate hypothesis IsoClosed, reducibility is a proposition, and the empty structure is not set apart.

Main definitions

• Cslib.Logic.IsoClosed: closure of a class of structures under isomorphism of finite structures.
• Cslib.Logic.FO.Definable: first-order definability of a class of finite structures.
• Cslib.Logic.FO.Reduces: first-order reducibility between classes of finite structures.

Main results

• Cslib.Logic.FO.Definable.isoClosed: definable classes are closed under isomorphism.
• Cslib.Logic.FO.Definable.compl, Cslib.Logic.FO.Definable.inter, Cslib.Logic.FO.Definable.union: Boolean operations.
• Cslib.Logic.FO.Reduces.refl, Cslib.Logic.FO.Reduces.trans: reducibility is a preorder on classes closed under isomorphism.
• Cslib.Logic.FO.Reduces.isoClosed: a class reducible to a class closed under isomorphism is closed under isomorphism.
• Cslib.Logic.IsoClosed.of_forall_imp: closure under isomorphism from one direction.
• Cslib.Logic.FO.Reduces.of_unitStructure: a reduction through a one-dimensional interpretation whose domain formula always holds, stated on the input universe.
• Cslib.Logic.FO.Reduces.of_tupleStructure: a reduction through an interpretation whose domain formula always holds, stated on the tuples of the input universe.
• Cslib.Logic.FO.Definable.of_reduces: definability is closed under first-order reductions.

References

• N. Immerman, Descriptive Complexity
• P. Senellart and A. Gnatenko, Descriptive Complexity in Lean: Completeness by First-Order Reductions

def Cslib.Logic.IsoClosed {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) : Prop

A class of structures is closed under isomorphism when it contains, with a finite structure, every structure isomorphic to it. Only finite structures are asked about, as in the notions of definability and reducibility of finite structures.

theorem Cslib.Logic.IsoClosed.of_forall_imp {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} (h : ∀ ⦃M N : CategoryTheory.Bundled L.Structure⦄ [Finite ↑M] (a : L.Equiv ↑M ↑N), M ∈ K → N ∈ K) : IsoClosed K

A class containing the image of each of its finite members under each isomorphism is closed under isomorphism.

First-order definability

def Cslib.Logic.FO.Definable {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) : Prop

A class of structures is first-order definable when some first-order sentence holds in exactly its finite members, among all finite structures.

theorem Cslib.Logic.FO.Definable.isEmpty {L : FirstOrder.Language} : Definable {M : CategoryTheory.Bundled L.Structure | IsEmpty ↑M}

The class of empty structures is first-order definable, by ∀ x, ⊥.

theorem Cslib.Logic.FO.Definable.isoClosed {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} (hK : Definable K) : IsoClosed K

A first-order definable class is closed under isomorphism.

theorem Cslib.Logic.FO.Definable.compl {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} (hK : Definable K) : Definable Kᶜ

The complement of a first-order definable class is first-order definable.

theorem Cslib.Logic.FO.Definable.inter {L : FirstOrder.Language} {K₁ K₂ : Set (CategoryTheory.Bundled L.Structure)} (h₁ : Definable K₁) (h₂ : Definable K₂) : Definable (K₁ ∩ K₂)

The intersection of two first-order definable classes is first-order definable.

theorem Cslib.Logic.FO.Definable.union {L : FirstOrder.Language} {K₁ K₂ : Set (CategoryTheory.Bundled L.Structure)} (h₁ : Definable K₁) (h₂ : Definable K₂) : Definable (K₁ ∪ K₂)

The union of two first-order definable classes is first-order definable.

First-order reductions

theorem Cslib.Logic.FO.coe_bundledOf {L : FirstOrder.Language} (M : Type w) [L.Structure M] : ↑(CategoryTheory.Bundled.of M) = M

The universe of a bundled structure Bundled.of M is M. The simp set fo_realize uses this to see the interpreted structure in the semantic statement of a reduction.

instance Cslib.Logic.FO.instFiniteαStructureOfModel {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type u_1} [Finite ι] (I : Interpretation L L' ι) (M : Type w) [L.Structure M] [Finite M] : Finite ↑(CategoryTheory.Bundled.of (I.Model M))

The structure interpreted in a finite structure is finite, also when bundled.

def Cslib.Logic.FO.Reduces {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (K : Set (CategoryTheory.Bundled L.Structure)) (K' : Set (CategoryTheory.Bundled L'.Structure)) : Prop

A class K of L-structures is first-order reducible to a class K' of L'-structures when some first-order interpretation of L' in L maps the finite members of K into K' and the other finite L-structures outside K' Immerman, Definition 2.11.

theorem Cslib.Logic.FO.Reduces.refl {L : FirstOrder.Language} [L.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} (hK : IsoClosed K) : Reduces K K

First-order reducibility is reflexive on classes closed under isomorphism, through the identity interpretation.

theorem Cslib.Logic.FO.Reduces.trans {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} [L'.IsRelational] [L''.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} {K'' : Set (CategoryTheory.Bundled L''.Structure)} (h : Reduces K K') (h' : Reduces K' K'') (hK'' : IsoClosed K'') : Reduces K K''

First-order reducibility is transitive when the last class is closed under isomorphism, through the composite interpretation Immerman, Exercise 2.15.

theorem Cslib.Logic.FO.Reduces.isoClosed {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (h : Reduces K K') (hK' : IsoClosed K') : IsoClosed K

A class reducible to a class closed under isomorphism is closed under isomorphism: isomorphic structures interpret isomorphic structures.

theorem Cslib.Logic.FO.Reduces.of_interpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} {ι : Type} [Finite ι] (I : Interpretation L L' ι) (h : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], M ∈ K ↔ CategoryTheory.Bundled.of (I.Model ↑M) ∈ K') : Reduces K K'

A first-order reduction through a given interpretation.

theorem Cslib.Logic.FO.Reduces.compl {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (h : Reduces K K') : Reduces Kᶜ K'ᶜ

A first-order reduction from K to K' is also a reduction from Kᶜ to K'ᶜ.

One-dimensional reductions

theorem Cslib.Logic.FO.Interpretation.mem_iff_unitStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K' : Set (CategoryTheory.Bundled L'.Structure)} (hK' : IsoClosed K') (I : Interpretation L L' Unit) (M : Type w) [L.Structure M] [Finite M] (hdom : ∀ (x : M), I.domain.Realize fun (x_1 : Unit) => x) : CategoryTheory.Bundled.of (I.Model M) ∈ K' ↔ { α := M, str := I.unitStructure M } ∈ K'

For a one-dimensional interpretation whose domain formula always holds, the interpreted structure belongs to a class closed under isomorphism exactly when the structure defined on the input universe does.

theorem Cslib.Logic.FO.Reduces.of_unitStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (I : Interpretation L L' Unit) (h : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], M ∈ K ↔ { α := ↑M, str := I.unitStructure ↑M } ∈ K') (hK' : IsoClosed K') (hdom : ∀ (M : Type w) [inst : L.Structure M] [Finite M] (x : M), I.domain.Realize fun (x_1 : Unit) => x) : Reduces K K'

A first-order reduction through a one-dimensional interpretation whose domain formula holds of every element of every finite structure, to a class closed under isomorphism, stated on the input universe: M ∈ K exactly when M, with the relations defined by the interpretation, belongs to K'.

Reductions on tuples

theorem Cslib.Logic.FO.Interpretation.mem_iff_tupleStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K' : Set (CategoryTheory.Bundled L'.Structure)} (hK' : IsoClosed K') {ι : Type} [Finite ι] (I : Interpretation L L' ι) (M : Type w) [L.Structure M] [Finite M] (hdom : ∀ (x : ι → M), I.domain.Realize x) : CategoryTheory.Bundled.of (I.Model M) ∈ K' ↔ { α := ι → M, str := I.tupleStructure M } ∈ K'

For an interpretation whose domain formula holds of every tuple, the interpreted structure belongs to a class closed under isomorphism exactly when the structure defined on the tuples of the input universe does.

theorem Cslib.Logic.FO.Reduces.of_tupleStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} {ι : Type} [Finite ι] (I : Interpretation L L' ι) (h : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], M ∈ K ↔ { α := ι → ↑M, str := I.tupleStructure ↑M } ∈ K') (hK' : IsoClosed K') (hdom : ∀ (M : Type w) [inst : L.Structure M] [Finite M] (x : ι → M), I.domain.Realize x) : Reduces K K'

A first-order reduction through an interpretation whose domain formula holds of every tuple of every finite structure, to a class closed under isomorphism, stated on the tuples of the input universe: M ∈ K exactly when the tuples ι → M, with the relations defined by the interpretation, belong to K'.

theorem Cslib.Logic.FO.Definable.of_reduces {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (hK' : Definable K') (h : Reduces K K') : Definable K

First-order definability is closed under first-order reductions: if K reduces to a class K' defined by φ, then K is defined by the pullback of φ Immerman, Framework 3.12.