First-order reductions between ordered queries

An ordered query K first-order reduces to K', written K ≤_fo K', when some first-order query on ordered structures maps the members of K to members of K' and the other structures outside K' [Immerman1999, Definition 2.11]. A first-order query on ordered structures includes first-order definitions of the numeric relations and constants of its image [Immerman1999, Remark 1.32]; with a domain formula other than true these are a genuine obligation, since target BIT need not be definable [Immerman1999, the paragraph after Exercise 1.33]. Here the admissible maps are therefore the images I.map hI of admissible ordered interpretations I that have a numeric certificate, and Ordered.Reduces is the many-one reducibility by these maps.

Reflexivity uses the identity interpretation of dimension one. Transitivity composes interpretations, substituting the inner numeric definitions into the outer formulas [Immerman1999, Proposition 1.28 and Exercise 2.15(1)]. Definability pulls back along reductions.

Main definitions

• Cslib.Logic.FO.Ordered.IsFirstOrderMap: the images of certified admissible interpretations.
• Cslib.Logic.FO.Ordered.Reduces: first-order reducibility of ordered queries.
• Cslib.Logic.FO.Ordered.DomainInterpretation.id: the identity interpretation.
• Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.id: its numeric certificate.

Main results

• Cslib.Logic.FO.Ordered.Reduces.refl, Cslib.Logic.FO.Ordered.Reduces.trans: ≤_fo is a preorder.
• Cslib.Logic.FO.Ordered.Reduces.compl: reductions between complements.
• Cslib.Logic.FO.Ordered.IsFirstOrderMap.isDomainMap: first-order maps are domain maps.
• Cslib.Logic.FO.Ordered.Definable.of_reduces: first-order definability pulls back.

References

• N. Immerman, Descriptive Complexity, Proviso 1.15, Definition 1.26, Proposition 1.28, Remark 1.32, Exercise 1.33 and the paragraph after it, Definition 2.11 and Exercise 2.15(1).

The identity interpretation

def Cslib.Logic.FO.Ordered.DomainInterpretation.id (L : FirstOrder.Language) : DomainInterpretation L L 1

The identity interpretation of dimension one: every element is in the domain and every input relation defines itself.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.card_id {L : FirstOrder.Language} (M : Structure L) : (id L).card M = M.size

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_id {L : FirstOrder.Language} {M : Structure L} (i : Fin ((id L).card M)) : (id L).unrank M i = fun (x : Fin 1) => Fin.cast ⋯ i

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.admissible_id {L : FirstOrder.Language} : (id L).Admissible

def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.id (L : FirstOrder.Language) : (DomainInterpretation.id L).Certificate

The identity interpretation defines the canonical numerics directly.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.map_id {L : FirstOrder.Language} [L.IsRelational] (M : Structure L) : (id L).map ⋯ M = M

The identity interpretation maps every ordered structure to itself.

First-order reductions

def Cslib.Logic.FO.Ordered.IsFirstOrderMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (f : Structure L → Structure L') : Prop

The maps between ordered structures given by first-order queries: images under admissible ordered interpretations with numeric certificates.

theorem Cslib.Logic.FO.Ordered.IsFirstOrderMap.isDomainMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {f : Structure L → Structure L'} (hf : IsFirstOrderMap f) : IsDomainMap f

First-order maps are domain maps, forgetting the certificate.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.isFirstOrderMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {k : ℕ} {I : DomainInterpretation L L' k} (hI : I.Admissible) (C : I.Certificate) : IsFirstOrderMap (I.map hI)

The image of a certified admissible interpretation is a first-order map.

theorem Cslib.Logic.FO.Ordered.IsFirstOrderMap.id {L : FirstOrder.Language} [L.IsRelational] : IsFirstOrderMap _root_.id

The identity is a first-order map.

theorem Cslib.Logic.FO.Ordered.IsFirstOrderMap.comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} [L'.IsRelational] [L''.IsRelational] {f : Structure L → Structure L'} {g : Structure L' → Structure L''} (hf : IsFirstOrderMap f) (hg : IsFirstOrderMap g) : IsFirstOrderMap (g ∘ f)

First-order maps compose.

def Cslib.Logic.FO.Ordered.Reduces {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (K : Query L) (K' : Query L') : Prop

First-order reducibility of ordered queries, K ≤_fo K': many-one reducibility by first-order maps [Immerman1999, Definition 2.11 and Remark 1.32]. This is the ordered counterpart of the order-free Cslib.Logic.FO.Reduces.

The target language is relational: the image carries only the canonical numeric constants, and Immerman's formulas for target constant symbols are not handled. The image is always ordered lexicographically, Remark 1.32's default ("unless we state otherwise"), so this is the lexicographic case of ≤_fo; reductions whose image order is another definable order are not covered.

theorem Cslib.Logic.FO.Ordered.Reduces.refl {L : FirstOrder.Language} [L.IsRelational] (K : Query L) : Reduces K K

First-order reducibility is reflexive.

theorem Cslib.Logic.FO.Ordered.Reduces.trans {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} [L'.IsRelational] [L''.IsRelational] {K : Query L} {K' : Query L'} {K'' : Query L''} (h : Reduces K K') (h' : Reduces K' K'') : Reduces K K''

First-order reducibility is transitive [Immerman1999, Exercise 2.15(1)].

theorem Cslib.Logic.FO.Ordered.Reduces.compl {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Query L} {K' : Query L'} (h : Reduces K K') : Reduces Kᶜ K'ᶜ

A reduction of K to K' reduces the complement of K to that of K'.

theorem Cslib.Logic.FO.Ordered.Reduces.of_interpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Query L} {K' : Query L'} {k : ℕ} {I : DomainInterpretation L L' k} (hI : I.Admissible) (C : I.Certificate) (h : ∀ (M : Structure L), M ∈ K ↔ I.map hI M ∈ K') : Reduces K K'

A certified admissible interpretation that maps exactly the members of K into K' reduces K to K'.

theorem Cslib.Logic.FO.Ordered.Definable.of_reduces {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Query L} {K' : Query L'} (h : Reduces K K') (hK' : Definable K') : Definable K

First-order definability pulls back along first-order reductions, by the certified pullback of the defining sentence.