Order-free interpretations on structures with at least two elements

The reductions in this module use order-free first-order interpretations. Input structures have no built-in order or numeric predicates; these are variants of the standard ordered setting.

Order-free reductions (Cslib.Logic.FO.Reduces) are asked to be correct on every finite structure, including the empty one and those with one element. On these, an interpretation of the unordered structures of this library has little room: an interpretation of positive dimension maps the empty structure to the empty structure, and a structure with one element to a structure with at most one element. Whether a reduction to a class exists then depends on how the class treats its smallest members. Every structure with at most one element is an independent set instance with a solution, for example, while the empty clause on one element is an unsatisfiable CNF structure, so SAT is not order-free reducible to independent set in this sense.

Immerman's Boolean-constant convention requires at least two elements, with distinct 0 and 1 Immerman, Proviso 1.15. Here the same size restriction is used without built-in order: ReducesNontrivial K K' requires an order-free interpretation to be correct on each finite structure with at least two elements. It is distinct from the unrestricted Reduces, which also handles empty and singleton structures. Such reductions compose when the first interpretation preserves nontriviality, or when the second reduction is unrestricted. A compiled tagged interpretation preserves nontriviality when its tagged output is nonempty.

Main definitions

• Cslib.Logic.FO.ReducesNontrivial: order-free reducibility on structures with two distinct elements.

Main results

• Cslib.Logic.FO.Reduces.reducesNontrivial: order-free reductions are reductions on nontrivial structures.
• Cslib.Logic.FO.ReducesNontrivial.refl, Cslib.Logic.FO.ReducesNontrivial.trans_reduces, Cslib.Logic.FO.ReducesNontrivial.trans_of_nontrivial: reflexivity and composition.
• Cslib.Logic.FO.ReducesNontrivial.of_tagged: reductions on nontrivial structures by tagged interpretations; no nonemptiness assumption is needed for correctness.
• Cslib.Logic.FO.TaggedInterpretation.nontrivial_and_mem_iff_toInterpretation: correctness together with nontriviality preservation when the tagged outputs are nonempty.
• Cslib.Logic.FO.Reduces.of_reducesNontrivial: between classes containing every structure with at most one element, reductions on nontrivial structures are order-free reductions.

References

• N. Immerman, Descriptive Complexity

def Cslib.Logic.FO.ReducesNontrivial {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 reducible by an order-free interpretation on nontrivial structures to a class K' of L'-structures when some first-order interpretation of L' in L maps every finite L-structure with two distinct elements inside K' exactly when it is in K.

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

An order-free reduction is a reduction on nontrivial structures.

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

Reducibility on nontrivial structures is reflexive on classes closed under isomorphism.

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

A reduction on nontrivial structures from K to K' is also one from Kᶜ to K'ᶜ.

theorem Cslib.Logic.FO.ReducesNontrivial.trans_reduces {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 : ReducesNontrivial K K') (h' : Reduces K' K'') (hK'' : IsoClosed K'') : ReducesNontrivial K K''

A reduction on nontrivial structures followed by an order-free reduction.

theorem Cslib.Logic.FO.ReducesNontrivial.trans_of_nontrivial {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)} {ι : Type} [Finite ι] (I : Interpretation L L' ι) (hI : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], Nontrivial ↑M → Nontrivial (I.Model ↑M) ∧ (M ∈ K ↔ CategoryTheory.Bundled.of (I.Model ↑M) ∈ K')) (h' : ReducesNontrivial K' K'') (hK'' : IsoClosed K'') : ReducesNontrivial K K''

A reduction on nontrivial structures through an interpretation that keeps them nontrivial, followed by a reduction on nontrivial structures.

theorem Cslib.Logic.FO.Reduces.of_reducesNontrivial {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (h : ReducesNontrivial K K') (hK : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], Subsingleton ↑M → M ∈ K) (hK' : ∀ (N : CategoryTheory.Bundled L'.Structure) [Finite ↑N], Subsingleton ↑N → N ∈ K') : Reduces K K'

A reduction on nontrivial structures between classes containing every finite structure with at most one element is an order-free reduction: an interpretation maps a structure with at most one element to a structure with at most one element.

theorem Cslib.Logic.FO.TaggedInterpretation.nontrivial_and_mem_iff_toInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (hK' : IsoClosed K') (hcopy : CopyInvariant K') {T : Type} [Finite T] {ι : T → Type} [∀ (t : T), Finite (ι t)] (I : TaggedInterpretation L L' T ι) (hne : ∀ (M : Type w) [inst : L.Structure M] [Finite M], Nontrivial M → Nonempty (I.Model M)) (hlarge : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], Nontrivial ↑M → (M ∈ K ↔ CategoryTheory.Bundled.of (I.Model ↑M) ∈ K')) (M : CategoryTheory.Bundled L.Structure) [Finite ↑M] (hM : Nontrivial ↑M) : Nontrivial ((I.toInterpretation (Interpretation.empty L L')).Model ↑M) ∧ (M ∈ K ↔ CategoryTheory.Bundled.of ((I.toInterpretation (Interpretation.empty L L')).Model ↑M) ∈ K')

A compiled tagged interpretation preserves class membership and nontriviality when its tagged outputs are nonempty and the target class is closed under isomorphism and copies.

theorem Cslib.Logic.FO.ReducesNontrivial.of_tagged {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (hK' : IsoClosed K') (hcopy : CopyInvariant K') {T : Type} [Finite T] {ι : T → Type} [∀ (t : T), Finite (ι t)] (I : TaggedInterpretation L L' T ι) (hlarge : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], Nontrivial ↑M → (M ∈ K ↔ CategoryTheory.Bundled.of (I.Model ↑M) ∈ K')) : ReducesNontrivial K K'

Tagged interpretations give reductions on nontrivial structures to classes closed under isomorphism and copies.