Relativized first-order projections

A Projection N N' L L' ι interprets numeric vocabulary N' using only numeric vocabulary N, and each output relation of L' by a projection formula over N and the input vocabulary L. The domain is numeric as well: input bits affect neither the output universe nor numeric tests.

This is a relativized, vocabulary-parametric extension of first-order projections Immerman and Landau, Definitions 3.3--3.6. Classical projections additionally use a positive-dimensional full tuple universe and preserve the canonical numeric predicates. Neither those restrictions nor a logarithmic-space encoding theorem are implicit here. The target vocabularies are relational, as required by Interpretation; numeric constants can instead be represented by unary predicates.

Main definitions

• Cslib.Logic.FO.Projection: a numeric interpretation and a projection formula for each output relation.
• Cslib.Logic.FO.Projection.toInterpretation: the ordinary interpretation on the sum vocabularies.
• Cslib.Logic.FO.Projection.inputStructure: the output input-relation structure on the numeric model.
• Cslib.Logic.FO.Projection.tupleInputStructure: the output input-relation structure on the full tuple domain.
• Cslib.Logic.FO.Projection.onFormula: pull back a projection formula to a projection formula.
• Cslib.Logic.FO.Projection.comp: composition, with product coordinates.

Main results

• Cslib.Logic.FO.Projection.realize_onFormula: projection pullback preserves truth.
• Cslib.Logic.FO.Projection.modelEquiv: agreement with the ordinary interpretation of sum vocabularies.
• Cslib.Logic.FO.Projection.tupleModelEquiv: isomorphism of the numeric model with the full tuple domain when the numeric domain formula always holds.
• Cslib.Logic.FO.Projection.compEquiv: composition agrees with successive interpretations of both vocabularies.
• Cslib.Logic.FO.Projection.relMap_comp_inputStructure, Cslib.Logic.FO.Projection.realize_comp_rel_tupleStructure: the input relations of a composite projection are those of the iterated projection.
• Cslib.Logic.FO.Projection.IsQF.comp: quantifier-free relativized projections compose.

References

• N. Immerman, Descriptive Complexity
• N. Immerman and S. Landau, The Complexity of Iterated Multiplication

structure Cslib.Logic.FO.Projection (N : FirstOrder.Language) (N' : FirstOrder.Language) (L : FirstOrder.Language) (L' : FirstOrder.Language) (ι : Type u_1) : Type (max (max (max (max (max u_1 u_2) u_3) u_5) u_7) u_9)

A relativized projection between two numeric/input vocabulary pairs. Numeric predicates and the output domain are interpreted without access to the input relations.

• numeric : Interpretation N N' ι

  Interpret the output numeric structure and domain using numeric formulas alone.

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

  Each output input-relation bit is a numeric choice of a constant or input literal.

def Cslib.Logic.FO.Projection.toInterpretation {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Projection N N' L L' ι) : Interpretation (N.sum L) (N'.sum L') ι

Forget the projection restriction, retaining an ordinary interpretation.

@[instance_reducible]

def Cslib.Logic.FO.Projection.inputStructure {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Projection N N' L L' ι) (M : Type u_4) [N.Structure M] [L.Structure M] [L'.IsRelational] : L'.Structure (I.numeric.Model M)

The output input-relation structure. It is supplied explicitly so that it does not compete with the numeric structure instance on the same universe.

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

def Cslib.Logic.FO.Projection.modelEquiv {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} [N'.IsRelational] [L'.IsRelational] (I : Projection N N' L L' ι) (M : Type u_4) [N.Structure M] [L.Structure M] : (N'.sum L').Equiv (I.numeric.Model M) (I.toInterpretation.Model M)

The numeric model with projected input relations agrees with the ordinary interpretation of the sum vocabularies. This connects projection semantics to the existing interpretation API.

def Cslib.Logic.FO.Projection.onLiteral {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} (I : Projection N N' L L' ι) : InputLiteral L' α → ProjectionFormula N L (α × ι)

Pull back one literal, substituting a projection for its relation and preserving polarity.

noncomputable def Cslib.Logic.FO.Projection.onFormula {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} [Finite ι] [N'.IsRelational] (I : Projection N N' L L' ι) (p : ProjectionFormula N' L' α) : ProjectionFormula N L (α × ι)

Pull back a projection formula. Numeric tests use the ordinary numeric interpretation; input literals are replaced by projections.

theorem Cslib.Logic.FO.Projection.realize_onFormula {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} [Finite ι] [N'.IsRelational] [L'.IsRelational] (I : Projection N N' L L' ι) {M : Type u_4} [N.Structure M] [L.Structure M] (p : ProjectionFormula N' L' α) (x : α → I.numeric.Model M) : ((I.onFormula p).toFormula.Realize fun (q : α × ι) => ↑(x q.1) q.2) ↔ p.toFormula.Realize x

Projection pullback is truth preserving on the interpreted numeric universe, equipped with the input relations specified by the projection.

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

The identity projection, with one coordinate and unchanged numeric and input relations.

def Cslib.Logic.FO.Projection.idEquiv {N : FirstOrder.Language} {L : FirstOrder.Language} [N.IsRelational] [L.IsRelational] (M : Type u_4) [N.Structure M] [L.Structure M] : (N.sum L).Equiv ((Projection.id N L).numeric.Model M) M

The identity projection preserves both numeric and input relations.

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

Compose projections, including their numeric interpretations. The output coordinate type is the product of the two coordinate types.

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

A composite projection is isomorphic to successive interpretation, preserving both numeric and input relations. The underlying equivalence is the existing numeric composition map.

theorem Cslib.Logic.FO.Projection.comp_numeric {N : FirstOrder.Language} {N' : FirstOrder.Language} {N'' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [N'.IsRelational] (J : Projection N' N'' L' L'' κ) (I : Projection N N' L L' ι) : (J.comp I).numeric = J.numeric.comp I.numeric

The numeric interpretation of a composite projection is the composite of the numeric interpretations.

theorem Cslib.Logic.FO.Projection.comp_numeric_domain {N : FirstOrder.Language} {N' : FirstOrder.Language} {N'' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [N'.IsRelational] (J : Projection N' N'' L' L'' κ) (I : Projection N N' L L' ι) : (J.comp I).numeric.domain = (J.numeric.comp I.numeric).domain

theorem Cslib.Logic.FO.Projection.comp_numeric_rel {N : FirstOrder.Language} {N' : FirstOrder.Language} {N'' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [N'.IsRelational] (J : Projection N' N'' L' L'' κ) (I : Projection N N' L L' ι) {n : ℕ} (R : N''.Relations n) : (J.comp I).numeric.rel R = (J.numeric.comp I.numeric).rel R

@[simp]

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

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

An input relation of a composite projection holds exactly when it holds after successive interpretation.

Projections on all tuples

@[instance_reducible]

def Cslib.Logic.FO.Projection.tupleInputStructure {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Projection N N' L L' ι) (M : Type u_4) [N.Structure M] [L.Structure M] [L'.IsRelational] : L'.Structure (ι → M)

The input relations defined by a projection on all tuples ι → M, beside the numeric relations Interpretation.tupleStructure of its numeric interpretation.

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

def Cslib.Logic.FO.Projection.tupleModelEquiv {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} [N'.IsRelational] [L'.IsRelational] (I : Projection N N' L L' ι) (M : Type u_4) [N.Structure M] [L.Structure M] (hdom : ∀ (x : ι → M), I.numeric.domain.Realize x) : (N'.sum L').Equiv (I.numeric.Model M) (ι → M)

When the numeric domain formula of a projection holds of every tuple, the numeric model with projected input relations is isomorphic to the tuples with the numeric and input relations defined by the projection.

@[simp]

theorem Cslib.Logic.FO.Projection.tupleModelEquiv_apply {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} [N'.IsRelational] [L'.IsRelational] (I : Projection N N' L L' ι) (M : Type u_4) [N.Structure M] [L.Structure M] (hdom : ∀ (x : ι → M), I.numeric.domain.Realize x) (x : I.numeric.Model M) : (I.tupleModelEquiv M hdom) x = ↑x

theorem Cslib.Logic.FO.Projection.realize_onFormula_tupleStructure {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} [Finite ι] [N'.IsRelational] [L'.IsRelational] (I : Projection N N' L L' ι) {M : Type u_4} [N.Structure M] [L.Structure M] (hdom : ∀ (x : ι → M), I.numeric.domain.Realize x) (p : ProjectionFormula N' L' α) (v : α → ι → M) : ((I.onFormula p).toFormula.Realize fun (q : α × ι) => v q.1 q.2) ↔ p.toFormula.Realize v

The pullback of a projection formula along a projection whose numeric domain formula holds of every tuple is realized as the projection formula on tuples.

theorem Cslib.Logic.FO.Projection.realize_comp_rel_tupleStructure {N : FirstOrder.Language} {N' : FirstOrder.Language} {N'' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [N'.IsRelational] [L'.IsRelational] (J : Projection N' N'' L' L'' κ) (I : Projection N N' L L' ι) {M : Type u_4} [N.Structure M] [L.Structure M] (hdom : ∀ (x : ι → M), I.numeric.domain.Realize x) {n : ℕ} (R : L''.Relations n) (v : Fin n × κ × ι → M) : ((J.comp I).rel R).toFormula.Realize v ↔ (J.rel R).toFormula.Realize fun (p : Fin n × κ) (i : ι) => v (p.1, p.2, i)

An input relation formula of a composite projection J.comp I, when the numeric domain formula of I holds of every tuple, is realized as that of J on the tuples of I.

structure Cslib.Logic.FO.Projection.IsQF {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Projection N N' L L' ι) : Prop

A quantifier-free relativized projection has a quantifier-free numeric interpretation and quantifier-free numeric guards in every input-relation definition. A classical qfp further restricts the numeric vocabulary and its interpretation; in particular the convention of Immerman and Landau, Definition 3.6 excludes BIT.

• numeric : I.numeric.IsQF

  The numeric domain and relation definitions are quantifier-free.

• rel {n : ℕ} (R : L'.Relations n) : (I.rel R).IsQF

  The numeric guards in each output input-relation definition are quantifier-free.

theorem Cslib.Logic.FO.Projection.IsQF.toInterpretation {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {I : Projection N N' L L' ι} (hI : I.IsQF) : I.toInterpretation.IsQF

theorem Cslib.Logic.FO.Projection.IsQF.onLiteral {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} {I : Projection N N' L L' ι} (hI : I.IsQF) (l : InputLiteral L' α) : (I.onLiteral l).IsQF

theorem Cslib.Logic.FO.Projection.IsQF.onFormula {N : FirstOrder.Language} {N' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} [Finite ι] [N'.IsRelational] {I : Projection N N' L L' ι} (hI : I.IsQF) {p : ProjectionFormula N' L' α} (hp : p.IsQF) : (I.onFormula p).IsQF

theorem Cslib.Logic.FO.Projection.isQF_id (N : FirstOrder.Language) (L : FirstOrder.Language) : (Projection.id N L).IsQF

theorem Cslib.Logic.FO.Projection.IsQF.comp {N : FirstOrder.Language} {N' : FirstOrder.Language} {N'' : FirstOrder.Language} {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [N'.IsRelational] {J : Projection N' N'' L' L'' κ} {I : Projection N N' L L' ι} (hJ : J.IsQF) (hI : I.IsQF) : (J.comp I).IsQF

Quantifier-free relativized projections compose. Requiring both numeric interpretations to be quantifier-free prevents the substitution from introducing quantified numeric tests.