Existential second-order logic and first-order reductions

An existential second-order sentence ∃ R₁ … Rₖ, φ of a relational language L' pulls back along a first-order interpretation I of L' in L of dimension κ: a relation variable of arity n becomes a relation variable of arity n * Nat.card κ, holding of the concatenated coordinates of n tuples, and φ pulls back along the extension of I that defines each relation variable by the corresponding new one Immerman, Definition 3.3. The pullback holds in M exactly when the sentence holds in I.Model M (FO.Interpretation.realize_onESOSentence), so existential second-order definability is closed under first-order reductions Immerman, Framework 3.12.

Main definitions

• Cslib.Logic.FO.Interpretation.sumVar: an interpretation extended to relation variables.
• Cslib.Logic.FO.Interpretation.onESOSentence: the pullback of an existential second-order sentence along an interpretation.

Main results

• Cslib.Logic.FO.Interpretation.realize_onESOSentence: the pullback holds in M exactly when the sentence holds in I.Model M.
• Cslib.Logic.ESO.Definable.of_reduces: existential second-order definability is closed under first-order reductions.

References

• N. Immerman, Descriptive Complexity

noncomputable def Cslib.Logic.FO.Interpretation.blockEquiv (κ : Type) [Finite κ] (n : ℕ) : Fin (n * Nat.card κ) ≃ Fin n × κ

The positions of n tuples indexed by κ, concatenated into a sequence of length n * Nat.card κ: each position is a coordinate of one of the tuples.

noncomputable def Cslib.Logic.FO.Interpretation.sumVar {L : FirstOrder.Language} {L' : FirstOrder.Language} {κ : Type} [Finite κ] (I : Interpretation L L' κ) {ι : Type} (arity : ι → ℕ) : Interpretation (L.sum (ESO.varLanguage fun (i : ι) => arity i * Nat.card κ)) (L'.sum (ESO.varLanguage arity)) κ

The extension of I to relation variables: a relation variable of arity n is defined by the relation variable of arity n * Nat.card κ applied to the concatenated coordinates of its arguments.

noncomputable def Cslib.Logic.FO.Interpretation.flatten {L : FirstOrder.Language} {L' : FirstOrder.Language} {κ : Type} [Finite κ] {I : Interpretation L L' κ} {M : Type w} [L.Structure M] {n : ℕ} (x : Fin n → I.Model M) : Fin (n * Nat.card κ) → M

The concatenated coordinates of a sequence of elements of an interpreted structure.

noncomputable def Cslib.Logic.FO.Interpretation.modelRel {L : FirstOrder.Language} {L' : FirstOrder.Language} {κ : Type} [Finite κ] {I : Interpretation L L' κ} {ι : Type} {arity : ι → ℕ} {M : Type w} [L.Structure M] (R : (i : ι) → Set (Fin (arity i * Nat.card κ) → M)) (i : ι) : Set (Fin (arity i) → I.Model M)

Relations on M of arities multiplied by Nat.card κ define relations on I.Model M: a sequence of elements is related when its concatenated coordinates are.

noncomputable def Cslib.Logic.FO.Interpretation.onESOSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {κ : Type} [Finite κ] {I : Interpretation L L' κ} [L'.IsRelational] (Φ : ESO.Sentence L') : ESO.Sentence L

The pullback of an existential second-order sentence along I: the arity of each relation variable is multiplied by the number of coordinates, and the first-order part is pulled back along the extension of I to the relation variables.

def Cslib.Logic.FO.Interpretation.sumVarEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {κ : Type} [Finite κ] {I : Interpretation L L' κ} {ι : Type} {arity : ι → ℕ} {M : Type w} [L.Structure M] [L'.IsRelational] (R : (i : ι) → Set (Fin (arity i * Nat.card κ) → M)) : (L'.sum (ESO.varLanguage arity)).Equiv ((I.sumVar arity).Model M) (I.Model M)

The structure interpreted by the extension of I in the expansion of M by relations R is isomorphic to the expansion of I.Model M by the relations modelRel R.

theorem Cslib.Logic.FO.Interpretation.realize_onESOSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {κ : Type} [Finite κ] {I : Interpretation L L' κ} {M : Type w} [L.Structure M] [L'.IsRelational] (Φ : ESO.Sentence L') : (onESOSentence Φ).Realize M ↔ Φ.Realize (I.Model M)

The pullback of an existential second-order sentence along I holds in M exactly when the sentence holds in the structure interpreted by I in M.

theorem Cslib.Logic.ESO.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 : FO.Reduces K K') : Definable K

Existential second-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.