Existential second-order logic

An existential second-order sentence ∃ R₁ … Rₖ, φ over a language L quantifies finitely many relation variables R₁, …, Rₖ of given arities over a first-order sentence φ of L extended by them. It holds in an L-structure M when some relations R₁, …, Rₖ on M make φ true, that is, when some expansion of M by these relations is a model of φ Fagin, Section 2, Immerman, Section 7.1. The relation variables form the relational language ESO.varLanguage arity, and the sentence φ is a sentence of Mathlib's first-order logic over L.sum (ESO.varLanguage arity).

A class of structures is existential second-order definable (ESO.Definable) when some existential second-order sentence holds in exactly its finite members; Fagin calls these classes generalized spectra, and his theorem identifies them with the classes decidable in nondeterministic polynomial time. The existential second-order definable classes contain the first-order definable ones, are closed under intersection and union, and are closed under isomorphism.

Main definitions

• Cslib.Logic.ESO.varLanguage: the relational language of relation variables of given arities.
• Cslib.Logic.ESO.Sentence: existential second-order sentences, with Sentence.Realize.
• Cslib.Logic.ESO.Sentence.ofSentence: a first-order sentence as an existential second-order one.
• Cslib.Logic.ESO.Definable: existential second-order definability of a class of finite structures.

Main results

• Cslib.Logic.ESO.Sentence.realize_ofSentence, Cslib.Logic.ESO.Sentence.realize_inf, Cslib.Logic.ESO.Sentence.realize_sup: semantics of the embedding of first-order logic and of conjunction and disjunction.
• Cslib.Logic.ESO.Sentence.realize_iff_of_equiv: invariance under isomorphism.
• Cslib.Logic.ESO.Definable.of_fo, Cslib.Logic.ESO.Definable.inter, Cslib.Logic.ESO.Definable.union, Cslib.Logic.ESO.Definable.isoClosed.

References

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

Relation variables

def Cslib.Logic.ESO.varLanguage {ι : Type} (arity : ι → ℕ) : FirstOrder.Language

The relational language with a relation symbol of arity arity i for each i : ι: the relation variables of an existential second-order sentence.

instance Cslib.Logic.ESO.instIsRelationalVarLanguage {ι : Type} (arity : ι → ℕ) : (varLanguage arity).IsRelational

@[instance_reducible]

def Cslib.Logic.ESO.varLanguage.structure {ι : Type} {arity : ι → ℕ} {M : Type w} (R : (i : ι) → Set (Fin (arity i) → M)) : (varLanguage arity).Structure M

The structure interpreting each relation variable i as the relation R i.

theorem Cslib.Logic.ESO.varLanguage.relMap_structure {ι : Type} {arity : ι → ℕ} {M : Type w} (R : (i : ι) → Set (Fin (arity i) → M)) {n : ℕ} (r : (varLanguage arity).Relations n) (x : Fin n → M) : FirstOrder.Language.Structure.RelMap r x ↔ x ∘ Fin.cast ⋯ ∈ R ↑r

def Cslib.Logic.ESO.varLanguage.sumInl {ι ι' : Type} {arity : ι → ℕ} {arity' : ι' → ℕ} : varLanguage arity →ᴸ varLanguage (Sum.elim arity arity')

The relation variables of arity among those of Sum.elim arity arity'.

def Cslib.Logic.ESO.varLanguage.sumInr {ι ι' : Type} {arity : ι → ℕ} {arity' : ι' → ℕ} : varLanguage arity' →ᴸ varLanguage (Sum.elim arity arity')

The relation variables of arity' among those of Sum.elim arity arity'.

theorem Cslib.Logic.ESO.varLanguage.sumInl_isExpansionOn {ι ι' : Type} {arity : ι → ℕ} {arity' : ι' → ℕ} {M : Type w} (R : (i : ι ⊕ ι') → Set (Fin (Sum.elim arity arity' i) → M)) : sumInl.IsExpansionOn M

theorem Cslib.Logic.ESO.varLanguage.sumInr_isExpansionOn {ι ι' : Type} {arity : ι → ℕ} {arity' : ι' → ℕ} {M : Type w} (R : (i : ι ⊕ ι') → Set (Fin (Sum.elim arity arity' i) → M)) : sumInr.IsExpansionOn M

Sentences

structure Cslib.Logic.ESO.Sentence (L : FirstOrder.Language) : Type (max (max 1 u) v)

An existential second-order sentence ∃ R₁ … Rₖ, φ over L: finitely many relation variables with their arities, and a first-order sentence φ of L extended by them.

• Var : Type

  The relation variables.

• finite : Finite self.Var
• arity : self.Var → ℕ

  The arity of each relation variable.

• matrix : (L.sum (varLanguage self.arity)).Sentence

  The first-order part, a sentence of L extended by the relation variables.

def Cslib.Logic.ESO.Sentence.Realize {L : FirstOrder.Language} (Φ : Sentence L) (M : Type w) [L.Structure M] : Prop

An existential second-order sentence holds in M when some relations on M, interpreting its relation variables, make its first-order part true.

def Cslib.Logic.ESO.Sentence.ofSentence {L : FirstOrder.Language} (φ : L.Sentence) : Sentence L

A first-order sentence, as an existential second-order sentence without relation variables.

@[simp]

theorem Cslib.Logic.ESO.Sentence.realize_ofSentence {L : FirstOrder.Language} {M : Type w} [L.Structure M] (φ : L.Sentence) : (ofSentence φ).Realize M ↔ M ⊨ φ

The embedding of first-order logic preserves truth.

@[instance_reducible]

instance Cslib.Logic.ESO.Sentence.instMin {L : FirstOrder.Language} : Min (Sentence L)

The conjunction of two existential second-order sentences, which quantifies the relation variables of both.

@[instance_reducible]

instance Cslib.Logic.ESO.Sentence.instMax {L : FirstOrder.Language} : Max (Sentence L)

The disjunction of two existential second-order sentences, which quantifies the relation variables of both.

theorem Cslib.Logic.ESO.Sentence.realize_onSentence_sumInl {L : FirstOrder.Language} {M : Type w} [L.Structure M] {Φ Ψ : Sentence L} (R : (i : Φ.Var ⊕ Ψ.Var) → Set (Fin (Sum.elim Φ.arity Ψ.arity i) → M)) : M ⊨ ((FirstOrder.Language.LHom.id L).sumMap varLanguage.sumInl).onSentence Φ.matrix ↔ M ⊨ Φ.matrix

Relations for the variables of Φ ⊓ Ψ restrict to relations for the variables of Φ.

theorem Cslib.Logic.ESO.Sentence.realize_onSentence_sumInr {L : FirstOrder.Language} {M : Type w} [L.Structure M] {Φ Ψ : Sentence L} (R : (i : Φ.Var ⊕ Ψ.Var) → Set (Fin (Sum.elim Φ.arity Ψ.arity i) → M)) : M ⊨ ((FirstOrder.Language.LHom.id L).sumMap varLanguage.sumInr).onSentence Ψ.matrix ↔ M ⊨ Ψ.matrix

Relations for the variables of Φ ⊓ Ψ restrict to relations for the variables of Ψ.

@[simp]

theorem Cslib.Logic.ESO.Sentence.realize_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {Φ Ψ : Sentence L} : (Φ ⊓ Ψ).Realize M ↔ Φ.Realize M ∧ Ψ.Realize M

Conjunction: Φ ⊓ Ψ holds exactly when both Φ and Ψ hold.

@[simp]

theorem Cslib.Logic.ESO.Sentence.realize_sup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {Φ Ψ : Sentence L} : (Φ ⊔ Ψ).Realize M ↔ Φ.Realize M ∨ Ψ.Realize M

Disjunction: Φ ⊔ Ψ holds exactly when Φ or Ψ holds.

def Cslib.Logic.ESO.Sentence.expansionEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (Φ : Sentence L) (e : L.Equiv M N) (R : (i : Φ.Var) → Set (Fin (Φ.arity i) → M)) : (L.sum (varLanguage Φ.arity)).Equiv M N

An isomorphism M ≃[L] N, together with relations on M and their images on N, is an isomorphism of the expansions.

theorem Cslib.Logic.ESO.Sentence.realize_of_equiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (Φ : Sentence L) (e : L.Equiv M N) (h : Φ.Realize M) : Φ.Realize N

theorem Cslib.Logic.ESO.Sentence.realize_iff_of_equiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (Φ : Sentence L) (e : L.Equiv M N) : Φ.Realize M ↔ Φ.Realize N

Existential second-order sentences are invariant under isomorphism.

Definable classes

def Cslib.Logic.ESO.Definable {L : FirstOrder.Language} (K : Set (CategoryTheory.Bundled L.Structure)) : Prop

A class of structures is existential second-order definable when some existential second-order sentence holds in exactly its finite members, among all finite structures: it is a generalized spectrum Fagin, Section 2.

theorem Cslib.Logic.ESO.Definable.of_fo {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} (hK : FO.Definable K) : Definable K

First-order definable classes are existential second-order definable.

theorem Cslib.Logic.ESO.Definable.inter {L : FirstOrder.Language} {K₁ K₂ : Set (CategoryTheory.Bundled L.Structure)} (h₁ : Definable K₁) (h₂ : Definable K₂) : Definable (K₁ ∩ K₂)

The intersection of two existential second-order definable classes is existential second-order definable.

theorem Cslib.Logic.ESO.Definable.union {L : FirstOrder.Language} {K₁ K₂ : Set (CategoryTheory.Bundled L.Structure)} (h₁ : Definable K₁) (h₂ : Definable K₂) : Definable (K₁ ∪ K₂)

The union of two existential second-order definable classes is existential second-order definable.

theorem Cslib.Logic.ESO.Definable.isoClosed {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} (hK : Definable K) : IsoClosed K

An existential second-order definable class is closed under isomorphism.