Existential projection of relation variables and guessed linear orders

Existential second-order sentences are closed under existentially quantifying additional relation variables: an existential second-order sentence Φ over L.sum (varLanguage ar₀) projects to an existential second-order sentence Φ.project over L whose relation variables are ι₀ ⊕ Φ.Var, holding in M iff some interpretation of ar₀ on M makes Φ hold (Sentence.realize_project).

In descriptive complexity on unordered structures, a standard application of Sentence.project is guessing an arbitrary strict linear order on a finite domain Fagin, Proof of Theorem 6, Immerman, Proof of Theorem 7.8. The language orderLanguage has a single binary relation symbol ltSym, constrained by isStrictLinearOrderSentence to be irreflexive, transitive, and trichotomous. On a finite structure M, the expansions satisfying isStrictLinearOrderSentence are precisely the linear orders orderRelOfEquiv e induced by bijections e : M ≃ Fin (Nat.card M) (realize_isStrictLinearOrderSentence).

Implementation notes

orderLanguage is defined as varLanguage (fun _ : Unit => 2) (with strict < symbol ltSym and isStrictLinearOrderSentence) rather than Mathlib's Language.order for two reasons:

1. Existential second-order quantification (ESO.Sentence and ESO.Sentence.project) quantifies over relation blocks of the form varLanguage arity adjoined via Language.sum. Defining orderLanguage directly as varLanguage (fun _ : Unit => 2) makes Sentence.withLinearOrder an immediate instance of Sentence.project.
2. Mathlib's Language.order represents a weak order ≤ (Language.IsOrdered), whereas the colexicographic tuple order in Fagin's power interpretation compares the highest differing coordinate via an irreflexive strict < relation.

Main definitions

• Cslib.Logic.ESO.varLanguage.sumAssoc: the homomorphism combining two blocks of relation variables into one.
• Cslib.Logic.ESO.Sentence.project: existential projection of an outer block of relation variables.
• Cslib.Logic.ESO.orderLanguage, Cslib.Logic.ESO.ltSym, Cslib.Logic.ESO.isStrictLinearOrderSentence: the binary relation variable for a guessed strict linear order and its first-order axioms.
• Cslib.Logic.ESO.orderRelOfEquiv: the binary relation on M induced by a numbering e : M ≃ Fin n.
• Cslib.Logic.ESO.Sentence.withLinearOrder: existentially quantifying a strict linear order on the domain before evaluating an ESO.Sentence (L.sum orderLanguage).

Main results

• Cslib.Logic.ESO.Sentence.realize_project: Φ.project holds in M iff Φ holds in some expansion of M by relations for ar₀.
• Cslib.Logic.ESO.realize_isStrictLinearOrderSentence_iff_irrefl_trans_trichotomous: on any domain, a binary relation satisfies isStrictLinearOrderSentence iff it is irreflexive, transitive, and trichotomous.
• Cslib.Logic.ESO.realize_isStrictLinearOrderSentence: on a finite domain M, a binary relation satisfies isStrictLinearOrderSentence iff it is orderRelOfEquiv e for some e : M ≃ Fin (Nat.card M).
• Cslib.Logic.ESO.Sentence.realize_withLinearOrder: on a finite structure M, Φ.withLinearOrder holds iff Φ holds on (M, orderRelOfEquiv e) for some numbering e : M ≃ Fin (Nat.card M).
• Cslib.Logic.ESO.Definable.of_withLinearOrder: a class characterized on every finite structure under every numbering by a sentence over L.sum orderLanguage is existential second-order definable over L.

References

• R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets
• N. Immerman, Descriptive Complexity

Projection of relation variables

def Cslib.Logic.ESO.varLanguage.sumAssoc {L : FirstOrder.Language} {ι₁ ι₂ : Type} {ar₁ : ι₁ → ℕ} {ar₂ : ι₂ → ℕ} : (L.sum (varLanguage ar₁)).sum (varLanguage ar₂) →ᴸ L.sum (varLanguage (Sum.elim ar₁ ar₂))

The homomorphism combining two successive blocks of relation variables ar₁ and ar₂ into a single block Sum.elim ar₁ ar₂.

theorem Cslib.Logic.ESO.varLanguage.sumAssoc_isExpansionOn {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι₁ ι₂ : Type} {ar₁ : ι₁ → ℕ} {ar₂ : ι₂ → ℕ} (R₁ : (i : ι₁) → Set (Fin (ar₁ i) → M)) (R₂ : (j : ι₂) → Set (Fin (ar₂ j) → M)) : sumAssoc.IsExpansionOn M

def Cslib.Logic.ESO.Sentence.project {L : FirstOrder.Language} {ι₀ : Type} [Finite ι₀] {ar₀ : ι₀ → ℕ} (Φ : Sentence (L.sum (varLanguage ar₀))) : Sentence L

Existentially quantify an additional block of relation variables ar₀, turning an existential second-order sentence over L.sum (varLanguage ar₀) into one over L.

@[simp]

theorem Cslib.Logic.ESO.Sentence.realize_project {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι₀ : Type} [Finite ι₀] {ar₀ : ι₀ → ℕ} (Φ : Sentence (L.sum (varLanguage ar₀))) : Φ.project.Realize M ↔ ∃ (R₀ : (i : ι₀) → Set (Fin (ar₀ i) → M)), Φ.Realize M

Existential projection: Φ.project holds in M exactly when Φ holds in some expansion of M by relations for ar₀.

Guessed strict linear order

@[reducible, inline]

abbrev Cslib.Logic.ESO.orderLanguage : FirstOrder.Language

The language of a single binary relation variable, used for an existentially guessed strict linear order on the domain.

def Cslib.Logic.ESO.ltSym : orderLanguage.Relations 2

The binary relation symbol < of orderLanguage.

def Cslib.Logic.ESO.isStrictLinearOrderSentence : orderLanguage.Sentence

The first-order sentence over orderLanguage asserting that ltSym is a strict linear order (irreflexive, transitive, and trichotomous).

def Cslib.Logic.ESO.orderRelOfEquiv {N : Type w} {n : ℕ} (e : N ≃ Fin n) : Unit → Set (Fin 2 → N)

The binary relation on N induced by a numbering e : N ≃ Fin n: x 0 precedes x 1 when e (x 0) < e (x 1).

theorem Cslib.Logic.ESO.relMap_ltSym {N : Type w} (R : Unit → Set (Fin 2 → N)) (x : Fin 2 → N) : FirstOrder.Language.Structure.RelMap ltSym x ↔ x ∈ R ()

theorem Cslib.Logic.ESO.realize_isStrictLinearOrderSentence_iff_irrefl_trans_trichotomous {N : Type w} (R : Unit → Set (Fin 2 → N)) : N ⊨ isStrictLinearOrderSentence ↔ ((∀ (a : N), ![a, a] ∉ R ()) ∧ ∀ (a b c : N), ![a, b] ∈ R () ∧ ![b, c] ∈ R () → ![a, c] ∈ R ()) ∧ ∀ (a b : N), ![a, b] ∈ R () ∨ a = b ∨ ![b, a] ∈ R ()

On any type N (finite or not), a binary relation satisfies isStrictLinearOrderSentence iff it is irreflexive, transitive, and trichotomous.

theorem Cslib.Logic.ESO.realize_isStrictLinearOrderSentence_orderRelOfEquiv {N : Type w} {n : ℕ} (e : N ≃ Fin n) : N ⊨ isStrictLinearOrderSentence

Every numbering e : N ≃ Fin n induces a strict linear order satisfying isStrictLinearOrderSentence.

theorem Cslib.Logic.ESO.realize_isStrictLinearOrderSentence {N : Type w} [Finite N] (R : Unit → Set (Fin 2 → N)) : N ⊨ isStrictLinearOrderSentence ↔ ∃ (e : N ≃ Fin (Nat.card N)), R = orderRelOfEquiv e

On a finite type N, a binary relation satisfies isStrictLinearOrderSentence iff it is orderRelOfEquiv e for some bijection e : N ≃ Fin (Nat.card N).

def Cslib.Logic.ESO.Sentence.withLinearOrder {L : FirstOrder.Language} (Φ : Sentence (L.sum orderLanguage)) : Sentence L

Existentially quantify a strict linear order on the domain before evaluating an existential second-order sentence Φ over L.sum orderLanguage.

theorem Cslib.Logic.ESO.Sentence.realize_withLinearOrder {L : FirstOrder.Language} {M : Type w} [L.Structure M] [Finite M] (Φ : Sentence (L.sum orderLanguage)) : Φ.withLinearOrder.Realize M ↔ ∃ (e : M ≃ Fin (Nat.card M)), Φ.Realize M

On a finite structure M, Φ.withLinearOrder holds iff Φ holds on (M, orderRelOfEquiv e) for some numbering e : M ≃ Fin (Nat.card M).

theorem Cslib.Logic.ESO.Definable.of_withLinearOrder {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} (Φ : Sentence (L.sum orderLanguage)) (hΦ : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M] (e : ↑M ≃ Fin (Nat.card ↑M)), M ∈ K ↔ Φ.Realize ↑M) : Definable K

If Φ : Sentence (L.sum orderLanguage) agrees with K on every finite structure M under every numbering e : M ≃ Fin (Nat.card M), then K is existential second-order definable over L (witnessed by Φ.withLinearOrder).