First-order interpretations

A first-order interpretation I of a relational language L' in a language L, of dimension ι (a finite type), consists of a domain formula δ of L in variables ι and, for each relation symbol R of L' of arity n, a formula I.rel R of L with a block of variables ι for each of the n arguments. In an L-structure M it defines the L'-structure I.Model M whose elements are the tuples x : ι → M satisfying δ, with R holding of x₁, …, xₙ when I.rel R holds of their coordinates. Equality of the interpreted structure is equality of tuples. These are Immerman's first-order queries Immerman, Section 1.4, with a finite type of coordinates in place of the dimension k, so that composites need no reindexing.

Every formula φ of L' pulls back to a formula I.onFormula φ of L, obtained by replacing each variable by a tuple of variables, each relation symbol by its defining formula, equality by equality of coordinates, and each quantifier by a quantifier over a block of variables relativized to δ. Truth is preserved: M ⊨ I.onSentence φ ↔ I.Model M ⊨ φ Immerman, Definition 3.3 and Proposition 3.5. Interpretations act on isomorphisms (Interpretation.mapEquiv) and compose (Interpretation.comp), the interpreted structure of a composite being isomorphic to the iterated one (Interpretation.compEquiv).

The arguments of Interpretation L L' ι are in the order of the map on structures, which turns L-structures into L'-structures as a reduction turns instances of one problem into instances of another; formulas are mapped the other way, from L' to L.

Senellart and Gnatenko build interpretations, the pullback of formulas and first-order reductions over Mathlib's model theory as well Senellart and Gnatenko. Their interpretations are tagged: the interpreted universe is all of Tag × (Fin dim → M) for a finite type of tags, with no domain formula (a relativized variant restricts it), and a relation symbol has a defining formula for each choice of tags of its arguments. Here the interpreted universe is the set of tuples ι → M defined by the domain formula, with no tags, and the coordinates range over any finite type ι rather than Fin dim, so that the coordinates κ × ι of a composite need no reindexing.

Main definitions

• Cslib.Logic.FO.Interpretation: a first-order interpretation of L' in L of dimension ι.
• Cslib.Logic.FO.Interpretation.Model: the L'-structure interpreted in an L-structure.
• Cslib.Logic.FO.Interpretation.onFormula, Cslib.Logic.FO.Interpretation.onSentence: the pullback of formulas and sentences of L' to formulas and sentences of L.
• Cslib.Logic.FO.Interpretation.id: the identity interpretation of a relational language.
• Cslib.Logic.FO.Interpretation.comp: the composite of two interpretations.

Main results

• Cslib.Logic.FO.Interpretation.realize_onFormula, Cslib.Logic.FO.Interpretation.realize_onSentence: the pullback of a formula holds in M exactly when the formula holds in the interpreted structure.
• Cslib.Logic.FO.Interpretation.mapEquiv: isomorphic structures interpret isomorphic structures.
• Cslib.Logic.FO.Interpretation.idEquiv, Cslib.Logic.FO.Interpretation.compEquiv: the identity and composite interpretations, up to isomorphism.
• Cslib.Logic.FO.Interpretation.realize_comp_domain, Cslib.Logic.FO.Interpretation.relMap_comp_model: the domain and relations of a composite interpreted structure are those of the iterated one.

Implementation notes

The interpreted language is relational, as in finite model theory: interpreting function symbols would need, in every structure, a proof that their defining formulas define functions. There is no congruence relation, so equality is interpreted by equality of tuples, as in Immerman's first-order queries. The pullback uses Mathlib's FirstOrder.Language.Formula.iAlls and FirstOrder.Language.Formula.iInf, which choose an enumeration of ι, so it is noncomputable.

References

• N. Immerman, Descriptive Complexity
• P. Senellart and A. Gnatenko, Descriptive Complexity in Lean: Completeness by First-Order Reductions

structure Cslib.Logic.FO.Interpretation (L : FirstOrder.Language) (L' : FirstOrder.Language) (ι : Type u_1) : Type (max (max (max u u_1) v) v')

A first-order interpretation of the language L' in the language L, of dimension ι: a domain formula in variables ι, and for each relation symbol of L' of arity n a formula with variables Fin n × ι, a block of ι variables for each argument.

• domain : L.Formula ι

  The domain formula: the elements of an interpreted structure are the tuples satisfying it.

• rel {n : ℕ} : L'.Relations n → L.Formula (Fin n × ι)

  The formula defining a relation symbol, with a block of variables for each argument.

def Cslib.Logic.FO.Interpretation.empty (L : FirstOrder.Language) (L' : FirstOrder.Language) : Interpretation L L' Unit

The interpretation of dimension one with an empty domain.

def Cslib.Logic.FO.termVar {L' : FirstOrder.Language} [L'.IsRelational] {β : Type u_1} : L'.Term β → β

In a relational language a term is a variable; this is that variable.

@[simp]

theorem Cslib.Logic.FO.termVar_var {L' : FirstOrder.Language} [L'.IsRelational] {β : Type u_1} (x : β) : termVar (FirstOrder.Language.var x) = x

theorem Cslib.Logic.FO.realize_termVar {L' : FirstOrder.Language} [L'.IsRelational] {β : Type u_1} {N : Type u_2} [L'.Structure N] (t : L'.Term β) (v : β → N) : FirstOrder.Language.Term.realize v t = v (termVar t)

In a relational language a term takes the value of its variable.

def Cslib.Logic.FO.Interpretation.Model {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Interpretation L L' ι) (M : Type w) [L.Structure M] : Type (max u_1 w)

The universe of the structure interpreted by I in M: the tuples satisfying the domain formula.

def Cslib.Logic.FO.Interpretation.Model.mk {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] (x : ι → M) (hx : I.domain.Realize x) : I.Model M

Construct an element of the interpreted structure from a tuple satisfying the domain formula. Using this constructor rather than Subtype.mk keeps the syntactic type I.Model M at reducible transparency.

@[simp]

theorem Cslib.Logic.FO.Interpretation.Model.val_mk {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] (x : ι → M) (hx : I.domain.Realize x) : ↑(mk x hx) = x

theorem Cslib.Logic.FO.Interpretation.Model.ext {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] {x y : I.Model M} (h : ↑x = ↑y) : x = y

theorem Cslib.Logic.FO.Interpretation.Model.ext_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] {x y : I.Model M} : x = y ↔ ∀ (i : ι), ↑x i = ↑y i

Elements of an interpreted structure are equal when all their coordinates are.

instance Cslib.Logic.FO.Interpretation.instFiniteModel {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] [Finite ι] [Finite M] : Finite (I.Model M)

@[instance_reducible]

instance Cslib.Logic.FO.Interpretation.instStructureModel {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] [L'.IsRelational] : L'.Structure (I.Model M)

The structure interpreted by I in M: a relation symbol holds of some tuples when its defining formula holds of their coordinates.

theorem Cslib.Logic.FO.Interpretation.relMap_model {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] [L'.IsRelational] {n : ℕ} (R : L'.Relations n) (x : Fin n → I.Model M) : FirstOrder.Language.Structure.RelMap R x ↔ (I.rel R).Realize fun (p : Fin n × ι) => ↑(x p.1) p.2

Isomorphisms

def Cslib.Logic.FO.Interpretation.mapEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {M : Type w} [L.Structure M] [L'.IsRelational] {N : Type u_2} [L.Structure N] (I : Interpretation L L' ι) (e : L.Equiv M N) : L'.Equiv (I.Model M) (I.Model N)

Interpretations act on isomorphisms: an isomorphism M ≃[L] N maps tuples of M coordinatewise to tuples of N.

@[simp]

theorem Cslib.Logic.FO.Interpretation.mapEquiv_apply_val {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] [L'.IsRelational] {N : Type u_2} [L.Structure N] (e : L.Equiv M N) (x : I.Model M) : ↑((I.mapEquiv e) x) = ⇑e ∘ ↑x

The pullback of formulas

def Cslib.Logic.FO.Interpretation.snocVar {ι : Type u_1} {α : Type u_3} {n : ℕ} (p : (α ⊕ Fin (n + 1)) × ι) : (α ⊕ Fin n) × ι ⊕ ι

The variables of the pullback of the body of a quantifier: the coordinates of the newly bound variable become the variables Sum.inr, to be quantified.

noncomputable def Cslib.Logic.FO.Interpretation.onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Interpretation L L' ι) [L'.IsRelational] [Finite ι] {α : Type u_3} {n : ℕ} : L'.BoundedFormula α n → L.Formula ((α ⊕ Fin n) × ι)

The pullback of a bounded formula of L' along I, with each free or bound variable replaced by a block of free variables: relation symbols are replaced by their defining formulas, equality by equality of all coordinates, and quantifiers by quantifiers over tuples satisfying the domain formula.

theorem Cslib.Logic.FO.Interpretation.realize_onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] [L'.IsRelational] [Finite ι] {α : Type u_3} {n : ℕ} (φ : L'.BoundedFormula α n) (v : α → I.Model M) (xs : Fin n → I.Model M) : ((I.onBoundedFormula φ).Realize fun (p : (α ⊕ Fin n) × ι) => ↑(Sum.elim v xs p.1) p.2) ↔ φ.Realize v xs

The pullback of a bounded formula holds of the coordinates of some elements of the interpreted structure exactly when the formula holds of these elements.

noncomputable def Cslib.Logic.FO.Interpretation.onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Interpretation L L' ι) [L'.IsRelational] [Finite ι] {α : Type u_3} (φ : L'.Formula α) : L.Formula (α × ι)

The pullback of a formula of L' along I: a formula of L with a block of variables ι for each free variable.

@[simp]

theorem Cslib.Logic.FO.Interpretation.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} {M : Type w} [L.Structure M] [L'.IsRelational] [Finite ι] {α : Type u_3} (φ : L'.Formula α) (v : α → I.Model M) : ((I.onFormula φ).Realize fun (p : α × ι) => ↑(v p.1) p.2) ↔ φ.Realize v

The pullback of a formula holds of the coordinates of some elements of the interpreted structure exactly when the formula holds of these elements Immerman, Proposition 3.5 and Remark 3.6.

noncomputable def Cslib.Logic.FO.Interpretation.onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Interpretation L L' ι) [L'.IsRelational] [Finite ι] (φ : L'.Sentence) : L.Sentence

The pullback of a sentence of L' along I, a sentence of L Immerman, Definition 3.3.

@[simp]

theorem Cslib.Logic.FO.Interpretation.realize_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Interpretation L L' ι} (M : Type w) [L.Structure M] [L'.IsRelational] [Finite ι] (φ : L'.Sentence) : M ⊨ I.onSentence φ ↔ I.Model M ⊨ φ

The pullback of a sentence holds in M exactly when the sentence holds in the structure interpreted by I in M Immerman, Proposition 3.5.

The identity and composite interpretations

def Cslib.Logic.FO.Interpretation.id (L : FirstOrder.Language) : Interpretation L L Unit

The identity interpretation of a relational language, of dimension one: every element is in the domain and every relation symbol defines itself.

def Cslib.Logic.FO.Interpretation.idEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] [L.IsRelational] : L.Equiv ((Interpretation.id L).Model M) M

The structure interpreted by the identity interpretation is the structure itself.

noncomputable def Cslib.Logic.FO.Interpretation.comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {ι : Type u_1} {κ : Type u_2} [Finite ι] [L'.IsRelational] [Finite κ] (J : Interpretation L' L'' κ) (I : Interpretation L L' ι) : Interpretation L L'' (κ × ι)

The composite of an interpretation I of L' in L and an interpretation J of L'' in L', an interpretation of L'' in L whose tuples are indexed by pairs: the domain formula says that each block is in the domain of I and that the blocks satisfy the pullback of the domain formula of J, and the relation symbols are defined by the pullbacks of their definitions in J.

def Cslib.Logic.FO.Interpretation.compEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Type u_1} {κ : Type u_2} [Finite ι] [L'.IsRelational] [L''.IsRelational] [Finite κ] (J : Interpretation L' L'' κ) (I : Interpretation L L' ι) : L''.Equiv (J.Model (I.Model M)) ((J.comp I).Model M)

The composite of interpretations interprets, up to isomorphism, the structure interpreted by J in the structure interpreted by I.

@[simp]

theorem Cslib.Logic.FO.Interpretation.compEquiv_symm_apply_val_val {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Type u_1} {κ : Type u_2} [Finite ι] [L'.IsRelational] [L''.IsRelational] [Finite κ] (J : Interpretation L' L'' κ) (I : Interpretation L L' ι) (z : (J.comp I).Model M) (j : κ) (i : ι) : ↑(↑((J.compEquiv I).symm z) j) i = ↑z (j, i)

theorem Cslib.Logic.FO.Interpretation.realize_comp_domain {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Type u_1} {κ : Type u_2} [Finite ι] [L'.IsRelational] [Finite κ] (J : Interpretation L' L'' κ) (I : Interpretation L L' ι) (v : κ × ι → M) : (J.comp I).domain.Realize v ↔ ∃ (h : ∀ (j : κ), I.domain.Realize fun (i : ι) => v (j, i)), J.domain.Realize fun (j : κ) => Model.mk (fun (i : ι) => v (j, i)) ⋯

The domain formula of a composite holds of a tuple exactly when each of its blocks is in the domain of I and the blocks, as elements of the structure interpreted by I, satisfy the domain formula of J.

theorem Cslib.Logic.FO.Interpretation.relMap_comp_model {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Type u_1} {κ : Type u_2} [Finite ι] [L'.IsRelational] [L''.IsRelational] [Finite κ] (J : Interpretation L' L'' κ) (I : Interpretation L L' ι) {n : ℕ} (R : L''.Relations n) (x : Fin n → (J.comp I).Model M) : FirstOrder.Language.Structure.RelMap R x ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => (J.compEquiv I).symm (x i)

A relation of a composite interpreted structure holds exactly when it holds in the iterated interpreted structure.