Quantifier-free first-order reductions

A class K of L-structures is quantifier-free reducible to a class K' of L'-structures (FO.QFReduces K K') when it is first-order reducible to it (FO.Reduces) through a quantifier-free interpretation (Interpretation.IsQF): the domain and the relations of the interpreted structure are Boolean combinations of atomic formulas of L. Like first-order reducibility, quantifier-free reducibility is reflexive on classes closed under isomorphism of a relational language, because the identity interpretation is quantifier-free, and transitive when the last class is closed under isomorphism, because quantifier-free interpretations compose.

The vocabularies are parameters: no order or BIT predicate is assumed, and the dimension is any finite type. Quantifier-free reductions are therefore not quantifier-free projections, which moreover allow only a single input literal for each output bit and fix the numeric vocabulary Immerman and Landau, Definitions 3.3--3.6; see Complexity.Logics.FirstOrder.Projection.

A reduction through a given interpretation is proved by two kinds of arguments: syntactic side conditions, such as quantifier-freeness, and the semantic statement that M ∈ K exactly when the interpreted structure belongs to K'. For a one-dimensional interpretation whose domain formula always holds, QFReduces.of_unitStructure states the semantic part on the input universe itself, as Reduces.of_unitStructure does for first-order reductions; for an interpretation of any dimension whose domain formula always holds, QFReduces.of_tupleStructure states it on tuples of the input universe. The tactic fo_reduction applies these lemmas and proves the side conditions.

Main definitions

• Cslib.Logic.FO.QFReduces: quantifier-free reducibility between classes of finite structures.

Main results

• Cslib.Logic.FO.QFReduces.reduces: quantifier-free reductions are first-order reductions.
• Cslib.Logic.FO.QFReduces.refl, Cslib.Logic.FO.QFReduces.trans: quantifier-free reducibility is a preorder on classes closed under isomorphism.
• Cslib.Logic.FO.QFReduces.of_unitStructure: quantifier-free reductions through one-dimensional interpretations, stated on the input universe.
• Cslib.Logic.FO.QFReduces.of_tupleStructure: quantifier-free reductions through interpretations whose domain formula always holds, stated on tuples of the input universe.

References

• N. Immerman, Descriptive Complexity
• N. Immerman and S. Landau, The Complexity of Iterated Multiplication

def Cslib.Logic.FO.QFReduces {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 quantifier-free reducible to a class K' of L'-structures when some quantifier-free first-order interpretation of L' in L maps the finite members of K into K' and the other finite L-structures outside K'.

theorem Cslib.Logic.FO.QFReduces.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') (hI : I.IsQF) : QFReduces K K'

A quantifier-free reduction through a given interpretation.

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

A quantifier-free reduction is a first-order reduction.

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

Quantifier-free reducibility is reflexive on classes closed under isomorphism, through the identity interpretation.

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

Quantifier-free reducibility is transitive when the last class is closed under isomorphism, through the composite interpretation.

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

A class quantifier-free reducible to a class closed under isomorphism is closed under isomorphism.

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

A quantifier-free reduction from K to K' is also a reduction from Kᶜ to K'ᶜ.

theorem Cslib.Logic.FO.QFReduces.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') (hI : I.IsQF) (hK' : IsoClosed K') (hdom : ∀ (M : Type w) [inst : L.Structure M] [Finite M] (x : M), I.domain.Realize fun (x_1 : Unit) => x) : QFReduces K K'

A quantifier-free 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.

theorem Cslib.Logic.FO.QFReduces.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') (hI : I.IsQF) (hK' : IsoClosed K') (hdom : ∀ (M : Type w) [inst : L.Structure M] [Finite M] (x : ι → M), I.domain.Realize x) : QFReduces K K'

A quantifier-free 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.